Colloquium MathSTIC / EUR M&CS

Thursday 23 April 2026 at 2.00 pm
Venue: Room B405, LAGA
Available to watch online: https://bbb.math.univ-paris13.fr/b/chr-hyw-0rb-jz4

Link to the replay : 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
University of 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.