[proofplan] The proof is a compactness-plus-uniqueness argument. We first lift $H$ locally: for each point $(y_0, t_0) \in Y \times I$, the Lebesgue number lemma applied to a cover of $\{y_0\} \times I$ by preimages of evenly covered neighbourhoods in $X$ produces a product neighbourhood $N \times I$ of $\{y_0\} \times I$ that is partitioned into finitely many slabs $N \times [t_{i-1}, t_i]$, each of which maps under $H$ into an evenly covered open set. On each slab we lift inductively using the [local homeomorphism property of covering maps](/theorems/???), matching boundaries to preserve continuity. Uniqueness of lifts starting at a prescribed point is used at every boundary to glue the local lifts into a consistent map on $N \times I$. Finally, uniqueness lets the local lifts agree on overlaps, so they assemble into a global lift $\tilde{H}$ on $Y \times I$. [/proofplan]

[step:Reduce the problem to lifting on a single tube $\{y_0\} \times I$ at a time] Fix $y_0 \in Y$. We construct a neighbourhood $N = N(y_0) \subseteq Y$ and a continuous lift \begin{align*} \tilde{H}_N: N \times I &\to \tilde{X} \end{align*} such that $p \circ \tilde{H}_N = H|_{N \times I}$ and $\tilde{H}_N(-, 0) = \tilde{f}_0|_N$. Once this is done for each $y_0 \in Y$, the local lifts agree on overlaps by the uniqueness-of-lifts principle proved in Step 4 below, and therefore glue to a global continuous map $\tilde{H}: Y \times I \to \tilde{X}$ with the required properties. [/step]

