Kerodon

Proof. Since $\operatorname{\mathcal{D}}$ is an $\infty $-category and the comparison map $G: \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}/\operatorname{\mathcal{D}})} \rightarrow \operatorname{\mathcal{D}}$ is an inner fibration (Proposition 4.8.8.14), the simplicial set $\mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}/\operatorname{\mathcal{D}})}$ is also an $\infty $-category (Remark 4.1.1.9). Fix an integer $m \leq n+1$; we wish to show that the functor $F'$ is $m$-full. For $n = -2$, there is nothing to prove. If $n = -1$, then $U'$ is surjective on objects (by construction) and therefore essentially surjective. We may therefore assume without loss of generality that $n \geq 0$. Since $U'$ is an inner fibration (Proposition 4.8.8.18), it will suffice to show that for every morphism $\Delta ^1 \rightarrow \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}})}$, the projection map $\Delta ^{1} \times _{ \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}})} } \operatorname{\mathcal{E}}\rightarrow \Delta ^1$ is $m$-full (Proposition 4.8.5.27. Using Remark 4.8.8.13, we can replace $F$ by the projection map $\Delta ^1 \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}}\rightarrow \Delta ^1$, and thereby reduce to the situation where $\operatorname{\mathcal{D}}= \Delta ^1$ is an $(n,1)$-category. In this case, the functor $F'$ exhibits $\mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}/\operatorname{\mathcal{D}})}$ as a homotopy $n$-category of $\operatorname{\mathcal{C}}$ (Example 4.8.8.11), so the desired result follows from Example 4.8.5.12. $\square$