Internal languages of locally cartesian closed $(\infty,1)$-categories
Category Theory
2026-03-03 v2 Algebraic Topology
Logic
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\"of type theory with dependent sums, intensional identity types, and dependent products satisfying functional extensionality is the internal language of locally cartesian closed -categories.
Cite
@article{arxiv.2509.03371,
title = {Internal languages of locally cartesian closed $(\infty,1)$-categories},
author = {El Mehdi Cherradi},
journal= {arXiv preprint arXiv:2509.03371},
year = {2026}
}
Comments
v2; 41 pages, includes several corrections and information refactoring: parts of v1 have been made independent and expanded on separately (arXiv:2602.17347 and arXiv:2602.21083)