[proofplan] We construct the universal cover $\tilde{X}$ explicitly. Fix a basepoint $x_0 \in X$ and let $\tilde{X}$ be the set of path-homotopy classes $[\alpha]$ of paths $\alpha: I \to X$ starting at $x_0$. The projection $p([\alpha]) := \alpha(1)$ is set-theoretically fibred over $X$ by the endpoints of representative paths. We topologise $\tilde{X}$ by a basis $\{U_{[\alpha]}\}$ of "sheets" over evenly coverable opens; the three hypotheses on $X$ are each consumed at a distinct step. Semi-local simple connectivity ensures the basis sets are well-defined (concatenated paths are unambiguous up to homotopy inside the good neighbourhoods). Local path-connectedness upgrades the basis to a genuine topology for which $p$ is a covering map with homeomorphic sheets. Path-connectedness of $X$, together with the construction itself, lifts to path-connectedness of $\tilde{X}$. Finally, simple connectivity of $\tilde{X}$ is the canonical cancellation: a loop $\tilde{\sigma}$ at $[c_{x_0}]$ projects to a loop $\sigma = p \circ \tilde{\sigma}$ whose concatenations $[c_{x_0} \cdot \sigma|_{[0, t]}]$ identify with $\tilde{\sigma}(t)$, and the resulting null-homotopy of $[\sigma]$ in $\pi_1(X, x_0)$ retracts $\tilde{\sigma}$ to the constant path. [/proofplan]

[step:Define the set $\tilde{X}$ and the projection $p$]Fix a basepoint $x_0 \in X$. Let $P(X, x_0)$ denote the set of continuous paths $\alpha: I \to X$ with $\alpha(0) = x_0$, and let $\simeq$ denote path-homotopy rel endpoints. Define \begin{align*} \tilde{X} := P(X, x_0) / \simeq, \qquad p: \tilde{X} \to X, \quad [\alpha] \mapsto \alpha(1). \end{align*} The map $p$ is well-defined on equivalence classes because path-homotopy rel endpoints preserves the right endpoint $\alpha(1)$. Choose the distinguished basepoint \begin{align*} \tilde{x}_0 := [c_{x_0}] \in \tilde{X}, \end{align*} where $c_{x_0}: I \to X$ is the constant path $t \mapsto x_0$; then $p(\tilde{x}_0) = x_0$.[/step]

[guided]The construction rests on a heuristic: if $\tilde{X}$ is simply connected and $p: \tilde{X} \to X$ is a covering, then any two paths in $\tilde{X}$ from $\tilde{x}_0$ with the same endpoint are homotopic (by simple connectivity of $\tilde{X}$), so paths in $\tilde{X}$ from $\tilde{x}_0$ up to homotopy are **in bijection** with points of $\tilde{X}$. Projecting via $p$ converts them into paths in $X$ from $x_0$ up to homotopy — and path-homotopy in $X$ is preserved by lifting (see [Lifted Path Homotopy](/theorems/1888)). So points of the universal cover *must* correspond to homotopy classes of paths in $X$ from $x_0$. We take this bijection as the **definition**. Formally: set \begin{align*} \tilde{X} := P(X, x_0) / \simeq, \end{align*} where $P(X, x_0) = \{\alpha: I \to X \text{ continuous, } \alpha(0) = x_0\}$ and $\simeq$ is path-homotopy rel endpoints. Define the projection \begin{align*} p: \tilde{X} \to X, \qquad [\alpha] \mapsto \alpha(1). \end{align*} Why is $p$ well-defined? If $\alpha \simeq \alpha'$ rel endpoints, the homotopy fixes $\alpha(0) = \alpha'(0) = x_0$ and $\alpha(1) = \alpha'(1)$, so both representatives share the same endpoint and $p$ assigns the same value. Finally, take the constant path $c_{x_0}$ at $x_0$ as our distinguished lift of $x_0$: set $\tilde{x}_0 := [c_{x_0}]$. Then $p(\tilde{x}_0) = c_{x_0}(1) = x_0$.[/guided]

