Kerodon

Proof. Assume first that $X$ is an $n$-groupoid and let $\sigma _0, \sigma _1: \Delta ^ n \rightarrow X$ be $n$-simplices of $X$ which are homotopic relative to $\operatorname{\partial \Delta }^ n$. Since $X$ is a Kan complex, there exists a homotopy $h: \Delta ^1 \times \Delta ^ n \rightarrow X$ from $\sigma _0$ to $\sigma _1$ which is constant along $\operatorname{\partial \Delta }^ n$ (Proposition 3.2.1.4). For $0 \leq i \leq n$, let $\alpha _{i}: [n+1] \rightarrow [1] \times [n]$ denote the nondecreasing function given by the formula

and let $\tau _{i}$ denote the $(n+1)$-simplex of $X$ given by the composition

Let $\rho _{i}, \rho '_{i}: \Delta ^{n} \rightarrow X$ be the $n$-simplices of $X$ given by $\rho _{i} = d^{n+1}_{i}( \tau _ i )$ and $\rho '_{i} = d^{n+1}_{i+1}( \tau _ i )$; by construction, we have

We will complete the proof by showing that $\rho _{i} = \rho '_{i}$ for $0 \leq i \leq n$. Using our assumption that the homotopy $h$ is constant along the boundary $\operatorname{\partial \Delta }^{n}$, we see that the degenerate $(n+1)$-simplex $s^{n}_{i}( \rho _{i} )$ coincides with $\tau _ i$ on the horn $\Lambda ^{n+1}_{i} \subset \Delta ^{n+1}$. Invoking our assumption that $X$ is an $n$-groupoid, we conclude that $\tau _ i = s^{n}_{i}( \rho _{i} )$. Applying the face operator $d^{n+1}_{i+1}$, we obtain $\rho _{i} = \rho '_{i}$.

We now prove the converse. Assume that $X$ satisfies condition $(\ast )$; we wish to show that the Kan complex $X$ is an $n$-groupoid. Fix a pair of integers $0 \leq i \leq m$ with $m > n$ and a pair of $m$-simplices $\tau _0, \tau _1: \Delta ^{m} \rightarrow X$ which coincide on the horn $\Lambda ^{m}_{i} \subset \Delta ^{m}$; we wish to show that $\tau _0 = \tau _1$. Since $X$ is weakly $n$-coskeletal, it will suffice to prove that $\tau _0$ and $\tau _1$ coincide on the boundary $\operatorname{\partial \Delta }^{m}$: that is, to show that the $(m-1)$-simplices $\sigma _0 = d^{m}_{i}(\tau _0)$ and $\sigma _1 = d^{m}_{i}(\tau _1)$ coincide. Note that $\sigma _0$ and $\sigma _1$ have the same restriction to the boundary $\operatorname{\partial \Delta }^{m-1}$. Consequently, if $m \geq n+2$, the desired result follows from our assumption that $X$ is weakly $n$-coskeletal. We may therefore assume that $m = n+1$. By virtue of $(\ast )$, it will suffice to show that the $(m-1)$-simplices $\sigma _0$ and $\sigma _1$ are homotopic relative to $\operatorname{\partial \Delta }^{m-1}$. In fact, we will prove a stronger claim: the $m$-simplices $\tau _0$ and $\tau _1$ are homotopic relative to the horn $\Lambda ^{m}_{i} \subset \Delta ^{m}$. This follows from the observation that the restriction map $\operatorname{Fun}( \Delta ^{m}, X) \rightarrow \operatorname{Fun}( \Lambda ^{m}_{i}, X)$ is a trivial Kan fibration; see Corollary 3.1.3.6. $\square$