Internal languages of locally cartesian closed $(\infty ,1)$-categories

Abstract

We establish a DK-equivalence between the relative category of $\ddot{I}€$-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 $(\infty ,1)$-categories.

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)