Kerodon

Proof. Let $K$ be a simplicial set; we will show that precomposition with $f$ induces a bijection $\operatorname{Hom}_{\operatorname{Set_{\Delta }}}(K, \operatorname{Fun}(Y,Z) ) \rightarrow \operatorname{Hom}_{\operatorname{Set_{\Delta }}}(K, \operatorname{Fun}(X,Z) )$. Replacing $Z$ by the $n$-groupoid $\operatorname{Fun}(K,Z)$ (Corollary 3.5.5.13), we are reduced to proving that the natural map

is a bijection.

Let $h: X \rightarrow Z$ be a morphism of Kan complexes; we wish to show that there is a unique morphism $g: Y \rightarrow Z$ satisfying $g \circ f = h$. We first claim that there is a unique morphism $g_0: \operatorname{sk}_{n}(Y) \rightarrow Z$ satisfying $g_0 \circ \operatorname{sk}_{n}(f) = h|_{ \operatorname{sk}_{n}(X) }$. Our assumption that $f$ exhibits $Y$ as a fundamental $n$-groupoid of $X$ guarantees that $\operatorname{sk}_{n}(f)$ is surjective. It will therefore suffice to show that if $\sigma $ and $\sigma '$ are $m$-simplices of $X$ for $m \leq n$ satisfying $f(\sigma ) = f(\sigma ')$, then $h(\sigma ) = h(\sigma ')$. If $m < n$, then $\sigma = \sigma '$ and the result is clear. In the case $m = n$, the assumption that $f(\sigma ) = f(\sigma ')$ guarantees that $\sigma $ and $\sigma '$ are homotopic relative to $\operatorname{\partial \Delta }^{n}$, in which case the desired result follows from Proposition 3.5.5.12.

It follows from Remark 3.5.6.2 that every $(n+1)$-simplex $\tau $ of $Y$ can be lifted to an $(n+1)$-simplex $\widetilde{\tau }$ of $X$. In particular, $g_0 \circ \tau |_{ \operatorname{\partial \Delta }^{n+1} }$ extends to an $(n+1)$-simplex of $Z$, given by $h( \widetilde{\tau } )$. Since $Z$ is weakly $n$-coskeletal (Proposition 3.5.5.10), Proposition 3.5.4.12 guarantees that $g_0$ extends uniquely to a morphism $g: Y \rightarrow Z$, which automatically satisfies the equation $g \circ f = h$. $\square$