Kerodon

Proof. Assume first that there exists a weak homotopy equivalence $f: X \rightarrow Y$, where $Y$ is $n$-reduced. Choose a vertex $y \in Y$. Our assumption that $Y$ is $n$-reduced guarantees that the inclusion map $i: \{ y\} \hookrightarrow Y$ is bijective on $m$-simplices for $m \leq n$. Applying Corollary 3.5.2.2, we deduce that $i$ is $n$-connective. It follows that $Y$ is $(n+1)$-connective (Corollary 3.5.1.27). Since $f$ is a weak homotopy equivalence, the simplicial set $X$ is also $(n+1)$-connective.

We now prove the converse. Assume that $X$ is $(n+1)$-connective. In particular, $X$ is nonempty; we can therefore choose a vertex $x \in X$. Using Proposition 3.1.7.1, we can factor the inclusion map $\{ x\} \hookrightarrow X$ as a composition $\{ x \} \xrightarrow {j} E \xrightarrow {g} X$, where $j$ is anodyne and $g$ is a Kan fibration. Since the simplicial set $E$ is weakly contractible, our hypothesis that $X$ is $(n+1)$-connective guarantees that $f$ is $n$-connective (Proposition 3.5.1.26). Applying Corollary 3.5.2.4, we can factor $g$ as a composition $E \xrightarrow {g'} \widetilde{X} \xrightarrow {g''} X$, where $g'$ is a monomorphism which is bijective on $m$-simplices for $m \leq n$ and $g''$ is a trivial Kan fibration. Let $s$ be a section of $g''$ and let $Y = \widetilde{X} / E$ be the simplicial set obtained from $\widetilde{X}$ by collapsing the image of $g'$, so that we have a pushout square

Since $g'$ is a monomorphism, (3.70) is a homotopy pushout square (Example 3.4.2.12). Since $E$ is weakly contractible, it follows that $q$ is a weak homotopy equivalence (Proposition 3.4.2.10). It follows that the composite map $X \xrightarrow {s} \widetilde{X} \xrightarrow {q} Y$ is a weak homotopy equivalence from $X$ to an $n$-reduced simplicial set $Y$. $\square$