Elementary $\mathrm{\infty }$-toposes from type theory

We prove that every categorical model of dependent type theory with dependent sums and products, intensional identity types and univalent universes presents via its $\mathrm{\infty }$-localisation an elementary $\mathrm{\infty }$-topos, that is, a finitely complete, locally cartesian closed $\mathrm{\infty }$-category with enough univalent universal morphisms. We also show that elementary $\mathrm{\infty }$-toposes have small subobject classifiers. 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.