Kerodon

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

Corollary 3.5.5.15. Let $n$ be a nonnegative integer and let $f: X \rightarrow Y$ be a homotopy equivalence of $n$-groupoids. If $f$ is bijective on $m$-simplices for $m < n$, then $f$ is an isomorphism.

Proof. It follows from Corollary 3.5.5.14 that $f$ is a Kan fibration. Applying Proposition 3.2.7.2, we deduce that $f$ is a trivial Kan fibration. In particular, $f$ admits a section $g: Y \hookrightarrow X$. To complete the proof, it will suffice to show that $g$ is an epimorphism of simplicial sets. This follows from Corollary 3.5.5.14, since $g$ is also bijective on $m$-simplices for $m < n$. $\square$