Colloquium MathSTIC / EUR M&CS

Le jeudi 23 avril 2026 à 14h
Lieu: Salle B405 du LAGA
Possibilité de suivre en visio: https://bbb.math.univ-paris13.fr/b/chr-hyw-0rb-jz4

Lien de la rediffusion : https://bbb.math.univ-paris13.fr/playback/presentation/2.3/260aa433e092cf0e79b317a48abfe4178f8bd499-1776945086393

• To watch the video in full screen, click on this icon :

Ulrik Buchholz
Université de Nottingham
https://ulrikbuchholtz.dk/

The infinity-category of infinity-categories in simplicial type theory

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. Univalent foundations should be an ideal setting for doing model-independent higher category theory. However, it’s still an open problem whether HoTT can define the infinity-groupoid of infinity-categories.

Riehl and Shulman proposed an extension of HoTT, called simplicial type theory (STT), where the basic objects are simplicial infinity-groupoids. I will explain and motivate simplicial type theory, along with an extension that allows us to define the infinity-category of infinity-categories. The latter part is based on joint work with Daniel Gratzer and Jonathan Weinberger.