Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Corollary 3.5.7.13. Let $n$ be an integer and let $f: X \rightarrow Y$ be a morphism of $n$-truncated Kan complexes. Then $f$ is a homotopy equivalence if and only if it is $(n+1)$-connective.

Proof. If $n \leq -2$, then $X$ and $Y$ are contractible and there is nothing to prove. For $n \geq -1$, the desired result follows by combining Proposition 3.5.7.7 (and Remark 3.5.7.8) with Theorem 3.2.7.1. $\square$