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

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öf type theory with dependent sums, intensional identity types, and dependent products satisfying functional extensionality is the internal language of locally cartesian closed $(\mathrm{\infty },1)$-categories.