> [!definition]
>
> Let $X, Y$ be [[Topological Space|topological spaces]] and $f \in C(X, Y)$ be [[Continuity|continuous]], then $f$ is a **homotopy equivalence** if there exists a map $g \in C(Y, X)$, such that $f \circ g \in C(Y, Y)$ is [[Homotopy|homotopic]] to $\text{Id}_Y$, and $g \circ f \in C(X, X)$ is homotopic to $\text{Id}_X$. The mapping $g$ is known as the **homotopy inverse** of $f$.
>
> If there exists a homotopy equivalence$f \in C(X, Y)$, then $X$ and $Y$ are **homotopy equivalent** or of the **same homotopy type**. Homotopy equivalence is an [[Equivalence Relation|equivalence relation]].
>
> *Proof*. Let $X, Y, Z$ be topological spaces with homotopy equivalences $f \in C(X, Y)$ and $f' \in C(Y, Z)$. Let $g \in C(Y, X)$ and $g' \in C(Y, Z)$ be the homotopy inverses of $f$ and $f'$, respectively, then
> $
> (f' \circ f) \circ (g \circ g') = f'\circ (f \circ g) \circ g'
> $
> where $(f \circ g)$ is homotopic to $\text{Id}_Y$. Thus $(f' \circ f) \circ (g \circ g')$ is homotopic to $(f' \circ g')$, which is homotopic to $\text{Id}_Z$.