Internal language conjecture for locally cartesian closed infinity-categories

Let $\mathbf{CompCat}_{\Sigma, \Pi_\text{ext}, \text{Id}}$ be the category of models of intensional Martin–Löf type theory with dependent sums, extensional dependent products, and identity types, and let $\mathbf{QCat}_{lcc}$ be the category of locally cartesian closed quasicategories. The functor

$$\mathbf{Ho}_\infty: \mathbf{CompCat}_{\Sigma, \Pi_\text{ext}, \text{Id}} \to \mathbf{QCat}_{lcc}$$

assigning to a model its underlying quasicategory is a DK-equivalence. This conjecture asserts that the internal language of locally cartesian closed quasicategories is a dependent type theory with dependent sums, extensional dependent products, and intensional identity types. The paper states that its goal is to establish this conjecture, so the claim is resolved by the results of the paper.