[step:Define the basis of sheets $U_{[\alpha]}$ for the topology on $\tilde{X}$] Call an open $U \subseteq X$ **good** if $U$ is path-connected and the inclusion $U \hookrightarrow X$ induces the trivial map $\pi_1(U, u) \to \pi_1(X, u)$ for every $u \in U$ — equivalently, every loop in $U$ is null-homotopic *in $X$*. By semi-local simple connectivity of $X$, every point of $X$ has a neighbourhood $V$ in which every loop is null-homotopic in $X$; by local path-connectedness, we may shrink $V$ to a path-connected neighbourhood. Hence good opens cover $X$. For a good open $U \subseteq X$ and a class $[\alpha] \in \tilde{X}$ with $\alpha(1) \in U$, define \begin{align*} U_{[\alpha]} := \{[\alpha \cdot \beta] : \beta: I \to U \text{ continuous, } \beta(0) = \alpha(1)\}, \end{align*} where $\alpha \cdot \beta$ denotes path concatenation. The class $[\alpha \cdot \beta]$ depends only on $[\alpha]$ and the path-homotopy class of $\beta$ rel endpoints **within $U$**: if $\beta \simeq \beta'$ rel endpoints in $U$ then $\alpha \cdot \beta \simeq \alpha \cdot \beta'$ rel endpoints in $X$ (see [Group Laws for Paths up to Homotopy](/theorems/1877)). In fact, because $U$ is good, *any* two paths $\beta, \beta'$ in $U$ with the same endpoints satisfy $\beta \simeq \beta'$ rel endpoints in $X$: the loop $\beta \cdot \overline{\beta'}$ lies in $U$ and is null-homotopic in $X$ by goodness of $U$.[/step]

[guided]To topologise $\tilde{X}$ we need a basis of open sets. The right intuition is: near a point $[\alpha] \in \tilde{X}$ lying over $x = \alpha(1) \in X$, neighbours of $[\alpha]$ should be obtained by extending $\alpha$ slightly within a "good" neighbourhood $U$ of $x$. **Good opens.** Define $U \subseteq X$ open to be **good** if $U$ is path-connected and every loop in $U$ is null-homotopic in $X$ (not only in $U$). Equivalently, the homomorphism $\pi_1(U, u) \to \pi_1(X, u)$ induced by inclusion is trivial for every $u \in U$. **Every point has a good neighbourhood.** By the semi-local simple connectivity hypothesis on $X$, every $x \in X$ has an open neighbourhood $V$ in which every loop is null-homotopic in $X$. By the local path-connectedness hypothesis, the path component of $x$ in $V$ is open in $X$ (components of open sets in locally path-connected spaces are open). Shrink $V$ to this path component; the result is good. Hence the good opens cover $X$. **Definition of the basic sheet.** For a good open $U \subseteq X$ and a class $[\alpha] \in \tilde{X}$ with $\alpha(1) \in U$, define \begin{align*} U_{[\alpha]} := \{[\alpha \cdot \beta] : \beta: I \to U, \, \beta(0) = \alpha(1)\}. \end{align*} That is: extend the path $\alpha$ by any path $\beta$ lying **entirely in $U$** starting where $\alpha$ ends, and take the resulting homotopy class in $\tilde{X}$. **Independence from representatives.** Suppose $\alpha \simeq \alpha'$ rel endpoints, so $[\alpha] = [\alpha']$. Then $\alpha \cdot \beta \simeq \alpha' \cdot \beta$ rel endpoints (concatenation respects homotopy; see [Group Laws for Paths up to Homotopy](/theorems/1877)), so $[\alpha \cdot \beta] = [\alpha' \cdot \beta]$ — the set $U_{[\alpha]}$ only depends on the class $[\alpha]$, not on the representative. **Collapsing of $\beta$.** In fact, which $\beta$ we pick in $U$ between fixed endpoints $\alpha(1)$ and some $y \in U$ is irrelevant. If $\beta, \beta'$ are two such paths, then the loop $\beta \cdot \overline{\beta'}$ (traversing $\beta$ then $\beta'$ in reverse) lies in $U$ — but $U$ is good, so this loop is null-homotopic in $X$. Thus $\beta \simeq \beta'$ rel endpoints in $X$, and $[\alpha \cdot \beta] = [\alpha \cdot \beta']$ in $\tilde{X}$. This means $U_{[\alpha]}$ is parametrised by the endpoints of $\beta$: the map $[\alpha \cdot \beta] \mapsto \beta(1)$ is a **bijection** from $U_{[\alpha]}$ onto $U$. This bijection will shortly be upgraded to a homeomorphism.[/guided]

[step:Verify the $U_{[\alpha]}$ form a basis and $p$ is locally homeomorphic] We show two structural properties of the collection $\mathcal{B} := \{U_{[\alpha]} : U \subseteq X \text{ good open}, [\alpha] \in \tilde{X}, \alpha(1) \in U\}$. *$\mathcal{B}$ is a basis.* Every $[\alpha] \in \tilde{X}$ belongs to some $U_{[\alpha]}$: pick any good open $U$ containing $\alpha(1)$ (such $U$ exists by the goodness argument of Step 2), and take $\beta$ to be the constant path at $\alpha(1)$ in $U$; then $[\alpha] = [\alpha \cdot \beta] \in U_{[\alpha]}$. For the intersection property, let $[\gamma] \in U_{[\alpha]} \cap V_{[\alpha']}$ with $U, V$ good. Then $\gamma(1) \in U \cap V$. By local path-connectedness of $X$, the path component $W$ of $\gamma(1)$ in $U \cap V$ is open in $X$, and it is good (any loop in $W$ is a loop in $U$, hence null-homotopic in $X$). By the collapsing argument of Step 2, \begin{align*} W_{[\gamma]} \subseteq U_{[\alpha]} \cap V_{[\alpha']}, \end{align*} because any element of $W_{[\gamma]}$ has the form $[\gamma \cdot \delta]$ with $\delta$ in $W \subseteq U \cap V$, hence lies in both $U_{[\alpha]}$ and $V_{[\alpha']}$. *$p$ restricts to a bijection $U_{[\alpha]} \to U$.* The map $p: U_{[\alpha]} \to U$ sends $[\alpha \cdot \beta] \mapsto \beta(1)$; it is onto since $U$ is path-connected (for any $y \in U$, pick a path $\beta$ from $\alpha(1)$ to $y$ in $U$). It is injective by the collapsing argument: if $[\alpha \cdot \beta] = [\alpha \cdot \beta']$ with $\beta(1) = \beta'(1)$, the endpoints match, and conversely if $\beta(1) = \beta'(1)$ we showed $[\alpha \cdot \beta] = [\alpha \cdot \beta']$. Equip $\tilde{X}$ with the topology generated by $\mathcal{B}$. Then $p: \tilde{X} \to X$ is continuous: for a good open $U \subseteq X$, \begin{align*} p^{-1}(U) = \bigsqcup_{[\alpha] \in p^{-1}(U)/\sim_U} U_{[\alpha]}, \end{align*} where $\sim_U$ is the equivalence relation $[\alpha] \sim_U [\alpha']$ iff $U_{[\alpha]} = U_{[\alpha']}$. The disjointness follows from injectivity of $p$ on each sheet: if $[\gamma] \in U_{[\alpha]} \cap U_{[\alpha']}$ with $U$ good, then by the collapsing argument applied to $[\gamma]$ both sheets equal $U_{[\gamma]}$. Thus $p^{-1}(U)$ is a disjoint union of open sets, each mapped bijectively onto $U$ by $p$. The inverse map $U \to U_{[\alpha]}$ is $y \mapsto [\alpha \cdot \beta_y]$, where $\beta_y$ is any path in $U$ from $\alpha(1)$ to $y$; this is well-defined by the collapsing argument, and shown continuous by the same basis-open argument applied with smaller good neighbourhoods inside $U$. Hence $p|_{U_{[\alpha]}}: U_{[\alpha]} \to U$ is a homeomorphism, and $p$ is a **covering map** with good opens as evenly covered opens.[/step]

[guided]We verify the collection $\mathcal{B}$ is a basis for a topology, then identify the sheets over good opens. **Basis property: covering.** Each $[\alpha] \in \tilde{X}$ lies in *some* basic set: pick any good open $U \ni \alpha(1)$ (exists by Step 2), and take $\beta$ the constant path at $\alpha(1)$; then $\alpha \simeq \alpha \cdot \beta$ rel endpoints (reparametrisation), so $[\alpha] = [\alpha \cdot \beta] \in U_{[\alpha]}$. **Basis property: intersection.** Let $[\gamma] \in U_{[\alpha]} \cap V_{[\alpha']}$, where $U, V$ are good. Then $\gamma(1) \in U \cap V$. The set $U \cap V$ is open but may not be good (e.g. not path-connected); local path-connectedness of $X$ gives us a path-connected open $W \subseteq U \cap V$ containing $\gamma(1)$ — concretely, $W$ is the path component of $\gamma(1)$ in $U \cap V$, which is open because $X$ is locally path-connected. The set $W$ is good: it is path-connected by construction, and any loop in $W$ is a loop in $U$, hence null-homotopic in $X$ because $U$ is good. We claim $W_{[\gamma]} \subseteq U_{[\alpha]} \cap V_{[\alpha']}$. Take a typical element $[\gamma \cdot \delta]$ with $\delta$ a path in $W$ from $\gamma(1)$. Since $W \subseteq U$, the path $\delta$ lies in $U$. We must produce a representation $[\gamma \cdot \delta] = [\alpha \cdot \beta]$ with $\beta$ a path in $U$; we use that $[\gamma] \in U_{[\alpha]}$, so $[\gamma] = [\alpha \cdot \beta_0]$ for some path $\beta_0$ in $U$. Then $[\gamma \cdot \delta] = [\alpha \cdot \beta_0 \cdot \delta] = [\alpha \cdot (\beta_0 \cdot \delta)]$, and $\beta_0 \cdot \delta$ is a path in $U$. Thus $[\gamma \cdot \delta] \in U_{[\alpha]}$. Similarly $[\gamma \cdot \delta] \in V_{[\alpha']}$. **Restriction of $p$ to a sheet.** Fix a good open $U$ and a class $[\alpha]$ with $\alpha(1) \in U$. Define $p_U : U_{[\alpha]} \to U$, $[\alpha \cdot \beta] \mapsto \beta(1)$. - *Surjective.* Since $U$ is path-connected, for any $y \in U$ there is a path $\beta$ in $U$ from $\alpha(1)$ to $y$. - *Injective.* If $\beta(1) = \beta'(1)$, then (as in Step 2) the loop $\beta \cdot \overline{\beta'}$ lies in $U$, hence null-homotopic in $X$ by goodness, so $\beta \simeq \beta'$ rel endpoints, giving $[\alpha \cdot \beta] = [\alpha \cdot \beta']$. **Evenly covered over good opens.** Give $\tilde{X}$ the topology generated by $\mathcal{B}$. To see $p^{-1}(U) = \bigsqcup U_{[\alpha]}$ is a disjoint union over distinct sheets: if $[\gamma] \in U_{[\alpha]} \cap U_{[\alpha']}$ (same $U$, different $[\alpha], [\alpha']$), then $[\gamma] = [\alpha \cdot \beta] = [\alpha' \cdot \beta']$, and by the above the set $U_{[\alpha]}$ depends only on the class $[\gamma]$ — hence $U_{[\alpha]} = U_{[\gamma]} = U_{[\alpha']}$. Thus distinct sheets (i.e. distinct sets $U_{[\alpha]}$) are disjoint. **Homeomorphism of sheets.** The map $p_U$ is bijective. It is continuous because $U_{[\alpha]}$ is a basis element mapped onto the open set $U$, and the preimage of any open $W \subseteq U$ under $p_U$ is $W_{[\alpha']}$ for an appropriate representative (using the good subset obtained by shrinking inside $U$). Its inverse $y \mapsto [\alpha \cdot \beta_y]$ (with $\beta_y$ a path in $U$ from $\alpha(1)$ to $y$) is well-defined independent of the choice of $\beta_y$ (by the collapsing argument) and continuous because a small good neighbourhood $W \subseteq U$ around $y$ maps to $W_{[\alpha \cdot \beta_y]} \subseteq U_{[\alpha]}$ under $p_U^{-1}$. Therefore $p_U$ is a homeomorphism, exhibiting $U$ as evenly covered. The good opens cover $X$, so $p: \tilde{X} \to X$ is a **covering map**.[/guided]

[step:Show $\tilde{X}$ is path-connected]Every class $[\alpha] \in \tilde{X}$ is connected by a path to $\tilde{x}_0 = [c_{x_0}]$. Given a representative path $\alpha \in [\alpha]$, define \begin{align*} \tilde{\alpha}: I &\to \tilde{X} \\ s &\mapsto [\alpha_s], \end{align*} where $\alpha_s: I \to X$ is the truncation $\alpha_s(t) := \alpha(st)$ (so $\alpha_s$ is the restriction of $\alpha$ to $[0, s]$ rescaled to $[0, 1]$). Then $\tilde{\alpha}(0) = [\alpha_0] = [c_{x_0}] = \tilde{x}_0$ and $\tilde{\alpha}(1) = [\alpha_1] = [\alpha]$, and $p \circ \tilde{\alpha} = \alpha$ (since $p([\alpha_s]) = \alpha_s(1) = \alpha(s)$). *Continuity of $\tilde{\alpha}$.* Fix $s_0 \in I$ and a basic neighbourhood $U_{[\alpha_{s_0}]}$ of $\tilde{\alpha}(s_0)$ with $U$ a good open containing $\alpha(s_0)$. By continuity of $\alpha$, there is $\varepsilon > 0$ with $\alpha(s) \in U$ for $|s - s_0| < \varepsilon$. For such $s$, the path $\beta_s(t) := \alpha(s_0 + t(s - s_0))$ is a path in $U$ from $\alpha(s_0)$ to $\alpha(s)$, and $\alpha_s \simeq \alpha_{s_0} \cdot \beta_s$ rel endpoints (the homotopy reparametrises $\alpha$ on $[0, s]$). Therefore $\tilde{\alpha}(s) = [\alpha_s] = [\alpha_{s_0} \cdot \beta_s] \in U_{[\alpha_{s_0}]}$. So $\tilde{\alpha}^{-1}(U_{[\alpha_{s_0}]})$ contains the open $\varepsilon$-ball around $s_0$, and $\tilde{\alpha}$ is continuous at $s_0$. Hence $\tilde{\alpha}$ is a path in $\tilde{X}$ from $\tilde{x}_0$ to $[\alpha]$, proving $\tilde{X}$ is path-connected.[/step]

[guided]To show $\tilde{X}$ is path-connected, it suffices to connect any point $[\alpha] \in \tilde{X}$ to $\tilde{x}_0 = [c_{x_0}]$ by a path. The natural candidate is to let a parameter $s$ sweep $\alpha$ from its start to its finish: at time $s$ we have traversed only the initial portion of $\alpha$. **Construction.** Fix a representative path $\alpha: I \to X$ from $x_0$. For $s \in [0, 1]$ define the **truncation** \begin{align*} \alpha_s: I \to X, \qquad \alpha_s(t) := \alpha(st). \end{align*} Then $\alpha_s(0) = \alpha(0) = x_0$, so $\alpha_s \in P(X, x_0)$ and $[\alpha_s] \in \tilde{X}$. At $s = 0$, $\alpha_0 \equiv x_0$ is the constant path, so $[\alpha_0] = \tilde{x}_0$. At $s = 1$, $\alpha_1 = \alpha$, so $[\alpha_1] = [\alpha]$. Define the candidate path \begin{align*} \tilde{\alpha}: I \to \tilde{X}, \qquad s \mapsto [\alpha_s]. \end{align*} Note $p(\tilde{\alpha}(s)) = \alpha_s(1) = \alpha(s)$, so $p \circ \tilde{\alpha} = \alpha$: $\tilde{\alpha}$ is a **lift** of $\alpha$. **Continuity.** Fix $s_0 \in I$. We check $\tilde{\alpha}$ is continuous at $s_0$ by showing the preimage of each basic open $U_{[\alpha_{s_0}]}$ around $\tilde{\alpha}(s_0)$ contains a neighbourhood of $s_0$. Let $U$ be a good open containing $\alpha(s_0)$. By continuity of $\alpha$, there is $\varepsilon > 0$ such that $\alpha(s) \in U$ for all $s \in (s_0 - \varepsilon, s_0 + \varepsilon) \cap I$. For such $s$, we rewrite $\alpha_s$ as a concatenation of $\alpha_{s_0}$ with a short path in $U$. Define the tail \begin{align*} \beta_s: I \to U, \qquad \beta_s(t) := \alpha(s_0 + t(s - s_0)). \end{align*} This is a path from $\alpha(s_0)$ to $\alpha(s)$ lying in $U$ (since $s$ is within $\varepsilon$ of $s_0$, the interpolants also stay within $\varepsilon$ of $s_0$ and $\alpha$ of them stay in $U$). The concatenation $\alpha_{s_0} \cdot \beta_s$ first traverses $\alpha$ on $[0, s_0]$ then on $[s_0, s]$, which is a reparametrisation of $\alpha_s$. Hence $\alpha_s \simeq \alpha_{s_0} \cdot \beta_s$ rel endpoints (see [Group Laws for Paths up to Homotopy](/theorems/1877)), so $[\alpha_s] = [\alpha_{s_0} \cdot \beta_s] \in U_{[\alpha_{s_0}]}$. We conclude $(s_0 - \varepsilon, s_0 + \varepsilon) \cap I \subseteq \tilde{\alpha}^{-1}(U_{[\alpha_{s_0}]})$, i.e. $\tilde{\alpha}$ is continuous at $s_0$. Since $s_0$ was arbitrary, $\tilde{\alpha}$ is continuous on $I$, hence a path in $\tilde{X}$ from $\tilde{x}_0$ to $[\alpha]$. This proves $\tilde{X}$ is path-connected. We have used: - **Continuity of $\alpha$** at $s_0$, which is a property of a single path. - **Existence of good opens**, which uses semi-local simple connectivity and local path-connectedness of $X$. - **Definition of $\tilde{X}$** as path-homotopy classes, which makes $\alpha_s \simeq \alpha_{s_0} \cdot \beta_s$ a consequence of [Group Laws for Paths up to Homotopy](/theorems/1877).[/guided]

[step:Show $\tilde{X}$ is simply connected]By [Characterisation of Simply Connected Spaces](/theorems/1883), it suffices to show every loop in $\tilde{X}$ at $\tilde{x}_0$ is null-homotopic. Let $\tilde{\sigma}: I \to \tilde{X}$ be a loop at $\tilde{x}_0$, and let $\sigma := p \circ \tilde{\sigma}: I \to X$ be its projection (a loop in $X$ at $x_0$). The key identification: for each $s \in I$, $\tilde{\sigma}(s) = [\sigma_s]$, where $\sigma_s(t) := \sigma(st)$. Indeed, both $s \mapsto \tilde{\sigma}(s)$ and $s \mapsto [\sigma_s]$ are paths in $\tilde{X}$ from $\tilde{x}_0$ (at $s = 0$, $\tilde{\sigma}(0) = \tilde{x}_0$ and $[\sigma_0] = [c_{x_0}] = \tilde{x}_0$) that are lifts of $\sigma$ (for the second, $p([\sigma_s]) = \sigma_s(1) = \sigma(s)$, and continuity was established in Step 4). By [Uniqueness of Lifts](/theorems/1885), applied to the connected domain $I$, the two lifts coincide. Evaluating at $s = 1$: \begin{align*} \tilde{x}_0 = \tilde{\sigma}(1) = [\sigma_1] = [\sigma]. \end{align*} Thus $[\sigma] = [c_{x_0}]$ in $\tilde{X}$, which unpacks to: the loop $\sigma$ in $X$ is path-homotopic rel endpoints to the constant path $c_{x_0}$. Choose a path-homotopy $H: I \times I \to X$ with $H(t, 0) = \sigma(t)$, $H(t, 1) = x_0$, $H(0, s) = H(1, s) = x_0$. By the [Homotopy Lifting Lemma](/theorems/1887) applied to the covering $p: \tilde{X} \to X$ and the homotopy $H$, with initial lift $\tilde{\sigma}$ (of $\sigma = H(\cdot, 0)$ starting at $\tilde{x}_0$), there exists a unique lift \begin{align*} \tilde{H}: I \times I \to \tilde{X}, \qquad \tilde{H}(t, 0) = \tilde{\sigma}(t), \quad \tilde{H}(0, s) = \tilde{x}_0, \quad p \circ \tilde{H} = H. \end{align*} At $s = 1$, the map $t \mapsto \tilde{H}(t, 1)$ is a lift of the constant loop $t \mapsto x_0$ starting at $\tilde{x}_0$; by [Uniqueness of Lifts](/theorems/1885), it is constantly $\tilde{x}_0$. Moreover, the loop side $t = 1$: $s \mapsto \tilde{H}(1, s)$ is a lift of the constant path $s \mapsto x_0$ starting at $\tilde{\sigma}(1) = \tilde{x}_0$; by the same uniqueness, it is constantly $\tilde{x}_0$. So $\tilde{H}$ is a path-homotopy in $\tilde{X}$ from $\tilde{\sigma}$ to the constant loop at $\tilde{x}_0$, rel endpoints. Hence $[\tilde{\sigma}] = [c_{\tilde{x}_0}]$ in $\pi_1(\tilde{X}, \tilde{x}_0)$, and $\pi_1(\tilde{X}, \tilde{x}_0) = \{e\}$.[/step]

[guided]To show $\tilde{X}$ is simply connected, we show every loop in $\tilde{X}$ at $\tilde{x}_0$ is null-homotopic. This uses simple connectivity of $\tilde{X}$, not of $X$ — so where does the argument get its traction? From the definition of $\tilde{X}$ itself: its points are homotopy classes in $X$, and a loop in $\tilde{X}$ corresponds to a loop in $X$ whose truncations already represent the moving point. **Setting up the loop.** Let $\tilde{\sigma}: I \to \tilde{X}$ be a loop at $\tilde{x}_0$, and set $\sigma := p \circ \tilde{\sigma}$. Then $\sigma$ is a loop in $X$ at $x_0$ (since $p(\tilde{x}_0) = x_0$ and $p$ is a covering hence continuous). **Key identification.** We claim $\tilde{\sigma}(s) = [\sigma_s]$ for all $s$, where $\sigma_s(t) = \sigma(st)$ is the truncation. *Proof of claim.* Both $s \mapsto \tilde{\sigma}(s)$ and $s \mapsto [\sigma_s]$ are maps $I \to \tilde{X}$ with the following properties: 1. Both start at $\tilde{x}_0$: $\tilde{\sigma}(0) = \tilde{x}_0$ (it is a loop at $\tilde{x}_0$) and $[\sigma_0] = [c_{x_0}] = \tilde{x}_0$. 2. Both are continuous: $\tilde{\sigma}$ by assumption, and $s \mapsto [\sigma_s]$ by the continuity argument of Step 4 applied to the path $\sigma$. 3. Both are lifts of $\sigma$: $p \circ \tilde{\sigma} = \sigma$ by definition of $\sigma$, and $p([\sigma_s]) = \sigma_s(1) = \sigma(s)$. By [Uniqueness of Lifts](/theorems/1885), applied to the connected domain $I$ and the covering $p$, two continuous lifts of $\sigma$ agreeing at $s = 0$ agree everywhere. Hence $\tilde{\sigma}(s) = [\sigma_s]$ for all $s$. **Consequence at $s = 1$.** Since $\tilde{\sigma}$ is a loop, $\tilde{\sigma}(1) = \tilde{x}_0$. But by the identification, $\tilde{\sigma}(1) = [\sigma_1] = [\sigma]$. So \begin{align*} [\sigma] = \tilde{x}_0 = [c_{x_0}] \quad \text{in } \tilde{X}. \end{align*} Unravelling the definition of $\tilde{X}$: this says the loop $\sigma$ in $X$ is path-homotopic rel endpoints to the constant path $c_{x_0}$ in $X$. **Lifting the null-homotopy.** Let $H: I \times I \to X$ be a path-homotopy from $\sigma$ to $c_{x_0}$: continuous with $H(t, 0) = \sigma(t), H(t, 1) = x_0, H(0, s) = H(1, s) = x_0$. By the [Homotopy Lifting Lemma](/theorems/1887) applied to the covering $p$ and the homotopy $H$, with initial lift $\tilde{\sigma}$ of $H(\cdot, 0) = \sigma$ starting at $\tilde{x}_0$, there is a unique continuous $\tilde{H}: I \times I \to \tilde{X}$ with \begin{align*} p \circ \tilde{H} = H, \qquad \tilde{H}(\cdot, 0) = \tilde{\sigma}, \qquad \tilde{H}(0, s) = \tilde{x}_0. \end{align*} Is $\tilde{H}$ a homotopy rel endpoints in $\tilde{X}$? We check the three remaining boundary conditions. - $s \mapsto \tilde{H}(0, s)$: this is the constant $\tilde{x}_0$, by the initial lift condition. - $s \mapsto \tilde{H}(1, s)$: $p \circ (\tilde{H}(1, \cdot)) = H(1, \cdot) = x_0$ (constant), so $\tilde{H}(1, \cdot)$ is a lift of a constant path. It starts at $\tilde{H}(1, 0) = \tilde{\sigma}(1) = \tilde{x}_0$. By [Uniqueness of Lifts](/theorems/1885), a lift of a constant path with specified starting point is constant — so $\tilde{H}(1, s) = \tilde{x}_0$ for all $s$. - $t \mapsto \tilde{H}(t, 1)$: $p \circ \tilde{H}(\cdot, 1) = H(\cdot, 1) = c_{x_0}$ is the constant $x_0$. Starts at $\tilde{H}(0, 1) = \tilde{x}_0$. By [Uniqueness of Lifts](/theorems/1885), $\tilde{H}(t, 1) = \tilde{x}_0$ for all $t$. Therefore $\tilde{H}$ is a path-homotopy from $\tilde{\sigma}$ to the constant loop $c_{\tilde{x}_0}$, rel endpoints, in $\tilde{X}$. So $[\tilde{\sigma}] = [c_{\tilde{x}_0}]$ in $\pi_1(\tilde{X}, \tilde{x}_0)$. Since $\tilde{\sigma}$ was arbitrary, $\pi_1(\tilde{X}, \tilde{x}_0) = \{e\}$. By [Characterisation of Simply Connected Spaces](/theorems/1883), $\tilde{X}$ is simply connected.[/guided]

[step:Assemble: $\tilde{X}$ is a universal cover] By Step 1, $p: \tilde{X} \to X$ is a well-defined map. By Step 3, $p$ is a covering map. By Step 4, $\tilde{X}$ is path-connected. By Step 5, $\tilde{X}$ is simply connected. A covering map with path-connected, simply connected total space is by definition a **universal cover**. Therefore $X$ admits a universal cover, completing the proof. [/step]