# Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$

Proposition 3.1.5.12. Let $f: X_{} \rightarrow Y_{}$ be a morphism of simplicial sets. If $f$ is a homotopy equivalence, then it is a weak homotopy equivalence. The converse holds if $X_{}$ and $Y_{}$ are Kan complexes.

Proof. The first assertion follows from Remark 3.1.5.5. For the second, assume that $f$ is a weak homotopy equivalence. If $X_{}$ is a Kan complex, then precomposition with $f$ induces a bijection $\pi _0( \operatorname{Fun}(Y_{}, X_{} ) ) \rightarrow \pi _0( \operatorname{Fun}( X_{}, X_{} ) )$. We can therefore choose a map of simplicial sets $g: Y_{} \rightarrow X_{}$ such that $g \circ f$ is homotopic to the identity on $X_{}$ It follows that $f \circ g \circ f$ is homotopic to $f = \operatorname{id}_{Y_{}} \circ f$. Invoking the injectivity of the map $\pi _0( \operatorname{Fun}(Y_{}, Y_{} ) ) \xrightarrow {\circ f} \pi _0( \operatorname{Fun}( X_{}, Y_{} ) )$, we conclude that $f \circ g$ is homotopic to $\operatorname{id}_{ Y_{} }$, so that $g$ is a homotopy inverse to $f$. $\square$