Kerodon

Proof. It follows from Proposition 4.8.3.6 that $F$ exhibits $\operatorname{cosk}^{\circ }_{n+1}(\operatorname{\mathcal{C}})$ as a local $n$-truncation of $\operatorname{\mathcal{C}}$. Applying Proposition 4.8.2.14, we see that $\operatorname{\mathcal{C}}$ is locally $n$-truncated if and only if $F$ is an equivalence of $\infty $-categories. We wish to show that if this condition is satisfied, then $F$ is a trivial Kan fibration. By virtue of Proposition 4.5.5.20, it will suffice to show that $F$ is an isofibration. For $n \neq -1$, this is automatic (Proposition 4.8.3.6). We will therefore assume that $n = -1$. Using Proposition 4.8.3.6, we see that $F$ is an inner fibration. Fix a morphism $\overline{u}: \overline{X} \rightarrow \overline{Y}$ in the $\infty $-category $\operatorname{cosk}_{0}^{\circ }(\operatorname{\mathcal{C}})$. Then there are unique objects $X,Y \in \operatorname{\mathcal{C}}$ satisfying $\overline{X} = F(X)$ and $\overline{Y} = F(Y)$. Choose a morphism $u: X \rightarrow Y$ satisfying $F(u) = \overline{u}$. To complete the proof, it will suffice to show that if $\overline{u}$ is an isomorphism in $\operatorname{cosk}_{0}^{\circ }(\operatorname{\mathcal{C}})$, then $u$ is an isomorphism in $\operatorname{\mathcal{C}}$. Let $\overline{v}: \overline{Y} \rightarrow \overline{X}$ be a homotopy inverse to $\overline{u}$. Then we can write $\overline{v} = F(v)$ for some morphism $v: Y \rightarrow X$ of $\operatorname{\mathcal{C}}$. Since the mapping space $\operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,X)$ is either empty or contractible, the composition $v \circ u$ is automatically homotopic to $\operatorname{id}_{X}$: that is $v$ is a left homotopy inverse to $u$. A similar argument shows that $v$ is right homotopy inverse to $u$, so that $u$ is an isomorphism as desired. $\square$