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