# Alex Rice

I am studying at the University of Cambridge after completing the first year of my PhD at the University of Birmingham. I am working under the supervision of Jamie Vicary.

## Contact

alex.rice at cl.cam.ac.uk | |

Office Address | Office FS35 The Computer Laboratory University of Cambridge William Gates Building Cambridge CB3 0FD United Kingdom |

Matrix | @alexarice:matrix.org |

GitHub | https://github.com/alexarice |

## About Me

My main interests at the moment are category theory, especially higher category theory, and Homotopy Type Theory. I am currently looking at various definitions of globular higher categories and am thinking about semi-strictness problems and types of composition.

Before starting my PhD I completed a 4-year integrated masters program in Mathematics and Computer Science at the University of Oxford. During this time I took courses including Category Theory (including theory of monoidal categories), Algebraic Topology, Homological Algebra, Logic, ZFC Set Theory, and Representation Theory.

I also enjoy playing with functional programming languages such as Haskell or Agda and am a user of Emacs and the Nixos Linux distribution.

## Teaching

- Teaching assistant for “Advanced Functional Programming” (Autumn 2019)
- Teaching assistant for “Logic and Computation” (Spring 2019)
- Supervisor for “Semantics of Programming Languages” (Autumn 2020)
- Supervisor for “Prolog” (Spring 2021 and Spring 2022)
- Supervisor for “Introduction to Probability” (Summer 2021)
- Supervisor for “Object Oriented Programming” (Autumn 2021)

## Events

I have attended the following events:

- SYCO 10
- FLOC 2022 (HoTT/UF, LICS, FSCD)
- YAMCATS 27
- Midlands graduate school (MGS) 2022
- Logic and Higher Structures
- FSCD 2021
- ACT 2021, which I helped organise.
- Categories and Companions Symposium 2021
- SYCO 6
- SYCO 3
- SYCO 2
- MGS Christmas lectures in Sheffield 2019

## Papers

- A Type Theory for Strictly Unital Infinity Categories (pdf, arxiv)
- A Type Theory for Strictly Associative Infinity Categories (pdf, arxiv)
- New minimal linear inferences in Boolean logic independent of switch and medial, FSCD 2021 (pdf, link)
- Coinductive Invertibility in Higher Categories (pdf,formalisation,github,arxiv)

## Talks

- December 2022: A Type Theory for Strictly Associative Infinity Categories, SYCO 10 (Slides)
- August 2022: A Type Theory for Strictly Unital Infinity Categories, LICS 2022 (Slides)
- May 2022: Type theoretic approaches to semistrict higher categories, YAMCATS 27 (Slides)
- July 2021: New minimal linear inferences in Boolean logic independent of switch and medial, FSCD 2021 (Recording, Slides)
- June 2021: Categories and Companions Symposium - Biased composition in infinity categories (Recording, Slides)
- 25th September 2020: Birmingham theory group lab lunch - Biased composition in infinity categories
- 19th March 2020: Birmingham theory group lab lunch - Coinductive Invertibility in Higher Categories (slides)

## Posts

- The Kavvos-Sojakova proof of Syllepsis in Agda
- Linear inferences of size 7 - 09/10/2020
- Strictly Associative Group Theory using Univalence - 29/05/2020
- Strictly Associative Group Theory - 26/03/2020