L’EUR M&CS, en collaboration avec le laboratoire LAGA, a le plaisir de vous inviter à une nouvelle séance de son Colloquium MathSTIC / EUR M&CS. Nous accueillerons à cette occasion Ulrik Buchholtz, chercheur à l’Université de Nottingham, pour une présentation à la frontière des mathématiques fondamentales et de l’informatique théorique.
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.
Informations pratiques
- Date : Jeudi 23 avril 2026
- Heure : 14h00
- Lieu : Salle B405 du LAGA (Université Sorbonne Paris Nord)
Vous ne pouvez pas vous déplacer ?
Le séminaire sera accessible en direct via l’outil de visioconférence à ce lien : https://bbb.math.univ-paris13.fr/b/chr-hyw-0rb-jz4
Pour en savoir plus sur les travaux d’Ulrik Buchholtz, visitez sa page personnelle.