Sets in homotopy type theory

Egbert Rijke, Bas Spitters

Publikation: Bidrag til tidsskrift/Konferencebidrag i tidsskrift /Bidrag til avisTidsskriftartikelForskningpeer review

12 Citationer (Scopus)

Abstract

Homotopy type theory may be seen as an internal language for the ∞-category of weak ∞-groupoids. Moreover, weak ∞-groupoids model the univalence axiom. Voevodsky proposes this (language for) weak ∞-groupoids as a new foundation for Mathematics called the univalent foundations. It includes the sets as weak ∞-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' of ∞-toposes. We prove that sets in homotopy type theory form a ΠW-pretopos. This is similar to the fact that the 0-truncation of an ∞-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.

OriginalsprogEngelsk
TidsskriftMathematical Structures in Computer Science
Vol/bind25
Nummer5
Sider (fra-til)1172-1202
Antal sider31
ISSN0960-1295
DOI
StatusUdgivet - 30 jun. 2015

Fingeraftryk

Dyk ned i forskningsemnerne om 'Sets in homotopy type theory'. Sammen danner de et unikt fingeraftryk.

Citationsformater