Internal languages of locally cartesian closed $(\infty,1)$-categories
El Mehdi Cherradi
公開日: 2025/9/3
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.