Sets in homotopy type theory

Abstract

Homotopy Type Theory may be seen as an internal language for the $\infty$-category of weak $\infty$-groupoids which in particular models the univalence axiom. Voevodsky proposes this language for weak $\infty$-groupoids as a new foundation for mathematics called the Univalent Foundations of Mathematics. It includes the sets as weak $\infty$-groupoids with contractible connected components, and thereby it includes (much of) the traditional set theoretical foundations as a special case. We thus wonder whether those `discrete' groupoids do in fact form a (predicative) topos. More generally, homotopy type theory is conjectured to be the internal language of `elementary' $\infty$-toposes. We prove that sets in homotopy type theory form a $\Pi W$-pretopos. This is similar to the fact that the $0$-truncation of an $\infty$-topos is a topos. We show that both a subobject classifier and a $0$-object classifier are available for the type theoretical universe of sets. However, both of these are large and moreover, the $0$-object classifier for sets is a function between $1$-types (i.e. groupoids) rather than between sets. Assuming an impredicative propositional resizing rule we may render the subobject classifier small and then we actually obtain a topos of sets.

References in corpus (5)

• Higher Topos Theory
• Univalent categories and the Rezk completion
• Elementary quotient completion
• Experimental library of univalent formalization of mathematics
• A preliminary univalent formalization of the p-adic numbers

Cited by in corpus (8)

• Modalities in homotopy type theory
• Topological Quantum Gates in Homotopy Type Theory
• Synthetic topology in Homotopy Type Theory for probabilistic programming
• On Small Types in Univalent Foundations
• Uniform Elgot Iteration in Foundations
• The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations
• Intrinsically Correct Sorting in Cubical Agda
• On Generalized Ordered Sets: A constructive development