Kerodon

Proof. We may assume without loss of generality that $n \geq 0$ (otherwise, the result follows immediately from the construction). For every morphism of simplicial sets $K \rightarrow \operatorname{\mathcal{D}}$, Remark 4.8.8.15 determines a comparison map

We will prove that each $\theta _{K}$ is an isomorphism of simplicial sets; Proposition 4.8.8.16 then follows by taking $K = \operatorname{\mathcal{D}}$. Note that the construction $K \mapsto \theta _{K}$ carries colimits (in the category of simplicial sets with a morphism to $\operatorname{\mathcal{D}}$) to limits (in the arrow category $\operatorname{Fun}( [1], \operatorname{Set_{\Delta }})$). By virtue of Remark 1.1.3.13, we can assume without loss of generality that $K$ is a standard simplex. Replacing $F$ by the projection map $K \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}}\rightarrow K$ and $\operatorname{\mathcal{D}}'$ by the fiber product $K \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{D}}'$, we are reduced to proving Proposition 4.8.8.16 in the special case where $\operatorname{\mathcal{D}}$ is a standard simplex: in particular, it is an $(n,1)$-category. In this case, $\operatorname{\mathcal{D}}'$ is also an $(n,1)$-category (Proposition 4.8.6.32), and we can identify $\mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}/\operatorname{\mathcal{D}})}$ with the homotopy $n$-category of $\operatorname{\mathcal{C}}$ (Example 4.8.8.11). Applying Proposition 4.8.4.7, we see that the horizontal maps in the commutative diagram

are isomorphisms. The desired result now follows by passing to fibers of the vertical maps. $\square$