[proofplan] The argument has a single engine: the [Homotopy Lifting Lemma](/theorems/1887), which produces a lift $\tilde{H}: I \times I \to \tilde{X}$ of the given path homotopy $H$ with prescribed bottom edge $\tilde{\gamma}$. The work is then to check that $\tilde{H}$ is actually a path homotopy — i.e., that its top edge is $\tilde{\gamma}'$ and its vertical edges are constant paths. Each of these checks reduces to a uniqueness-of-lifts argument: the sides and top of $\tilde{H}$ are lifts of known paths (including constant paths) starting from known points, so they are determined by those starting points and must equal $\tilde{\gamma}'$, $c_{\tilde{x}_0}$, or $c_{\tilde{x}_1}$ respectively. [/proofplan] [step:Lift the path homotopy $H$ using the Homotopy Lifting Lemma] Since $\gamma, \gamma': I \to X$ are homotopic as paths (rel endpoints), there exists a continuous map \begin{align*} H: I \times I &\to X \end{align*} with $H(-, 0) = \gamma$, $H(-, 1) = \gamma'$, $H(0, s) = x_0$ for all $s \in I$, and $H(1, s) = x_1$ for all $s \in I$. Writing $I \times I$ as $Y \times I$ with $Y = I$, and viewing $H$ as a homotopy from $H(-, 0) = \gamma$ to $H(-, 1) = \gamma'$, we apply the [Homotopy Lifting Lemma](/theorems/1887). The hypotheses are verified: - $p: \tilde{X} \to X$ is a covering map (given). - $H: I \times I \to X$ is a continuous homotopy. - $\tilde{\gamma}: I \to \tilde{X}$ is a lift of $H(-, 0) = \gamma$. The lemma produces a unique continuous map \begin{align*} \tilde{H}: I \times I &\to \tilde{X} \end{align*} satisfying $\tilde{H}(-, 0) = \tilde{\gamma}$ and $p \circ \tilde{H} = H$. [/step] [step:Identify the left edge of $\tilde{H}$ as the constant path at $\tilde{x}_0$] Consider the restriction \begin{align*} \tilde{H}(0, \cdot): I &\to \tilde{X}, \\ s &\mapsto \tilde{H}(0, s). \end{align*} It is continuous, and $p(\tilde{H}(0, s)) = H(0, s) = x_0$ for every $s \in I$, so $\tilde{H}(0, \cdot)$ is a lift of the constant path $c_{x_0}: I \to X$. Its starting value is \begin{align*} \tilde{H}(0, 0) = \tilde{\gamma}(0) = \tilde{x}_0. \end{align*} Now the constant path at $\tilde{x}_0$, \begin{align*} c_{\tilde{x}_0}: I \to \tilde{X}, \quad s \mapsto \tilde{x}_0, \end{align*} is also a continuous lift of $c_{x_0}$ starting at $\tilde{x}_0$. By the unique-lift-along-an-interval property of covering maps (established as a Claim inside the proof of the [Homotopy Lifting Lemma](/theorems/1887)), two continuous lifts of a path that agree at $t = 0$ are equal. Therefore \begin{align*} \tilde{H}(0, s) = \tilde{x}_0 \quad \text{for all } s \in I. \end{align*} [guided] We want the homotopy $\tilde{H}$ in $\tilde{X}$ to be a **path** homotopy, not just a homotopy. Path homotopy requires the left and right vertical edges to be constant. The left edge $\tilde{H}(0, \cdot)$ projects under $p$ to $H(0, \cdot) = c_{x_0}$, so it is some lift of $c_{x_0}$. Which one? Only the starting point identifies it: $\tilde{H}(0, 0) = \tilde{\gamma}(0) = \tilde{x}_0$ by the condition $\tilde{H}(-, 0) = \tilde{\gamma}$. Two continuous lifts of the same path that start at the same point are equal — this is the uniqueness-of-lifts claim proved as part of the Homotopy Lifting Lemma. The constant lift $c_{\tilde{x}_0}$ is an obvious candidate lift of $c_{x_0}$ starting at $\tilde{x}_0$, so it must be the lift: $\tilde{H}(0, s) = \tilde{x}_0$ for every $s$. The underlying principle: a covering map is a local homeomorphism, and a path cannot move between disconnected sheets of a fibre. So a lift of a constant path — whose image is a single point, hence a single fibre — must itself be constant. [/guided] [/step] [step:Identify the right edge of $\tilde{H}$ as a constant path] Apply the same argument to the right edge: \begin{align*} \tilde{H}(1, \cdot): I \to \tilde{X}, \quad s \mapsto \tilde{H}(1, s). \end{align*} For every $s \in I$, $p(\tilde{H}(1, s)) = H(1, s) = x_1$, so $\tilde{H}(1, \cdot)$ is a continuous lift of $c_{x_1}: I \to X$. Set $\tilde{x}_1 := \tilde{H}(1, 0) = \tilde{\gamma}(1) \in p^{-1}(x_1)$. The constant path $c_{\tilde{x}_1}: I \to \tilde{X}$ is also a continuous lift of $c_{x_1}$ starting at $\tilde{x}_1$, so by the same uniqueness-of-lifts property, \begin{align*} \tilde{H}(1, s) = \tilde{x}_1 \quad \text{for all } s \in I. \end{align*} [/step] [step:Identify the top edge of $\tilde{H}$ as $\tilde{\gamma}'$] Consider \begin{align*} \tilde{H}(-, 1): I \to \tilde{X}, \quad t \mapsto \tilde{H}(t, 1). \end{align*} It is continuous, and for every $t \in I$, $p(\tilde{H}(t, 1)) = H(t, 1) = \gamma'(t)$, so $\tilde{H}(-, 1)$ is a continuous lift of $\gamma'$. Its starting value is \begin{align*} \tilde{H}(0, 1) = \tilde{x}_0 \end{align*} by Step 2. The given lift $\tilde{\gamma}': I \to \tilde{X}$ of $\gamma'$ also starts at $\tilde{x}_0$ by hypothesis. By the uniqueness-of-lifts property, \begin{align*} \tilde{H}(-, 1) = \tilde{\gamma}'. \end{align*} In particular, $\tilde{\gamma}'(1) = \tilde{H}(1, 1) = \tilde{x}_1 = \tilde{\gamma}(1)$. [guided] The top edge $\tilde{H}(-, 1)$ projects to $\gamma'$ and is therefore a lift of $\gamma'$. The theorem's hypothesis gives us a specific lift of $\gamma'$ in mind, namely $\tilde{\gamma}'$, which starts at $\tilde{x}_0$. If we can show the top edge also starts at $\tilde{x}_0$, uniqueness of lifts forces the two to coincide. The top edge starts at $\tilde{H}(0, 1)$. This is the top-left corner of the square $I \times I$. We computed the entire left edge in Step 2: $\tilde{H}(0, \cdot) \equiv \tilde{x}_0$. In particular the corner value is $\tilde{x}_0$, matching $\tilde{\gamma}'(0) = \tilde{x}_0$. So uniqueness applies and $\tilde{H}(-, 1) = \tilde{\gamma}'$. A consequence drops out for free: the endpoint $\tilde{\gamma}'(1)$ equals the top-right corner $\tilde{H}(1, 1)$, which by Step 3 is $\tilde{x}_1 = \tilde{\gamma}(1)$. This is the "In particular" statement of the theorem — both lifts arrive at the same point in the fibre over $x_1$. [/guided] [/step] [step:Assemble the path homotopy from $\tilde{\gamma}$ to $\tilde{\gamma}'$] Combining Steps 1-4, we have constructed a continuous map $\tilde{H}: I \times I \to \tilde{X}$ satisfying: \begin{align*} \tilde{H}(-, 0) &= \tilde{\gamma} && \text{(Step 1)}, \\ \tilde{H}(-, 1) &= \tilde{\gamma}' && \text{(Step 4)}, \\ \tilde{H}(0, s) &= \tilde{x}_0 \quad \text{for all } s \in I && \text{(Step 2)}, \\ \tilde{H}(1, s) &= \tilde{x}_1 \quad \text{for all } s \in I && \text{(Step 3)}. \end{align*} This is exactly the definition of a path homotopy from $\tilde{\gamma}$ to $\tilde{\gamma}'$ in $\tilde{X}$ (rel endpoints $\tilde{x}_0, \tilde{x}_1$). The "in particular" statement $\tilde{\gamma}(1) = \tilde{\gamma}'(1) = \tilde{x}_1$ was established in Step 4. This completes the proof. [/step]