Kerodon

Proof. By virtue of Proposition 4.8.3.6, the weak $n$-coskeleton $\operatorname{cosk}^{\circ }_{n}(\operatorname{\mathcal{C}})$ is an $\infty $-category. Combining Corollary 4.8.4.13 with Proposition 1.5.5.11, we conclude that $\mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}})}$ is also an $\infty $-category. To complete the proof, it will suffice to show that if $\sigma $ and $\tau $ are $m$-simplices of $\mathrm{h}_{\mathit{\leq n}}\mathit{(\operatorname{\mathcal{C}})}$ for some $m > n$ which satisfy $\sigma |_{ \Lambda ^{m}_{i} } = \tau |_{ \Lambda ^{m}_{i} }$ for some $0 < i < m$, then $\sigma = \tau $. Choose maps $\widetilde{\sigma }, \widetilde{\tau }: \operatorname{sk}_{n}( \Delta ^{m} ) \rightarrow \operatorname{\mathcal{C}}$ representing $\sigma $ and $\tau $. Using Proposition 4.8.4.11, we can choose an isomorphism $\alpha $ from $\widetilde{\sigma }|_{ \operatorname{sk}_{n}( \Lambda ^{m}_{i}) }$ to $\widetilde{\tau }|_{ \operatorname{sk}_{n}(\Lambda ^{m}_{i} ) }$ whose image in $\operatorname{Fun}( \operatorname{sk}_{n-1}( \Lambda ^{m}_{i} ), \operatorname{\mathcal{C}})$ is an identity morphism. If $m \geq n+2$, then $\alpha $ is also an isomorphism from $\widetilde{\sigma }|_{ \operatorname{sk}_{n}( \Delta ^ m) }$ to $\widetilde{\tau }|_{ \operatorname{sk}_{n}( \Delta ^ m ) }$, so that $\sigma = \tau $ as desired. In the case $m = n+1$, the morphisms $\widetilde{\sigma }$ and $\widetilde{\tau }$ can be extended to diagrams $\overline{\sigma }, \overline{\tau }: \Delta ^{n+1} \rightarrow \operatorname{\mathcal{C}}$. Using Proposition 1.5.7.6, we can extend $\alpha $ to an isomorphism of $\overline{\sigma }$ with $\overline{\tau }$. Restricting to the $n$-skeleton of $\Delta ^{m}$, we again conclude that $\sigma = \tau $. $\square$