  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.

Category Theory;Logic in Computer Science