[step:Partition the interval using Lebesgue's number lemma on $\{y_0\} \times I$]Since $p: \tilde{X} \to X$ is a covering map, each point $x \in X$ has an open neighbourhood that is evenly covered by $p$. The collection \begin{align*} \mathcal{U} = \{U \subseteq X : U \text{ is open and evenly covered by } p\} \end{align*} is an open cover of $X$, so $\{H^{-1}(U) : U \in \mathcal{U}\}$ is an open cover of $Y \times I$. The fibre $\{y_0\} \times I$ is compact (homeomorphic to $I = [0, 1]$), so this cover restricts to an open cover of $\{y_0\} \times I$. For each $t \in I$ choose an evenly covered open $U_t \ni H(y_0, t)$ and an open product box $V_t \times W_t \subseteq Y \times I$ with $(y_0, t) \in V_t \times W_t \subseteq H^{-1}(U_t)$. The sets $\{V_t \times W_t\}_{t \in I}$ cover $\{y_0\} \times I$. Extracting a finite subcover and taking the intersection of the $V$-factors, we obtain an open neighbourhood $N \ni y_0$ in $Y$ and a partition \begin{align*} 0 = t_0 < t_1 < \dots < t_k = 1 \end{align*} of $I$ such that for each $i = 1, \dots, k$ there is an evenly covered open set $U_i \subseteq X$ with \begin{align*} H(N \times [t_{i-1}, t_i]) \subseteq U_i. \end{align*}[/step]

[guided]We need to lift $H$ on a product neighbourhood $N \times I$ of $\{y_0\} \times I$, but the covering property is local in $X$: we only know how to lift into $\tilde{X}$ when the image lies inside a single evenly covered open set. The Lebesgue number lemma is the standard tool for upgrading a pointwise covering condition to a uniform one on a compact set. Concretely: $\{y_0\} \times I \cong I$ is compact and Hausdorff, and the preimages $H^{-1}(U)$ (over evenly covered $U$) cover it. By compactness we can find finitely many product boxes $V_j \times W_j$ whose union contains $\{y_0\} \times I$, with each $H(V_j \times W_j)$ lying inside a single evenly covered set. Taking the $V$-factor intersection gives a uniform neighbourhood $N$ of $y_0$ that works across the whole interval; refining the partition of $I$ so that each slab $N \times [t_{i-1}, t_i]$ fits into one of the $V_j \times W_j$ boxes (equivalently, one of the $H^{-1}(U)$) gives the slab structure. The upshot is: we have reduced the global lifting problem on the tube $N \times I$ to finitely many local lifting problems, one per slab, where each slab maps into a single evenly covered set.[/guided]

[step:Lift slab by slab using local homeomorphisms over evenly covered sets]We construct continuous maps $\tilde{H}_i: N \times [t_{i-1}, t_i] \to \tilde{X}$ inductively, satisfying \begin{align*} p \circ \tilde{H}_i &= H|_{N \times [t_{i-1}, t_i]}, \\ \tilde{H}_1(y, t_0) &= \tilde{f}_0(y) \quad \text{for all } y \in N, \\ \tilde{H}_i(y, t_{i-1}) &= \tilde{H}_{i-1}(y, t_{i-1}) \quad \text{for all } y \in N,\ i \ge 2. \end{align*} **Base case $i = 1$.** Since $U_1$ is evenly covered, write \begin{align*} p^{-1}(U_1) = \bigsqcup_{\alpha \in A_1} \tilde{U}_{1,\alpha} \end{align*} as a disjoint union of open sets, each mapped homeomorphically onto $U_1$ by $p$. By continuity of $\tilde{f}_0$ and the fact that $\tilde{f}_0(y_0) \in p^{-1}(x_0) \cap p^{-1}(U_1)$ (because $x_0 = H(y_0, 0) \in U_1$), after shrinking $N$ to a smaller open neighbourhood of $y_0$ if necessary, we may assume \begin{align*} \tilde{f}_0(N) \subseteq \tilde{U}_{1,\alpha_1} \end{align*} for a single sheet $\tilde{U}_{1,\alpha_1}$. Let $s_1 := (p|_{\tilde{U}_{1,\alpha_1}})^{-1}: U_1 \to \tilde{U}_{1,\alpha_1}$ be the inverse homeomorphism (a continuous local section of $p$). Define \begin{align*} \tilde{H}_1: N \times [t_0, t_1] &\to \tilde{X}, \\ (y, t) &\mapsto s_1(H(y, t)). \end{align*} Then $p \circ \tilde{H}_1 = p \circ s_1 \circ H = H$ on $N \times [t_0, t_1]$, and $\tilde{H}_1(y, 0) = s_1(H(y, 0)) = s_1(f_0(y))$. We also have $\tilde{f}_0(y) \in \tilde{U}_{1,\alpha_1}$ and $p(\tilde{f}_0(y)) = f_0(y)$, so $\tilde{f}_0(y) = s_1(f_0(y))$ because $s_1$ is the unique right inverse of $p$ landing in $\tilde{U}_{1,\alpha_1}$. Hence $\tilde{H}_1(y, 0) = \tilde{f}_0(y)$ on $N$. **Inductive step $i \ge 2$.** Suppose $\tilde{H}_{i-1}$ has been constructed on $N \times [t_{i-2}, t_{i-1}]$. The point $\tilde{H}_{i-1}(y_0, t_{i-1}) \in p^{-1}(U_i)$, and \begin{align*} p^{-1}(U_i) = \bigsqcup_{\alpha \in A_i} \tilde{U}_{i,\alpha} \end{align*} is a disjoint union of sheets. Let $\tilde{U}_{i,\alpha_i}$ be the sheet containing $\tilde{H}_{i-1}(y_0, t_{i-1})$. By continuity of $\tilde{H}_{i-1}$, after shrinking $N$ to a smaller open neighbourhood of $y_0$ if necessary, we may assume \begin{align*} \tilde{H}_{i-1}(N \times \{t_{i-1}\}) \subseteq \tilde{U}_{i,\alpha_i}. \end{align*} Let $s_i := (p|_{\tilde{U}_{i,\alpha_i}})^{-1}: U_i \to \tilde{U}_{i,\alpha_i}$ be the local section, and define \begin{align*} \tilde{H}_i: N \times [t_{i-1}, t_i] &\to \tilde{X}, \\ (y, t) &\mapsto s_i(H(y, t)). \end{align*} Then $p \circ \tilde{H}_i = H$ on $N \times [t_{i-1}, t_i]$. At $t = t_{i-1}$, \begin{align*} \tilde{H}_i(y, t_{i-1}) = s_i(H(y, t_{i-1})) = s_i(p(\tilde{H}_{i-1}(y, t_{i-1}))) = \tilde{H}_{i-1}(y, t_{i-1}), \end{align*} where the last equality holds because $\tilde{H}_{i-1}(y, t_{i-1}) \in \tilde{U}_{i,\alpha_i}$ and $s_i$ is the inverse of $p$ on that sheet.[/step]

[guided]On each slab $N \times [t_{i-1}, t_i]$ the image under $H$ lies in an evenly covered open set $U_i$. By definition of "evenly covered", $p^{-1}(U_i)$ decomposes as a disjoint union of sheets, each homeomorphic to $U_i$ via $p$. Lifting a map into $U_i$ to a map into $\tilde{X}$ is therefore a finite choice: we must choose which sheet to land in, and once chosen, the lift is uniquely determined as $s_i \circ H$ where $s_i$ is the inverse homeomorphism on that sheet. The choice of sheet is forced by two continuity constraints. On the first slab ($i = 1$) the lift at $t = 0$ must agree with $\tilde{f}_0$, which is continuous — so $\tilde{f}_0(N)$ lies in a single sheet after shrinking $N$ (a connected image cannot straddle the disjoint open sheets). This fixes $\alpha_1$. On subsequent slabs the lift at $t = t_{i-1}$ must agree with the previously built $\tilde{H}_{i-1}$ on the slice $N \times \{t_{i-1}\}$, whose image is continuous and hence lies in a single sheet after shrinking $N$ again. This fixes $\alpha_i$. Why do sheets never collide? Because the $\tilde{U}_{i,\alpha}$ are pairwise disjoint open sets of $\tilde{X}$. Continuity of the already-defined lift prevents jumping between sheets, and the section $s_i$ is continuous because it is the inverse of the local homeomorphism $p|_{\tilde{U}_{i,\alpha_i}}$. Pasting $\tilde{H}_i$ to $\tilde{H}_{i-1}$ at $t = t_{i-1}$ works because they agree on the overlap $N \times \{t_{i-1}\}$; continuity of the pasted map follows from the [gluing lemma](/theorems/1871) applied to the closed cover $\{N \times [t_{i-2}, t_{i-1}],\ N \times [t_{i-1}, t_i]\}$ of $N \times [t_{i-2}, t_i]$. We may shrink $N$ a finite number of times (once per slab); after $k$ shrinkings $N$ is still an open neighbourhood of $y_0$, so no finiteness concern arises.[/guided]

[step:Glue the slab lifts into a single continuous lift on $N \times I$ via the gluing lemma] After the $k$ inductive steps, we have continuous maps $\tilde{H}_i: N \times [t_{i-1}, t_i] \to \tilde{X}$ that agree on adjacent boundaries $N \times \{t_{i-1}\}$. Define \begin{align*} \tilde{H}_N: N \times I &\to \tilde{X} \end{align*} by $\tilde{H}_N(y, t) = \tilde{H}_i(y, t)$ for $t \in [t_{i-1}, t_i]$. This is well-defined because the $\tilde{H}_i$ agree on the shared boundaries. The cover $\{N \times [t_{i-1}, t_i]\}_{i=1}^k$ is a finite closed cover of $N \times I$, so by the [gluing lemma for closed covers](/theorems/1871), $\tilde{H}_N$ is continuous. It satisfies $p \circ \tilde{H}_N = H|_{N \times I}$ and $\tilde{H}_N(-, 0) = \tilde{f}_0|_N$ by construction. [/step]

[step:Prove uniqueness of the lift on each vertical fibre $\{y\} \times I$] We now prove the following uniqueness statement, which powers both the well-definedness of the gluing across different base points $y_0 \in Y$ and the uniqueness part of the theorem: [claim:Unique lift along a single interval] Let $q: E \to B$ be a covering map and $\gamma: I \to B$ a path. If $\tilde{\gamma}_1, \tilde{\gamma}_2: I \to E$ are continuous lifts of $\gamma$ with $\tilde{\gamma}_1(0) = \tilde{\gamma}_2(0)$, then $\tilde{\gamma}_1 = \tilde{\gamma}_2$. [/claim] [proof] Let $S = \{t \in I : \tilde{\gamma}_1(t) = \tilde{\gamma}_2(t)\}$. We show $S = I$ by connectedness of $I$. *$S$ is non-empty.* $0 \in S$ by hypothesis. *$S$ is open in $I$.* Let $t_0 \in S$, so $\tilde{\gamma}_1(t_0) = \tilde{\gamma}_2(t_0) =: e_0$. Let $U \ni \gamma(t_0)$ be evenly covered, let $\tilde{U} \ni e_0$ be the sheet of $q^{-1}(U)$ containing $e_0$, and let $s = (q|_{\tilde{U}})^{-1}: U \to \tilde{U}$. By continuity of $\tilde{\gamma}_1, \tilde{\gamma}_2$, there is a neighbourhood $J \subseteq I$ of $t_0$ with $\tilde{\gamma}_j(J) \subseteq \tilde{U}$ for $j = 1, 2$. Then $\tilde{\gamma}_j|_J = s \circ \gamma|_J$ (since $s$ is the unique right inverse of $q$ on $\tilde{U}$), so $\tilde{\gamma}_1|_J = \tilde{\gamma}_2|_J$ and $J \subseteq S$. *$S$ is closed in $I$.* Let $t_0 \in I \setminus S$. Then $\tilde{\gamma}_1(t_0) \ne \tilde{\gamma}_2(t_0)$, but $q(\tilde{\gamma}_1(t_0)) = q(\tilde{\gamma}_2(t_0)) = \gamma(t_0)$. Let $U \ni \gamma(t_0)$ be evenly covered, and let $\tilde{U}_1, \tilde{U}_2$ be the (distinct) sheets of $q^{-1}(U)$ containing $\tilde{\gamma}_1(t_0)$ and $\tilde{\gamma}_2(t_0)$ respectively. By continuity there is a neighbourhood $J \subseteq I$ of $t_0$ with $\tilde{\gamma}_j(J) \subseteq \tilde{U}_j$ for $j = 1, 2$. Since $\tilde{U}_1 \cap \tilde{U}_2 = \varnothing$, $\tilde{\gamma}_1(t) \ne \tilde{\gamma}_2(t)$ for every $t \in J$, so $J \subseteq I \setminus S$. By connectedness of $I$, $S$ is either empty or all of $I$; since $0 \in S$, we conclude $S = I$, i.e., $\tilde{\gamma}_1 = \tilde{\gamma}_2$. [/proof] [/step]

[step:Glue local lifts over varying base points into a global lift $\tilde{H}: Y \times I \to \tilde{X}$] The construction of Step 2 through Step 4 produces, for each $y_0 \in Y$, an open neighbourhood $N(y_0) \subseteq Y$ and a continuous lift $\tilde{H}_{N(y_0)}: N(y_0) \times I \to \tilde{X}$ with $p \circ \tilde{H}_{N(y_0)} = H$ and $\tilde{H}_{N(y_0)}(-, 0) = \tilde{f}_0|_{N(y_0)}$. *Local lifts agree on overlaps.* Suppose $y \in N(y_0) \cap N(y_0')$ for two base points $y_0, y_0' \in Y$. Restrict both lifts to the fibre $\{y\} \times I$: \begin{align*} \tilde{H}_{N(y_0)}(y, \cdot), \ \tilde{H}_{N(y_0')}(y, \cdot): I \to \tilde{X} \end{align*} are both continuous lifts of the path $H(y, \cdot): I \to X$, and both start at $\tilde{f}_0(y)$ when $t = 0$. By the [Claim above], they agree on all of $I$. *Defining $\tilde{H}$.* Set \begin{align*} \tilde{H}: Y \times I &\to \tilde{X}, \\ (y, t) &\mapsto \tilde{H}_{N(y_0)}(y, t) \quad \text{for any } y_0 \text{ with } y \in N(y_0). \end{align*} The previous paragraph shows this is well-defined. Continuity is local: each point $(y, t) \in Y \times I$ has the open neighbourhood $N(y) \times I$ on which $\tilde{H} = \tilde{H}_{N(y)}$, which is continuous. So $\tilde{H}$ is continuous. By construction, $p \circ \tilde{H} = H$ and $\tilde{H}(-, 0) = \tilde{f}_0$. [/step]

[step:Deduce uniqueness of $\tilde{H}$ from the interval uniqueness claim] Suppose $\tilde{H}'$ is another continuous lift with $p \circ \tilde{H}' = H$ and $\tilde{H}'(-, 0) = \tilde{f}_0$. Fix $y \in Y$ and consider the two lifts of $H(y, \cdot): I \to X$ given by \begin{align*} \tilde{H}(y, \cdot), \ \tilde{H}'(y, \cdot): I \to \tilde{X}. \end{align*} Both are continuous and start at $\tilde{f}_0(y)$. By the Claim, $\tilde{H}(y, \cdot) = \tilde{H}'(y, \cdot)$. Since $y \in Y$ was arbitrary, $\tilde{H} = \tilde{H}'$. This completes the proof of the Homotopy Lifting Lemma. [/step]