| dc.description.abstract | Homotopy Type Theory (HoTT) is a formal system for constructive mathematical reasoning. The Univalent Foundations (UF) program enhances HoTT with the Univalence Axiom and Higher Inductive Types (HITs), proposing it as an alternative to ZFC for the foundations of mathematics. My thesis focuses on the categorical semantics of UF.
The semantics of the elimination principle of the identity type correspond to lifting properties, a fundamental component of model categories, which serve as an abstract framework for homotopy theory. In 2013, it was demonstrated that Kan Complexes, or equivalently $\infty$-groupoids, can support a model of UF. These findings suggest a profound connection between logic and homotopy theory / higher category theory. Over the past decade, numerous attempts have been made to expand on these results.
In my thesis, I investigate two ways in which models of HoTT relate to higher categories. The primary link is $\tl{Ho}_{\infty}(-)$, which produces a homotopy $\infty$-category of a category with weak equivalences (and perhaps additional structure). Using an incarnation of $\tl{Ho}_{\infty}(-)$, one can simultaneously introduce and characterize $(\infty,1)$-topoi in two models for higher categories.
We showcase three main results. The first starts with a type theory obeying certain rules and produces a locally cartesian closed $\infty$-category. The second and third state, that every $\infty$-topos, (respectively presentable and locally cartesian closed $\infty$-category) can be presented by a model category that models univalent HoTT (respectively HoTT+FunExt). We also prove that two of these constructions are compatible in a certain sense. | |
