 Homotopy lifting theorem for a covering map

A homotopy into the base of a covering space has a unique continuous lift once its initial map is continuously lifted. Local inverse sheets construct the lift along each time interval, and compactness of that interval permits a finite subdivision locally around each point of the homotopy's parameter space. Uniqueness on overlapping intervals follows from path lifting theorem uniqueness. In a homotopy of paths with endpoints fixed, a chosen lifted endpoint remains fixed because it varies continuously in a discrete fiber.