Let be a covering map,
Let be a homotopy from to
Let be a Lift of
Then there exists a unique homotopy such that

Proof

Let be an open cover of by evenly covered sets.
Say , with a homeomorphism

Fix .
By Lebesgue number lemma applied to ,
there is some st for some .
Furthermore, due to compactness of
we know that there is some open (a nbd of ),
such that

Why?

Idea is, take open in ,
so it is open in product topology,
so it is a union of where is open in ,
and is open in (interval).
Then take all the pairs that contain for some number .
Those will induce an open cover on the interval,
hence take the finite subcover,
and intersect the corresponding open sets in

Now set .
Finally, take such that , and set .

Step 1

Now and
Then we can set:

and note that agrees with on .

Step 2

Proceed iteratively, now using instead of (note that our and stay valid throughout)
Upshot:
Get map lifting and extending

Check

Lifts need to agree on ?
By Uniqueness of Lifts Lemma, they must agree on an open and closed subset of .
By construction, they agree on
So they have to agree on all of
eg by considering that they agree on (for each )
and are all connected.

Corollaries

Path Lifting Lemma
Path Push Forward Bijection Proposition

Covering Fundamental groups