Elementary $\mathrm{\infty }$-Toposes from Type Theory

Since its conception, it has been speculated that Homotopy Type Theory (HoTT) [7] is the internal language of particular higher categories also called elementary $\mathrm{\infty }$-toposes. A precise formulation of this statement was given by Kapulkin and Lumsdaine in [3, Conj. 3.7] and is known as the internal language conjecture. Here, HoTT is understood as Martin-Löf dependent type theory with dependent sums, dependent products, intensional identity types and univalent universes.

The conjecture fits into a series of important steps that have been made so far towards establishing such a connection between higher categories and type theory. Kapulkin and Szumiło [4] showed that dependent type theory with intensional identity types is the internal language of finitely complete $\mathrm{\infty }$-categories. Assuming in addition dependent products, Kapulkin [2] proved that every model presents a locally cartesian closed $\mathrm{\infty }$-category. Shulman [6] showed that HoTT can be interpreted as internal language into any Grothendieck $\mathrm{\infty }$-topos.

Proving a correspondence between HoTT and elementary $\mathrm{\infty }$-toposes is currently an open problem. Elementary $\mathrm{\infty }$-toposes are supposed to generalise both Grothendieck $\mathrm{\infty }$-toposes and ordinary 1-toposes. There is currently no generally agreed upon definition of an elementary $\mathrm{\infty }$-topos, even though there has been increasing interest in the topic in the last decade. We define an elementary $\mathrm{\infty }$-topos as a finitely complete, locally cartesian closed $\mathrm{\infty }$-category with enough univalent morphisms. In its precise statement, the internal language conjecture then asserts that there is a Dwyer-Kan equivalence ${\mathrm{Cl}}_{\mathrm{\infty }}:{\mathrm{𝐂𝐱𝐥𝐂𝐚𝐭}}_{\mathrm{𝙷𝚘𝚃𝚃}}\stackrel{\sim }{\to }{\mathrm{𝐄𝐥𝐓𝐨𝐩}}_{\mathrm{\infty }}$ between the category of categorical models of HoTT and the category of elementary $\mathrm{\infty }$-toposes, induced by sending each model to its $\mathrm{\infty }$-localisation at the class of homotopy equivalences. Proving that this functor exists, i.e. that the $\mathrm{\infty }$-localisation takes values in ${\mathrm{𝐄𝐥𝐓𝐨𝐩}}_{\mathrm{\infty }}$, and showing that this is a Dwyer-Kan equivalence has so far been an open problem.

In the talk, we will present the work [5] in which we prove the existence of this functor ${\mathrm{Cl}}_{\mathrm{\infty }}$, a first step towards proving the conjecture. That is, we show that every model of HoTT presents an elementary $\mathrm{\infty }$-topos via its $\mathrm{\infty }$-localisation. First, we use the fact that every model of HoTT has the structure of a tribe in the sense of Joyal [1]. We extend Joyal’s theory of tribes by introducing the notion of a univalent fibration in a tribe and the notion of a univalent tribe and we show that every categorical model of HoTT is such a univalent tribe. Then, we prove that every univalent tribe presents via its $\mathrm{\infty }$-localisation an elementary $\mathrm{\infty }$-topos inducing finite colimits and a subobject classifier under the presence of pushout types and propositional resizing. Thus, the functor ${\mathrm{Cl}}_{\mathrm{\infty }}$ can be obtained as a composite: ${\mathrm{𝐂𝐱𝐥𝐂𝐚𝐭}}_{\mathrm{𝙷𝚘𝚃𝚃}}\to \mathrm{𝐔𝐧𝐢𝐯𝐓𝐫𝐛}\to {\mathrm{𝐄𝐥𝐓𝐨𝐩}}_{\mathrm{\infty }}.$