Elementary $\infty$-toposes from type theory

TL;DR

This paper demonstrates that models of dependent type theory with certain features can be presented as elementary ∞-toposes, enriching the understanding of their categorical structures.

Contribution

It introduces the concept of univalent tribes and extends Joyal's tribes theory to connect type theory models with elementary ∞-toposes.

Findings

Every model with specified type-theoretic features presents an elementary ∞-topos.

Elementary ∞-toposes possess small subobject classifiers.

Extension of Joyal's tribes theory via univalent tribes and fibrations.

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. 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.