Elementary $\infty$-toposes from type theory

Abstract

We prove that every categorical model of dependent type theory with dependent sums and products, intensional identity types and univalent universes presents via its $\infty$-localisation an elementary $\infty$-topos, that is, a finitely complete, locally cartesian closed $\infty$-category with enough univalent universal morphisms. We also show that elementary $\infty$-toposes have small subobject classifiers and that the $\infty$-localisation admits finite colimits if the type theory has 0-types and pushout types. To achieve this, we extend Joyal's theory of tribes by introducing the notion of a univalent tribe and a univalent fibration in a tribe.