Existence and uniqueness of path lifts through a covering map

Given: The objects, hypotheses, and choice principles stated above.

Let $p:E\to B$ be a covering and $f:Y\to B$ continuous. A lift of $f$ through $p$ is a continuous map $\tilde{f}:Y\to E$ with $p\circ \tilde{f}=f$. This includes lifts of paths $I\to B$ and of homotopies $Y\times I\to B$; an initial lift prescribes the restriction at time $0$ (def-homotopy-relative-and-path-homotopy, def-path-connected). (Lifts of maps, paths, and homotopies through a covering map).

Let $(X,d)$ be a compact metric space (def-metric-compactness, def-metric-space) and let $\mathcal{U}$ be an open cover of $X$. Then there is a real $\delta >0$, a Lebesgue number for $\mathcal{U}$, such that every nonempty $A\subseteq X$ with $\mathrm{diam}(A)<\delta$ (def-metric-bounded-diameter) satisfies $A\subseteq U$ for some $U\in \mathcal{U}$. Diameters of nonempty subsets of $X$ are defined because a compact space is bounded (thm-compact-subset-is-closed-and-bounded) and a subset of a bounded set is bounded. No choice principle is used. (Every open cover of a compact metric space has a Lebesgue number: a $\delta >0$ such that every nonempty subset of diameter less than $\delta$ lies inside a single member of the cover).

Let $X$, $Y$ and $Z$ be topological spaces, with subspaces carrying the subspace topology (def-subspace-topology-top). Then: 1. Composites. If $f:X\to Y$ and $g:Y\to Z$ are continuous (def-continuous-map-top) then $g\circ f:X\to Z$ is continuous. 2. Open cover. Let $f:X\to Y$ be a function and let $\{U_i:i\in I\}$ be a family of open subsets of $X$ with ${\bigcup }_{i\in I}{U}_i=X$. If $f{\mathrm{\mid }}_{U_i}:U_i\to Y$ is continuous for every $i\in I$, then $f$ is continuous. 3. Finite closed cover. Let $f:X\to Y$ be a function, let $n\ge 1$ and let $F_1,\dots ,F_n$ be closed subsets of $X$ with $F_1\cup \cdots \cup F_n=X$. If $f{\mathrm{\mid }}_{F_k}:F_k\to Y$ is continuous for every $k$, then $f$ is continuous. The converses of claims 2 and 3 hold with no hypothesis on the cover at all: every restriction of a continuous map to a subspace is continuous (def-subspace-topology-top). The finiteness in claim 3 is not removable; see the remarks. (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous).

Let $(X,\mathcal{T})$ be a topological space (def-topological-space). An open cover of $(X,\mathcal{T})$ is a family $\mathcal{U}\subseteq \mathcal{T}$ of open sets with $X=\bigcup \mathcal{U}$; a subcover of $\mathcal{U}$ is a subfamily that is itself an open cover; and $(X,\mathcal{T})$ is compact when every open cover of it has a finite subcover. (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).