First of all, in case anyone missed it, Chris Kapulkin recently wrote a guest post at the n-category cafe summarizing the current state of the art regarding “homotopy type theory as the internal language of higher categories”.

I’ve just posted a preprint which improves that state a bit, providing a version of “Lang(C)” containing univalent strict universes for a wider class of (∞,1)-toposes C:

• Univalence for inverse EI diagrams

Previously our collection of such models included the following two examples:

1. Slice (∞,1)-categories of ∞Gpd, obtained from slices of the model category of simplicial sets. Here the universes can be obtained simply by pullback to the appropriate slice. (In type theory, this just means working in a nonempty context.) Just as in ordinary category theory, in higher category theory we have , so these give us models in (∞,1)-toposes of diagrams on any ∞-groupoid.
2. Diagrams of ∞-groupoids indexed by inverse 1-categories. These are a sort of “well-founded diagram” which enables us to build universes inductively step-by-step.

The idea of this paper is that we should be able to combine these models. Essentially, we build universes inductively as in an inverse diagrams model, but each step of the induction is a slice category. This results in diagrams indexed by something I’m calling “inverse EI (∞,1)-categories”, which are like inverse categories except that they can contain nontrivial automorphisms (and higher automorphisms). The terminology comes from the classical notion of “EI category”, which is one in which all Endomorphisms are Isomorphisms; these are a generalization to the ∞-case but with a well-foundedness restriction.

I had this thought over a year ago, and with the idea in hand, working out the details was fairly straightforward. There are several reasons it took me so long. One is named Arthur and just turned two years old last month. Another is that along the way I got caught up in a spin-off project. But the most important is that I got stuck — not in constructing the new models of type theory, but in proving that they model the desired (∞,1)-categories!

There are by now a lot of models for (∞,1)-categories and diagrams on them, but it turns out that the one I needed didn’t quite exist yet. The indexing object that most naturally falls out of this approach is an internal category in simplicial sets, and until last year these had not been shown to admit a model structure presenting the theory of (∞,1)-categories. In fact, I myself had wondered about that for quite unrelated reasons; and last March Geoffroy Horel proved it. It turns out to be quite subtle! The basic idea (non-model-category-enthusiasts can skip to the next paragraph now) is to lift the complete-Segal-space model structure along the nerve functor to bisimplicial sets; but instead of Rezk’s complete-Segal-space model structure that is a localization of the Reedy (i.e. injective) model structure, Horel has to use an analogous one that localizes the projective model structure on bisimplicial sets.

Horel had also constructed a model structure on the category of internal presheaves over an internal category in simplicial sets, which it was easy to compare mine to. But what remained was to connect this model structure to some previously-known model category for (∞,1)-presheaves, to show that it has the right homotopy theory. Geoffroy and I went back and forth with several ideas, but nothing seemed to work easily. Finally, a couple months ago I learned that Pedro Boavida de Brito had constructed a “Grothendieck construction” relating internal presheaves on internal categories to an appropriate model structure of “left fibrations” over complete Segal spaces (the latter I had also heard of several years earlier from Charles Rezk, but has still never been published). He and I were then able to work out how to relate the latter to left fibrations over quasicategories or to enriched diagrams on simplicially enriched categories. His paper is not yet available, but he gave me permission to cite it forwards in my preprint.

There are a few reasons I think this result is interesting. One is, of course, that we still don’t know whether all (∞,1)-toposes model type theory with univalent strict universes, so any progress in this direction is nice. Another is that classical equivariant algebraic topology is in fact equivalent to the homotopy theory of diagrams on some inverse EI (∞,1)-category — as long as the group of equivariance is compact Lie! (I always wondered, when hearing about equivariant homotopy theory as a graduate student, why compact Lie groups seemed to make certain things better-behaved. These models may or may not have anything to do with any of the advantages of compact Lie groups that equivariant homotopy theorists are familiar with, but it’s intriguing that the same condition arises.) Thus, synthetic homotopy theory can be used (modulo the expected initiality theorem) to prove things about equivariant homotopy theory, which is a notoriously difficult subject.

Finally, I believe this is the first model for univalence involving a model category that is cooked up expressly for the purpose. Voevodsky’s original model used Quillen’s model category of simplicial sets, and my earlier models in inverse diagrams and elegant Reedy presheaves used the Reedy model structure due to Reedy and Kan. But the model categories that I ended up with in this paper seem to be new; they have a Reedy flavor (thinking about this led to the spin-off work I mentioned above) but I have not seen them anywhere else. (In higher category theory language, they are an intriguing mixture of “algebraic” and “non-algebraic”: the automorphisms act non-algebraically, while the noninvertible maps act algebraically.) This gives me some hope that the general problem may be solvable: so far we haven’t managed to build univalent universes in existing model categories such as injective simplicial presheaves, but maybe somewhere out there there are different model categories that are better-adapted to modeling type theory.

Unfortunately, I don’t see any useful way of directly generalizing the construction in this paper; it still seems very closely tied to the well-founded-induction inverse-category philosophy. I guess there is some hope that it might generalize to a sort of “elegant generalized-Reedy (∞,1)-category”, but so far I have not managed to make anything like that work.