Kerodon

Proof. By virtue of Proposition 3.5.3.23, the coskeleton $\operatorname{cosk}_{n+1}(X)$ is a Kan complex. Combining Corollary3.5.6.15 with Proposition 1.5.5.11, we conclude that $\pi _{\leq n}(X)$ is a Kan complex. To complete the proof, it will suffice to show that if $\sigma $ and $\tau $ are $m$-simplices of $\pi _{\leq n}(X)$ for some $m > n$ which satisfy $\sigma |_{ \Lambda ^{m}_{i} } = \tau |_{ \Lambda ^{m}_{i} }$ for some $0 \leq i \leq m$, then $\sigma = \tau $. Choose maps $\widetilde{\sigma }, \widetilde{\tau }: \operatorname{sk}_{n}( \Delta ^{m} ) \rightarrow X$ representing $\sigma $ and $\tau $. Using Proposition 3.5.6.12, we can choose a homotopy from $\widetilde{\sigma }|_{ \operatorname{sk}_{n}( \Lambda ^{m}_{i}) }$ to $\widetilde{\tau }|_{ \operatorname{sk}_{n}(\Lambda ^{m}_{i} ) }$ which is constant when restricted to the skeleton $\operatorname{sk}_{n-1}( \Lambda ^{m}_{i} ) = \operatorname{sk}_{n-1}( \Delta ^ m )$. If $m \geq n+2$, then $h$ is also a homotopy 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 morphisms $\overline{\sigma }, \overline{\tau }: \Delta ^{n+1} \rightarrow X$. Using Corollary 3.1.3.6, we can extend $h$ to a homotopy $\overline{h}$ from $\overline{\sigma }$ to $\overline{\tau }$. Restricting this homotopy to the $n$-skeleton of $\Delta ^{m}$, we again conclude that $\sigma = \tau $. $\square$