$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proposition 3.2.1.13. Let $f: (X,x) \rightarrow (Y,y)$ be a morphism of pointed Kan complexes. The following conditions are equivalent:
- $(1)$
The underlying morphism of simplicial sets $f: X \rightarrow Y$ is a homotopy equivalence (Definition 3.1.6.1): that is, there exists a morphism of simplicial sets $g: Y \rightarrow X$ such that $g \circ f$ and $f \circ g$ are homotopic to the identity maps $\operatorname{id}_{X}$ and $\operatorname{id}_{Y}$, respectively.
- $(2)$
The map $f$ is a pointed homotopy equivalence: that is, there exists a morphism of pointed simplicial sets $g: (Y,y) \rightarrow (X,x)$ such that $g \circ f$ and $f \circ g$ are pointed homotopic to the identity maps $\operatorname{id}_{X}$ and $\operatorname{id}_{Y}$, respectively.
Proof of Proposition 3.2.1.13.
Let $f: (X,x) \rightarrow (Y,y)$ be a morphism of pointed Kan complexes which is a homotopy equivalence; we wish to show that $f$ is a pointed homotopy equivalence (the reverse implication follows immediately from the definitions). Using Lemma 3.2.1.14, we deduce that there is a morphism of pointed Kan complexes $g: (Y,y) \rightarrow (X,x)$ such that the homotopy class $[g]$ is a left inverse of $[f]$ in the pointed homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}_{\ast }$. Since $f$ is a homotopy equivalence, it follows that $g$ is also a homotopy equivalence. Applying Lemma 3.2.1.14 again, we conclude that $[g]$ admits a left inverse in the pointed homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}_{\ast }$. In particular, $[g]$ is an isomorphism in $\mathrm{h} \mathit{\operatorname{Kan}}_{\ast }$, so its right inverse $[f]$ is also an isomorphism.
$\square$