An Algebraic Folk Model Structure for Internal Categories
Date:
Quillen model categories provide an abstract framework in which to do homotopy theory. A key example is the folk model structure on $\mathbf{Cat}$, for which the notion of homotopy is that of equivalences of categories. The construction of this model structure requires the axiom of choice, meaning that groupoidal models of type theory which exploit the structure of the trivial cofibrations are not constructive. In analogy to work by Gambino, Henry, Sattler and Szumiło on the effective model structure on simplicial objects in a lextensive category, we construct a model structure on internal categories that does not require the axiom of choice; when we consider categories internal to $\mathbf{Set}$ and assume the axiom of choice, this recovers the folk model structure on $\mathbf{Cat}$. Moreover, we prove that this forms an algebraic model structure whose underlying ordinary model structure turns out to recover Everaert, Kieboom and Van de Linden’s folk model structure on internal categories equipped with the trivial topology. Restricting this construction to a model structure on internal groupoids, the extra algebraicity provides us with a constructive model of Martin-Löf Type Theory due to the type-theoretic algebraic weak factorisation systems of Gambino and Larrea. In this talk, I will introduce the construction of this algebraic model structure and some related ideas.
