### Univalence in (∞,1)-toposes

#### Posted by Mike Shulman

It’s been believed for a long time that homotopy type theory should be an “internal logic” for $(\infty,1)$-toposes, in the same way that higher-order logic (or extensional type theory) is for 1-toposes. Over the past decade a lot of steps have been taken towards realizing this vision, but one important gap that’s remained is the construction of sufficiently strict universe objects in model categories presenting $(\infty,1)$-toposes: the object classifiers of an $(\infty,1)$-topos correspond directly only to a kind of “weakly Tarski” universe in type theory, which would probably be tedious to use in practice (no one has ever seriously tried).

Yesterday I posted a preprint that closes this gap (in the cases of most interest), by constructing strict univalent universe objects in a class of model categories that suffice to present all Grothendieck $(\infty,1)$-toposes. The model categories are, perhaps not very surprisingly, left exact localizations of injective model structures on simplicial presheaves, which were previously known to model all the rest of type theory; the main novelty is a new more explicit “algebraic” characterization of the injective fibrations, enabling the construction of universes.

I don’t have time to write a long blog post today, but if you want a longer and more detailed overview you can just check out the chatty 7-page introduction to the paper, or the slides from my talk about it at last month’s Midwest HoTT seminar. Let me just note here some important points:

- The metatheory is ZFC plus as many inaccessible cardinals as we want universes.
- The type theory is Book HoTT, with univalence as an axiom.
- The model categories are simplicial, not cubical. It’s possible that similar methods would work cubically, but cubical sets are less well-studied in model category theory, and it’s not yet known what $(\infty,1)$-toposes can be presented by (what varieties of) cubical sets.
- The $(\infty,1)$-toposes are Grothendieck, not elementary, although the techniques might prove useful for the elementary case (e.g. via a Yoneda embedding).
- We only construct an interpretation of type theory into $(\infty,1)$-toposes, not the “strong internal language conjecture” that a “homotopy theory of type theories” is
*equivalent*to the homotopy theory of some flavor of elementary $(\infty,1)$-topos — although again, the same techniques might prove useful for the latter. - The initiality principle is not addressed; it remains as open or as solved as you previously believed it to be.
- The main remaining semantic open problem is constructing higher inductive types in such a way that the universes are closed under them. I am optimistic about this and have some ideas; in particular, it’s possible that some of the ideas used in cubical models could be adapted to the simplicial case.

## Re: Univalence in (∞,1)-toposes

Congratulations Mike! I can’t wait to read the paper.

I don’t suppose I can entice you to speak about this theorem this summer? ;)