On homotopy classes of paths in \(X\) starting at \(x_0\text{,}\) define \([\alpha]\sim_H[\beta]\) if \(\alpha\) and \(\beta\) have the same endpoint and \([\alpha*\bar\beta]\in H\text{.}\) This is an equivalence relation: symmetry uses inverses in \(H\text{,}\) and transitivity uses
\begin{equation*}
[\alpha*\bar\beta]\,[\beta*\bar\gamma]=[\alpha*\bar\gamma].
\end{equation*}
Let \(X_H\) be the set of equivalence classes, written \([\alpha]_H\text{,}\) and define \(p_H([\alpha]_H)=\alpha(1)\text{.}\)
For a path-connected open set \(U\) whose loops are null-homotopic in \(X\text{,}\) and for \(\alpha\) ending at \(x\in U\text{,}\) set
\begin{equation*}
B_H([\alpha]_H,U):=
\{[\alpha*\gamma]_H\mid \gamma\text{ is a path in }U\text{ starting at }x\}.
\end{equation*}
As in the path-space construction of
Proposition 3.15, these sets form a basis, the distinct sets over a fixed
\(U\) partition
\(p_H^{-1}(U)\text{,}\) and each restriction
\(p_H|_{B_H([\alpha]_H,U)}\) is a homeomorphism onto
\(U\text{.}\) Hence
\(p_H\) is a covering. Every point
\([\alpha]_H\) is joined to
\([c_{x_0}]_H\) by the path obtained from the initial segments of
\(\alpha\text{,}\) so
\(X_H\) is path-connected.
Set \(\tilde x_H=[c_{x_0}]_H\text{.}\) If \(\gamma\) is a loop at \(x_0\text{,}\) its lift starting at \(\tilde x_H\) ends at \([\gamma]_H\text{.}\) It is therefore a loop if and only if
\begin{equation*}
[\gamma]_H=[c_{x_0}]_H \iff [\gamma]\in H.
\end{equation*}
By
Proposition 3.7(1), this says precisely that
\((p_H)_*\pi_1(X_H,\tilde x_H)=H\text{.}\)
