The n-Category Café

Mike posted on the HoTT blog about his paper shortly after it appeared, so I will not be summarizing it again, but let me mention that we now know many models of the Univalence Axiom, although there is still way more to be done.

Peter and I tried to answer the question: what is the right notion of a weak equivalence between type theories? You can think of two different answers to this question, depending on the background you came to HoTT with. If you are more logically-minded, you would think of properties such conservativity and bi-interpretatibility, and indeed, these motivate one of our definitions: a weak equivalence of theories is a translation that allows lifting of types up to equivalence and terms up to propositional equality (Def. 3.1 in the linked paper). If on the other hand, you are a homotopy theorist and you know that each (intensional) type theory has a classifying fibration category, then you would expect that a weak equivalence will be a map between theories that induces an equivalence of the underlying fibration categories. Now here is a great thing about HoTT: these two notions coincide (Prop. 3.3)!

So since a category with weak equivalences is just a presentation of an $\infty$-category (or a homotopy theory), we obtain several $\infty$-categories of type theories: $\mathrm{Th}_{\mathrm{Id},\Sigma}$ of type theories with $\mathrm{Id}$-types and dependent sums, $\mathrm{Th}_{\mathrm{Id},\Sigma, \Pi}$ of those that also carry dependent product structure and yet-to-be-defined $\mathrm{Th}_{\mathsf{HoTT}}$. We next construct functors from these $\infty$-categories to various $\infty$-categories of $\infty$-categories. And thus there are maps $\mathrm{Th}_{\mathrm{Id},\Sigma} \to \mathrm{Lex}_\infty$ ($\infty$-categories with finite limits), $\mathrm{Th}_{\mathrm{Id},\Sigma, \Pi} \to \mathrm{LCCC}_\infty$ (locally cartesian closed $\infty$-categories), and conjecturally $\mathrm{Th}_{\mathsf{HoTT}} \to \mathrm{ElTop}_\infty$ (elementary $\infty$-toposes). We conjecture that these functors are $\infty$-equivalences (see Sec. 3). At that point, neither $\mathrm{Th}_{\mathsf{HoTT}}$ nor $\mathrm{ElTop}_\infty$ was a well-defined concept, so in this case our conjecture was really only a conjectural conjecture (joke credit: Tom Hales’ talk at Big Proof). (Note to experts: to be independent of the Initiality Conjecture, we formulated everything in the language of contextual categories instead, but one ultimately wants the conjectures to hold for syntactically-presented type theories.)

We then move on to equip both $\mathrm{Th}_{\mathrm{Id},\Sigma}$ and $\mathrm{Th}_{\mathrm{Id},\Sigma, \Pi}$ with a left semi-model structure. I won’t spell out the details here, but the construction itself feels really natural to me. All classes of maps have explicit description and in fact ended up being exactly our first guesses. And all the nice things that you could ask for hold in our setting. For instance, the cofibrant type theories (which should be thought of as the free ones) end up being precisely the theories that are extensions by types and terms, without any equations.

A few months later, Mike gave a tentative definition of an elementary $\infty$-topos, thus making our conjectural conjecture less conjectural. Mike blogged about this definition and his post led to some interesting exchanges in the comments, so I encourage you to take a look if you haven’t yet. During the HoTT MRC, Jonas Frey, Tamara von Glehn, Nima Rasekh, Inna Zakharevich worked with this definition, trying to prove analogues of some results from $1$-topos theory, including: stability under gluing and redundancy of including existence of finite colimits in the axioms. Their results constitute a basis of the theory of elementary $\infty$-toposes and I hope they will appear soon.

Once these conjectures were properly formulated, Karol and I decided to attack the first one of them, i.e. the equivalence $\mathrm{Th}_{\mathrm{Id},\Sigma} \simeq \mathrm{Lex}_\infty$. One can decompose the functor $\mathrm{Th}_{\mathrm{Id},\Sigma} \simeq \mathrm{Lex}_\infty$ into a composite:

$\mathrm{Th}_{\mathrm{Id},\Sigma} \to \mathrm{Trb} \to \mathrm{FibCat} \to \mathrm{Lex}_\infty$

where $\mathrm{Trb}$ is the category of tribes (which are models of type theory studied by Joyal) and $\mathrm{FibCat}$ is the category of fibration categories (in the sense of Brown). Why is it something desirable? First, tribes are very closely related to comprehension categories, a well-studied notion of a model for type theory, and we prove in the paper that the $\infty$-category of comprehension categories with $\mathrm{Id}$- and $\Sigma$-types is equivalent to that of tribes. Second, Karol had previously proven that the map $\mathrm{FibCat} \to \mathrm{Lex}_\infty$ is an equivalence. Thus in order to relate comprehension categories and $\infty$-categories, one needs to show an equivalence between tribes and fibration categories.

And although both of these notions feel really similar, this is not an easy task! Our initial idea was to construct a functor $\mathrm{FibCat} \to \mathrm{Trb}$ and show that both composites are weakly equivalent to identity functors. There is a canonical way of doing it, namely by taking a fibration category to the tribe of representable $\infty$-presheaves on it, which can be realized on the $1$-categorical level in many ways, but we couldn’t make any of them strictly $1$-functorial (or even weakly in any well-defined and useful sense). The second thought was to use Waldhausen’s Approximation Properties (Def. 2.8 + Thm. 2.9 in the linked paper), which is a criterion for equivalence of fibration categories, similar to the criterion for Quillen equivalence in terms of adjoint transposes of weak equivalences. And although our inverse-on-objects construction would be sufficient here, the Approximation Properties require the fibration category structure on the categories $\mathrm{Trb}$ and $\mathrm{FibCat}$. The latter had been previously constructed by Karol, but there seem to be fundamental obstacles to the existence of such a structure on the category of tribes. Indeed, tribes are in some sense more rigid than fibration categories and what we would consider a natural candidate for a path object in $\mathrm{Trb}$ did not satisfy the necessary conditions.

So what did we do in the end? We considered semi-simplicially enriched versions of both fibration categories and tribes (Def. 3.1 and 3.2) and showed that they both carry the fibration category structure (which required a slight modification of Karol’s previous results, see Sec. 4). Then, by explicitly constructing inverses, we proved that they are in fact equivalent to their respective unenriched analogues (Prop 3.12). Finally, we verified that the functor from semi-simplicial tribes to semi-simplicial fibration categories satisfies the Approximation Properties, and so the result now follows by 2-out-of-3. Oh, and in order to verify the Approximation Properties for the enriched version, we first check it for the unenriched version, so it’s really easy to get confused. Btw our notion of a semi-simplicial tribe was inspired by Joyal’s theory of simplicial tribes, but we had to modify the enriching category to ensure the equivalence between the enriched and the unenriched setting.

That’s what out there right now. So… what’s next? Last summer, Simon Cho, Cory Knapp, Clive Newstead, and Liang Ze Wong worked on comparing different categories of models of type theory, including contextual categories, categories with attributes, and comprehension categories. Hopefully they will bridge the gap between comprehension categories and contextual categories left by Karol and myself.

One should also try attacking the second conjecture, although it is going to be a much harder task. The main difficulty is that there is no known presentation, via some $1$-categories with extra structure, of locally cartesian closed $\infty$-categories, and so one would need to compare $\pi$-tribes (a.k.a. type-theoretic fibration categories) with locally cartesian closed $\infty$-categories directly. Another thing to look into are new models of the Univalence Axiom following a series of papers by Mike, since we still don’t know too many such models.