Sets in homotopy type theory

[Bas Spitters]

We just put the following on the arxiv. Those of you reading/writing
the book, will notice quite some overlap with what is in the set
theory chapter.

Sets in homotopy type theory
Egbert Rijke, Bas Spitters

Homotopy Type Theory may be seen as a language for the category of
weak oo-groupoids. Voevodsky proposes weak oo-groupoids as a new
foundation for mathematics called the univalent foundations. It
includes the sets as weak oo-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 oo-toposes. Similar to the fact that the
0-truncation of an oo-topos is a topos, we prove in our type
theoretical setting: sets in homotopy type theory form a PiW-pretopos.
The type theoretical universe of sets has a a subobject classifier as
well as a 0-object classifier, itself being a groupoid. Both of these
are large; assuming certain resizing rules we actually obtain a topos.
We also discuss the axiom of multiple choice.

http://arxiv.org/abs/1305.3835