[proofplan]
We verify the three axioms of an equivalence relation for homotopy equivalence of topological spaces. Reflexivity uses the identity map; symmetry swaps the roles of the homotopy equivalence and its homotopy inverse; transitivity composes two homotopy equivalences and verifies that the composite homotopy inverse works, using the fact that homotopy is compatible with composition.
[/proofplan]
[step:Verify reflexivity using the identity map]
For any topological space $X$, the identity map $\operatorname{id}_X: X \to X$ is a homotopy equivalence with homotopy inverse $\operatorname{id}_X$. Indeed, $\operatorname{id}_X \circ \operatorname{id}_X = \operatorname{id}_X \simeq \operatorname{id}_X$ (by reflexivity of homotopy of maps). Hence $X \simeq X$.
[/step]
[step:Verify symmetry by swapping the homotopy equivalence and its inverse]
Suppose $X \simeq Y$ via a homotopy equivalence $f: X \to Y$ with homotopy inverse $g: Y \to X$. By definition, $g \circ f \simeq \operatorname{id}_X$ and $f \circ g \simeq \operatorname{id}_Y$. But this means $g: Y \to X$ is itself a homotopy equivalence with homotopy inverse $f$: we have $f \circ g \simeq \operatorname{id}_Y$ and $g \circ f \simeq \operatorname{id}_X$. Hence $Y \simeq X$.
[/step]
[step:Verify transitivity by composing homotopy equivalences]
Suppose $X \simeq Y$ via $f: X \to Y$ with homotopy inverse $g: Y \to X$, and $Y \simeq Z$ via $h: Y \to Z$ with homotopy inverse $k: Z \to Y$. We claim that $h \circ f: X \to Z$ is a homotopy equivalence with homotopy inverse $g \circ k: Z \to X$.
We verify the two required homotopies.
**First composition.** We must show $(g \circ k) \circ (h \circ f) \simeq \operatorname{id}_X$. By associativity of composition, $(g \circ k) \circ (h \circ f) = g \circ (k \circ h) \circ f$. Since $k \circ h \simeq \operatorname{id}_Y$, the [Composition of Homotopies](/theorems/2230) applied to $k \circ h \simeq \operatorname{id}_Y$ (composed on the left with $g$ and on the right with $f$) gives $g \circ (k \circ h) \circ f \simeq g \circ \operatorname{id}_Y \circ f = g \circ f \simeq \operatorname{id}_X$.
**Second composition.** We must show $(h \circ f) \circ (g \circ k) \simeq \operatorname{id}_Z$. By the same reasoning, $(h \circ f) \circ (g \circ k) = h \circ (f \circ g) \circ k$. Since $f \circ g \simeq \operatorname{id}_Y$, the [Composition of Homotopies](/theorems/2230) gives $h \circ (f \circ g) \circ k \simeq h \circ \operatorname{id}_Y \circ k = h \circ k \simeq \operatorname{id}_Z$.
Hence $h \circ f$ is a homotopy equivalence, so $X \simeq Z$.
[guided]
We want to show that if $X \simeq Y$ and $Y \simeq Z$, then $X \simeq Z$. The natural candidate for a homotopy equivalence $X \to Z$ is the composition $h \circ f$, and for its homotopy inverse, $g \circ k$.
The key question is: why does $(g \circ k) \circ (h \circ f) \simeq \operatorname{id}_X$? We cannot simply "cancel" $k$ with $h$ and $g$ with $f$ — homotopy equivalence is not strict equality. Instead, we use the [Composition of Homotopies](/theorems/2230): if $\alpha_0 \simeq \alpha_1$ and $\beta_0 \simeq \beta_1$, then $\beta_0 \circ \alpha_0 \simeq \beta_1 \circ \alpha_1$.
Rewrite $(g \circ k) \circ (h \circ f) = g \circ (k \circ h) \circ f$ by associativity. We know $k \circ h \simeq \operatorname{id}_Y$. Applying the composition of homotopies with $g$ on the left (taking $\beta_0 = g$, $\beta_1 = g$, so $g \simeq g$ by reflexivity) and $f$ on the right (taking $\alpha_0 = (k \circ h) \circ f$, and using that $k \circ h \simeq \operatorname{id}_Y$ gives $(k \circ h) \circ f \simeq \operatorname{id}_Y \circ f = f$), we get:
\begin{align*}
g \circ (k \circ h) \circ f \simeq g \circ f \simeq \operatorname{id}_X.
\end{align*}
The second homotopy follows by the same argument with the roles interchanged: $(h \circ f) \circ (g \circ k) = h \circ (f \circ g) \circ k \simeq h \circ k \simeq \operatorname{id}_Z$.
[/guided]
[/step]
[step:Conclude that homotopy equivalence is an equivalence relation]
Having verified reflexivity, symmetry, and transitivity, we conclude that homotopy equivalence is an equivalence relation on the class of topological spaces.
[/step]
