Kerodon

Proof. We first prove $(1)$. Assume that $F$ is a left fibration, and suppose we are given integers $0 \leq i < n$; we wish to show that every lifting problem

admits a solution. If $m \leq n+2$, then $\sigma _0$ can be lifted to a morphism $\Lambda ^{m}_{i} \rightarrow \operatorname{\mathcal{C}}$ (Remark 4.8.8.17), so the desired result follows from our assumption that $F$ is a left fibration. We may therefore assume that $m \geq n+3$. If $n = -2$, then $G$ is an isomorphism and there is nothing to prove. If $n = -1$, then $G$ identifies $\mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}/\operatorname{\mathcal{D}})}$ with a full simplicial subset of $\operatorname{\mathcal{D}}$, and the desired result follows from the observation that $\Lambda ^{m}_{i}$ contains every vertex of $\Delta ^ m$. We may therefore assume that $n \geq 0$. Replacing $F$ by the projection map $\Delta ^ m \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}}\rightarrow \Delta ^ m$, we can reduce to the case where $\operatorname{\mathcal{D}}= \Delta ^ m$ is a standard simplex. In this case, $\mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}/\operatorname{\mathcal{D}})}$ is an $(n,1)$-category (Example 4.8.8.11). In particular, it is an $(n+1)$-coskeletal simplicial set, so the lifting problem (4.88) has a unique solution (since $\Lambda ^{m}_{i}$ contains the $(n+1)$-skeleton of $\Delta ^ m$).

Assertion $(2)$ follows by applying $(1)$ to the opposite inner fibration $U^{\operatorname{op}}: \operatorname{\mathcal{C}}^{\operatorname{op}} \rightarrow \operatorname{\mathcal{D}}^{\operatorname{op}}$. Assertion $(3)$ follows by combining $(1)$ and $(2)$ with Example 4.2.1.5. It remains to prove $(4)$. Fix an object $Y \in \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}/\operatorname{\mathcal{D}})}$ and an isomorphism $\overline{e}: \overline{X} \rightarrow V(Y)$ in the $\infty $-category $\operatorname{\mathcal{D}}$; we wish to show that $\overline{e}$ can be lifted to an isomorphism $e: X \rightarrow Y$ of $\mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}/\operatorname{\mathcal{D}})}$. If $n \leq -2$, then $G$ is an isomorphism and the result is obvious. Otherwise, the comparison map $F': \operatorname{\mathcal{C}}\rightarrow \mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}/\operatorname{\mathcal{D}})}$ is surjective on vertices, so we can choose an object $\widetilde{Y} \in \operatorname{\mathcal{C}}$ satisfying $F'( \widetilde{Y} ) = Y$. If $F$ is an isofibration, then there exists an isomorphism $\widetilde{e}: \widetilde{X} \rightarrow \widetilde{Y}$ of $\operatorname{\mathcal{C}}$ satisfying $F( \widetilde{e} ) = \overline{e}$. It follows that $e = F'( \widetilde{e} )$ is an isomorphism in $\mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}}/\operatorname{\mathcal{D}})}$ satisfying $G(e) = \overline{e}$. $\square$