A connected covering of a locally path-connected simply connected space is one-sheeted and trivial

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

For a covering $p:E\to B$, the total space $E$ is locally path-connected if and only if the base $B$ is locally path-connected. (Local path-connectedness lifts and descends along covering maps).

Endpoint-fixed homotopic paths in the base have lifts with the same endpoint whenever their lifts begin at the same point. (The endpoint of a lifted path depends only on its endpoint-fixed homotopy class).

A topological space $X$ is simply connected when it is nonempty and path-connected (def-path-connected) and, for every $x_0\in X$, the group ${\pi }_1(X,x_0)$ has exactly one element. (Simply connected topological spaces).

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).