From Filter Quotient Model Categories to Type Theory

Categorical logic is an area of category theory that uses categorical methods to construct and study models of various mathematical foundations, such as set theories and type theories. The idea is to construct categories whose objects axiomatically behave like sets or types, and then use the categorical structure to interpret the logical operations and axioms of the chosen foundation. We can use this approach to construct both standard and non-standard models of various foundations. One elegant way to construct non-standard models is via filter quotients of categories. It has, in particular, been used to construct models of set theory where the continuum hypothesis fails [1].

Here, for a given category $𝒞$ and a suitable poset of subterminal objects $\mathrm{\Phi }$ in $𝒞$, the filter quotient ${𝒞}_{\mathrm{\Phi }}$ is given as a filtered colimit ${\mathrm{colim}}_{U\in {\mathrm{\Phi }}^{op}}{𝒞}_{/U}$. This construction in particular comes with a projection functor $P_{\mathrm{\Phi }}:𝒞\to {𝒞}_{\mathrm{\Phi }}$, which preserves much of the structure of $𝒞$, hence preserving the property of being a model of a given foundation, resulting in new models.

In recent decades, we have seen the rise of homotopical foundations for mathematics, and in particular, various homotopy type theories (HoTT). Analogously, we have also witnessed the development of $\mathrm{\infty }$-categorical models of homotopy theory, proving that the $\mathrm{\infty }$-category of spaces and of sheaves on spaces are indeed models of HoTT. However, the study of non-standard models of HoTT via $\mathrm{\infty }$-categorical filter quotients has remained largely unexplored. Here, for a given $\mathrm{\infty }$-category $𝒞$ and a suitable poset $\mathrm{\Phi }$, the $\mathrm{\infty }$-categorical filter quotient is defined analogously as a filtered colimit of slice $\mathrm{\infty }$-categories ${𝒞}_{\mathrm{\Phi }}={\mathrm{colim}}_{U\in {\mathrm{\Phi }}^{op}}{𝒞}_{/U}$, which again comes with the projection functor $P_{\mathrm{\Phi }}:𝒞\to {𝒞}_{\mathrm{\Phi }}$ [2].

Constructing models of HoTT via $\mathrm{\infty }$-categories requires overcoming major technical challenges. Due to their syntactic nature, type theories are very strict, whereas $\mathrm{\infty }$-categories are inherently weak structures. One effective way to bridge this gap is to leverage model categories. Indeed, model categories are strict categories that nonetheless come with an underlying $\mathrm{\infty }$-category.

This approach breaks down the task into a two-step process. First, one constructs a suitable model category for a chosen $\mathrm{\infty }$-category. Then, one shows that the model category satisfies the conditions necessary to model HoTT. In the case of the $\mathrm{\infty }$-category of spaces, this has been realized via the Kan model structure on simplicial sets, whereas for $\mathrm{\infty }$-categories of sheaves (Grothendieck $\mathrm{\infty }$-topoi) this goal has been achieved via type-theoretic model topoi [3].

In this talk, I will show how this two-step approach can be extended to filter quotient $\mathrm{\infty }$-categories, resulting in new non-standard models of HoTT. More specifically, I show that many filter quotient $\mathrm{\infty }$-categories admit filter quotient model categories [4]. Moreover, I demonstrate that the projection functor $P_{\mathrm{\Phi }}$ preserves the property of being a model for HoTT, resulting in new non-standard models of HoTT [5, 6]. These non-standard models exhibit intriguing behaviors, such as non-standard natural numbers, that enrich our understanding of homotopical foundations.