Homotopy Lifting Property

Theorem

Let \(p:\widetilde X\to X\) be a covering space. If \(f_t:Y\to X\) is a homotopy in the base and \(\widetilde f_0:Y\to \widetilde X\) is a lift of \(f_0:Y\to X\), then there is a unique homotopy \(\widetilde f_t:Y\to \widetilde X\) which lifts \(f_t\).