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 -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 -toposes: the object classifiers of an -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 -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 -toposes can be presented by (what varieties of) cubical sets.
- The -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 -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 -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? ;)