Kerodon

Proof. We first show that $(1)$ implies $(2)$. Here we may assume that $n > 0$ (otherwise, the result is a special case of Proposition 3.5.1.22). Let $\overline{\tau }$ be an $n$-simplex of $Y$, and set $\overline{\tau }_0 = \overline{\tau }|_{ \Lambda ^{n}_{0} }$. Since $f$ is bijective on $m$-simplices for $m < n$, we can lift $\overline{\tau }_0$ to a morphism $\tau _0: \Lambda ^{n}_{0} \rightarrow X$. If $f$ is a Kan fibration, then the lifting problem

admits a solution, given by an $n$-simplex $\tau $ of $X$ satisfying $f( \tau ) = \overline{\tau }$.

The implication $(2) \Rightarrow (3)$ is a special case of Corollary 3.5.2.2. We will complete the proof by showing that $(3)$ implies $(1)$. Assume that $f$ is $n$-connective and fix a pair of integers $0 \leq i \leq m$ with $m > 0$; we wish to show that every lifting problem

admits a solution. We consider three cases:

• Suppose that $m < n$. In this case, our assumption that $f$ is bijective on $m$-simplices guarantees that there is a unique $m$-simplex $\sigma $ of $X$ satisfying $f(\sigma ) = \overline{\sigma }$. By construction, we have $(f \circ \sigma )|_{ \Lambda ^{m}_{i} } = \overline{\sigma }|_{ \Lambda ^{m}_{i} } = f \circ \sigma _0$. Since $f$ is bijective on simplices of dimension $< m$, it follows that $\sigma _0 = \sigma |_{ \Lambda ^{m}_{i} }$.

• Suppose that $m > n$. In this case, our assumption that $X$ is a Kan complex guarantees that we can extend $\sigma _0$ to an $m$-simplex $\sigma $ of $X$. By construction, we have

  \[ (f \circ \sigma )|_{ \Lambda ^{m}_{i} } = f \circ \sigma _0 = \overline{\sigma }|_{ \Lambda ^{m}_{i} }. \]

  Since $Y$ is an $n$-groupoid, it follows that $f \circ \sigma = \overline{\sigma }$.

• Suppose that $m = n$. Since $f$ is bijective on $(n-1)$-simplices, the morphism $\sigma _0$ admits a unique extension $\sigma _1: \operatorname{\partial \Delta }^{n} \rightarrow X$ satisfying $f \circ \sigma _1 = \overline{\sigma }|_{ \operatorname{\partial \Delta }^{n} }$. The morphism $f$ factors as a composition

  \[ X \xrightarrow {i} X \times _{ \operatorname{Fun}( \{ 0\} , Y) } \operatorname{Fun}( \Delta ^1, Y ) \xrightarrow {q} Y, \]

  where $i$ is a homotopy equivalence and $q$ is a Kan fibration (see Example 3.1.7.10). Since $f$ is $n$-connective, the Kan fibration $q$ is also $n$-connective (Proposition 3.5.1.26). Applying Proposition 3.5.2.1, we conclude that there is an $n$-simplex $\sigma $ of $X$ satisfying $\sigma _1 = \sigma |_{ \operatorname{\partial \Delta }^{n} }$ and a homotopy from $f(\sigma )$ to $\overline{\sigma }$ which is constant when restricted to $\operatorname{\partial \Delta }^{n}$. Since $Y$ is an $n$-groupoid, Proposition 3.5.5.12 guarantees that $f(\sigma ) = \overline{\sigma }$.