Internal languages of locally cartesian closed (∞,1)-categories

2025/09/03 by El Mehdi Cherradi, Cherradi, El Mehdi
Mathematics · #Advanced Topology and Set Theory #Algebraic Topology (math.AT) #Algebraic structures and combinatorial models #Category Theory (math.CT) #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic (math.LO)

paper · pdf · doi:10.48550/arxiv.2509.03371

openalex publication_date 2025/09/03 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

We establish a DK-equivalence between the relative category of π-tribes and the relative category of locally cartesian closed quasicategories. From this follows one of the internal languages conjecture: Martin-Löf type theory with dependent sums, intensional identity types, and dependent products satisfying functional extensionality is the internal language of locally cartesian closed (∞,1)-categories.

Citations

• Interpreting type theory in a quasicategory: a Yoneda approach
• Parametricity and Semi-Cubical Types
• Homotopical inverse diagrams in categories with attributes
• Notes on Clans and Tribes
• The homotopy theory of type theories

Related

• The internal languages of univalent categories
• Internal Languages of Finitely Complete (∞, 1)-categories
• The internal Yoneda lemma for locally Cartesian closed ∞-categories
• Interpreting type theory in a quasicategory: a Yoneda approach
• The homotopy theory of type theories