All (infty,1)-toposes have strict univalent universes
read the original 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.
This paper has not been read by Pith yet.
Forward citations
Cited by 5 Pith papers
-
Univalence without function extensionality
Categorical univalence of a universe does not entail function extensionality, as shown by polynomial models of type theory that refute the latter while satisfying the former.
-
Constructive higher sheaf models with applications to synthetic mathematics
Constructive higher sheaf models of type theory with univalence and higher inductive types are constructed to underpin synthetic mathematics.
-
Elementary $\infty$-toposes from type theory
Categorical models of dependent type theory with sums, products, identity types and univalent universes present elementary ∞-toposes via ∞-localization, which also possess small subobject classifiers.
-
Constructive higher sheaf models with applications to synthetic mathematics
Develops constructive higher sheaf models of type theory to support synthetic mathematics with univalence and higher inductive types.
-
From Copying to Corelations via Ancestry Partitions
Establishes that the ancestry quotient of the free binary PROP is equivalent as a PROP to the PROP for non-counital cocommutative comonoids.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.