arXiv · 2509.03371
Internal languages of locally cartesian closed $(\infty,1)$-categories
Abstract
We establish a DK-equivalence between the relative category of $\pi$-tribes and the relative category of locally cartesian closed quasicategories. From this follows one of the internal languages conjecture: Martin-L\"of type theory with dependent sums, intensional identity types, and dependent products satisfying functional extensionality is the internal language of locally cartesian closed $(\infty,1)$-categories.
Explore related subjects
Keep this discovery
El Mehdi Cherradi. 2025-09-03. Internal languages of locally cartesian closed $(\infty,1)$-categories. https://arxiv.org/abs/2509.03371
Cite the original work for its findings. Save a collection to share your selection of sources.