The EUR M&CS, in collaboration with the LAGA laboratory, is pleased to invite you to the latest session of its MathSTIC / EUR M&CS Colloquium. On this occasion, we will be welcoming Ulrik Buchholtz, a researcher at the University of Nottingham, for a talk at the intersection of fundamental mathematics and theoretical computer science.
The infinity-category of infinity-categories in simplicial type theory
Intervenant : Ulrik Buchholtz (University of Nottingham)
In univalent foundations, as proposed by Voevodsky, the basic objects are infinity-groupoids (or anima), so every construction and theorem respects the natural notion of equivalence for each type of mathematical object. A formal account of this is given by homotopy type theory (HoTT), based on Martin-Löf’s dependent type theory extended with Voevodsky’s univalence axiom.
I will explain and motivate simplicial type theory, along with an extension that allows us to define the infinity-category of infinity-categories. This part is based on joint work with Daniel Gratzer and Jonathan Weinberger.
Practical information
- Date : Thursday 23 April 2026
- Time: 2.00 pm
- Venue: Room B405, LAGA (Sorbonne Paris Nord University)
Can’t make it in person?
The seminar will be streamed live via the video conferencing tool at this link: https://bbb.math.univ-paris13.fr/b/chr-hyw-0rb-jz4
To find out more about Ulrik Buchholtz’s work, visit his personal page.