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.

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

References in corpus (27)

• Sheafifiable homotopy model categories
• A 2-categories companion
• Understanding the small object argument
• The identity type weak factorisation system
• Simplicial structures on model categories and functors
• The Simplicial Model of Univalent Foundations (after Voevodsky)
• Algebraic weak factorisation systems I: accessible AWFS
• Homotopy limits and colimits and enriched homotopy theory
• Units of ring spectra and Thom spectra
• Homotopy-theoretic aspects of 2-monads
• Algebraic model structures
• Two-Level Type Theory and Applications
• The Frobenius Condition, Right Properness, and Uniform Fibrations
• Fibrations and homotopy colimits of simplicial sheaves
• On the homotopy groups of spheres in homotopy type theory
• The homotopy theory of type theories
• Computational Higher Type Theory I: Abstract Cubical Realizability
• Goodwillie's Calculus of Functors and Higher Topos Theory
• Computational Higher Type Theory II: Dependent Cubical Realizability
• A model structure on internal categories in simplicial sets
• Algebraic Type Theory and Universe Hierarchies
• A Theory of Elementary Higher Toposes
• On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory
• Internal sizes in $\mu$-abstract elementary classes
• Universes for category theory
• Nilpotent Types and Fracture Squares in Homotopy Type Theory
• On lifting univalence to the equivariant setting

Cited by in corpus (8)

• Towards a constructive simplicial model of Univalent Foundations
• Nilpotent Types and Fracture Squares in Homotopy Type Theory
• Proper Orbifold Cohomology
• On the Nielsen-Schreier Theorem in Homotopy Type Theory
• Filter Quotients and Non-Presentable $(\infty ,1)$-Toposes
• Synthetic fibered $(\infty ,1)$-category theory
• Yoneda's lemma for internal higher categories
• Univalence in Higher Category Theory