Peter LeFanu Lumsdaine: Type theories as internal languages for (∞,1)-categories

Abstract

Since the beginnings of HoTT, it’s been expected that variants of Martin-Löf’s Intensional Type Theory (ITT) should provide internal languages for suitable (∞,1)-categories, analogously to how Extensional Type Theory provides internal languages for locally cartesian closed categories. Even stating this precisely, however, is non-trivial: it should assert that some kind of ∞-category of theories in ITT is equivalent, in some suitable sense, to some ∞-category of suitably-structured ∞-categories.

In the paper [KL2018], Chris Kapulkin and I set up two precise conjectures of this form, using the machinery of fibration categories to present the ∞-categories of type theories involved. The first of these conjectures states that ITT with just 1, Σ, and Id gives an internal language for (∞,1)-categories with finite limits; this was proven by Chris Kapulkin and Karol Szumiło in [KS2019]. The second conjecture states that ITT with 1, Σ, Id, and Π-types gives an internal language for locally cartesian closed (∞,1)-categories; a proof of this was recently announced by El Mehdi Cherradi in [Ch2025].

I plan to give several seminars this term presenting the details of the story outlined above. In the first, I will present the background and precise setup for these internal language conjectures, mostly following [KL2018].

• [KL2018] Chris Kapulkin, Peter LeFanu Lumsdaine, “The homotopy theory of type theories”, Adv. Math. 2018, https://doi.org/10.1016/j.aim.2018.08.003, https://arxiv.org/abs/1610.00037
• [KS2019] Chris Kapulkin, Karol Szumiło, “Internal languages of finitely complete (∞,1)-categories”, Selecta Math. 2019, https://doi.org/10.1007/s00029-019-0480-0, https://arxiv.org/abs/1709.09519
• [Ch2025] El Mehdi Cherradi, “Internal languages of locally cartesian closed (∞,1)-categories”, preprint 2025, https://arxiv.org/abs/2509.03371