2025/12/21 by Apol, Daniël, Petrowitsch, Maximilian
Computer Science · Mathematics · #Advanced Topology and Set Theory #Algebraic Topology (math.AT) #Category Theory (math.CT) #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic (math.LO) #Logic, programming, and type systems
paper · doi:10.48550/arxiv.2512.18891
openalex publication_date 2025/12/21 · openalex created_date 2025/12/24 · openalex updated_date 2026/07/28
We prove that every categorical model of dependent type theory with dependent sums and products, intensional identity types and univalent universes presents via its ∞-localisation an elementary ∞-topos, that is, a finitely complete, locally cartesian closed ∞-category with enough univalent universal morphisms. We also show that elementary ∞-toposes have small subobject classifiers and that the ∞-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.