Solution (source code)

= Solution

Use the <equivalence relation induced by a function>:
$$
x\sim x'\quad\Longleftrightarrow\quad f(x)=f(x').
$$
Equality in $Y$ supplies reflexivity, symmetry, and transitivity, so this is an <equivalence relation>. Define $\bar f:X/{\sim}\to Y$ by $\bar f([x])=f(x)$. It is well-defined; it is <injective> by the definition of $\sim$ and <surjective> because $f$ is <surjective>.

For an <open set> $W\subseteq Y$,
$$
p^{-1}\bigl(\bar f^{-1}(W)\bigr)=f^{-1}(W)
$$
is <open> by <continuity> of $f$. The <quotient topology> therefore makes $\bar f^{-1}(W)$ <open>, proving that $\bar f$ is <continuous>.

The <continuous image of a compact space> theorem applied to $p$ makes $X/{\sim}$ <compact>. If $C$ is <closed> in $X/{\sim}$, it is <compact>, and $\bar f(C)$ is <compact> in the <Hausdorff space> $Y$, hence <closed>. Thus $\bar f$ is a <closed map>. Its <inverse function> is <continuous>, since its <preimage> of $C$ is precisely $\bar f(C)$. We have proved that $\bar f$ is a <homeomorphism>, including the <compact-to-Hausdorff continuous bijection theorem> used in the argument.