# 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 |

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

## About Me

My main interests at the moment are type theory, including Homotopy Type Theory, and its applications to higher category 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 formalising things in Agda and and am a user of Emacs and the NixOS Linux distribution.

## Papers

- Strictly Associative and Unital ∞-Categories as a Generalized Algebraic Theory (pdf, arxiv)
- A Type Theory for Strictly Unital Infinity Categories (pdf, arxiv, doi)
- A Type Theory for Strictly Associative Infinity Categories (pdf, arxiv)
- New minimal linear inferences in Boolean logic independent of switch and medial, Extended version in LMCS (pdf, arxiv, lmcs), originally presented at FSCD 2021 (pdf, link)
- Coinductive Invertibility in Higher Categories (pdf, formalisation, github, arxiv)

## Talks

- April 2023: Strictly Associative Group Theory using Univalence, HoTT/UF 2023 (slides)
- 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

## 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, Spring 2022, and Spring 2023)
- Supervisor for “Introduction to Probability” (Summer 2021)
- Supervisor for “Object Oriented Programming” (Autumn 2021)

## Events

I have attended the following events:

- HoTT/UF 2023
- SYCO 11
- 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