Kerodon

Proof. It follows from Theorem 1.5.3.7 that $\operatorname{Fun}(K,\operatorname{\mathcal{C}})$ is an $\infty $-category. Since $\operatorname{\mathcal{C}}$ is weakly $n$-coskeletal, the $\infty $-category $\operatorname{Fun}(K,\operatorname{\mathcal{C}})$ is also weakly $n$-coskeletal (Corollary 3.5.4.13). To complete the proof, it will suffice to show that if $n \geq 0$, then $\operatorname{Fun}(K,\operatorname{\mathcal{C}})$ is minimal in dimension $n$ (Proposition 4.8.1.7). Suppose we are given a pair of $n$-simplices $\sigma _0, \sigma _1: \Delta ^ n \rightarrow \operatorname{Fun}(K,\operatorname{\mathcal{C}})$ and an isomorphism $\sigma _0 \xrightarrow {\sim } \sigma _1$ whose restriction to $\operatorname{\partial \Delta }^ n$ is an identity morphism; we wish to show that $\sigma _0 = \sigma _1$. Let us identify $\sigma _0$ and $\sigma _1$ with diagrams $f_0, f_1: \Delta ^ n \times K \rightarrow \operatorname{\mathcal{C}}$. Since $\operatorname{\mathcal{C}}$ 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 guarantees that there is an isomorphism of $f_0( \tau )$ with $f_1(\tau )$ whose image in $\operatorname{Fun}( \operatorname{\partial \Delta }^ n, \operatorname{\mathcal{C}})$ is an identity morphism. The equality $f_0( \tau ) = f_1(\tau )$ now follows from the fact that $\operatorname{\mathcal{C}}$ is minimal in dimension $n$ (Proposition 4.8.1.7). $\square$