All $(\infty ,1)$-toposes have strict univalent universes

Abstract

We prove the conjecture that any Grothendieck $(\infty ,1)$-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can be used as a formal language for reasoning internally to $(\infty ,1)$-toposes, just as higher-order logic is used for 1-toposes. As part of the proof, we give a new, more explicit, characterization of the fibrations in injective model structures on presheaf categories. In particular, we show that they generalize the coflexible algebras of 2-monad theory.

71 pages. v2: fixed some typos, added a few remarks

References in corpus (4)

• The identity type weak factorisation system
• Homotopy limits and colimits and enriched homotopy theory
• Units of ring spectra and Thom spectra
• Algebraic Type Theory and Universe Hierarchies

Cited by in corpus (2)

• Proper Orbifold Cohomology
• Univalence in Higher Category Theory