Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

April 17, 2019

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 (,1)(\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 (,1)(\infty,1)-toposes: the object classifiers of an (,1)(\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 (,1)(\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 (,1)(\infty,1)-toposes can be presented by (what varieties of) cubical sets.
  • The (,1)(\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 (,1)(\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 (,1)(\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.
Posted at April 17, 2019 12:35 AM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/3106

2 Comments & 0 Trackbacks

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? ;)

Posted by: Emily Riehl on April 17, 2019 4:33 PM | Permalink | Reply to this

Re: Univalence in (∞,1)-toposes

Thanks. I may talk about it at CT 2019 as you suggest; we’ll see. I’ll definitely talk about it at HoTT 2019, though.

Posted by: Mike Shulman on April 21, 2019 2:17 AM | Permalink | Reply to this

Post a New Comment