Fibre bijection by path lifting (source code)

= Fibre bijection by path lifting

If the base of a covering is path-connected, a path from $x_0$ to $x_1$ gives a bijection
$$
p^{-1}(x_0)\longrightarrow p^{-1}(x_1)
$$
by sending each initial lift point to the endpoint of its unique lifted path. Lifting the reversed path gives the inverse bijection.