Local path-connectedness lifts and descends along covering maps

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

A covering map is a continuous surjection $p:E\to B$ such that every $b\in B$ has an open neighbourhood $U$ for which $p^{-1}(U)$ is a disjoint union of open sets $V_j$, called sheets, and each restriction $p{\mathrm{\mid }}_{V_j}:V_j\to U$ is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a $U$ is evenly covered, and $p^{-1}(b)$ is the fibre over $b$. A covering is trivial when it is isomorphic over $B$ to a product projection $B\times F\to B$ with $F$ discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

Let $(X,\mathcal{T})$ be a topological space (def-topological-space) and let $x\in X$. Subsets carry the subspace topology (def-subspace-topology-top); connectedness is def-connected-space and path-connectedness is def-path-connected. $X$ is locally connected at $x$ when for every open $U$ with $x\in U$ there is an open connected $V$ with $x\in V\subseteq U$, and locally connected when this holds at every point; $X$ is locally path-connected at $x$ when for every open $U$ with $x\in U$ there is an open path-connected $V$ with $x\in V\subseteq U$, and locally path-connected when this holds at every point. (Locally connected and locally path-connected spaces: a neighbourhood base of open connected, respectively open path-connected, sets at every point).

Let $(X,{\mathcal{T}}_X)$ and $(Y,{\mathcal{T}}_Y)$ be topological spaces and let $f:X\to Y$ be a function. Continuity is as in def-continuous-map-top, injections, surjections and bijections as in def-injection-surjection-bijection. $f$ is an open map if $f[U]$ is open in $Y$ for every open $U\subseteq X$, a closed map if $f[F]$ is closed in $Y$ for every closed $F\subseteq X$, and a homeomorphism if $f$ is a continuous bijection whose inverse $f^{-1}:Y\to X$ is also continuous; the spaces are homeomorphic when such an $f$ exists. (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological).