Kerodon

Proof. It follows from Corollary 3.1.3.4 that $\operatorname{Fun}(K,X)$ is a Kan complex. Since $X$ is weakly $n$-coskeletal (Proposition 3.5.5.10), it follows that $\operatorname{Fun}(K,X)$ is also weakly $n$-coskeletal (Corollary 3.5.4.13). We will complete the proof by showing that $\operatorname{Fun}(K,X)$ satisfies condition $(\ast )$ of Proposition 3.5.5.12. Suppose we are given a pair of $n$-simplices $\sigma _0, \sigma _1: \Delta ^ n \rightarrow \operatorname{Fun}(K,X)$ which are homotopic relative to $\operatorname{\partial \Delta }^{n}$; we wish to show that $\sigma _0 = \sigma _1$. Let us identify $\sigma _0$ and $\sigma _1$ with morphisms $f_0, f_1: \Delta ^ n \times K \rightarrow X$. Since $X$ is weakly $n$-coskeletal, it will suffice to show that $f_0$ and $f_1$ coincide on $m$-simplices $\tau = (\tau ', \tau '')$ of $\Delta ^ n \times K$ for $m \leq n$. If $\tau '$ factors through the boundary $\operatorname{\partial \Delta }^ n$, this follows immediately from the equality $\sigma _0|_{\operatorname{\partial \Delta }^ n} = \sigma _1|_{ \operatorname{\partial \Delta }^ n}$. We may therefore assume without loss of generality that $m = n$ and that $\tau ': \Delta ^ m \rightarrow \Delta ^ n$ is the identity map. In this case, our assumption that $\sigma _0$ and $\sigma _1$ are homotopic relative to $\operatorname{\partial \Delta }^ n$ guarantees that $f_0(\tau )$ and $f_1(\tau )$ are homotopic relative to $\operatorname{\partial \Delta }^ n$, so that $f_0( \tau ) = f_1(\tau )$ by virtue of Proposition 3.5.5.12. $\square$