§ Definition of covering space

It's important that when we say that $p^{-1}(U) = U \times F$, that the local homeomorphisms of $U \times {i} \rightarrow U$ is given by $p|_{U \times \{ i \}}$: it is not some other map that gives us the homeomorphism, but $p$ itself. This makes $p$ locally bijective on a nbhd.

§ Path lifting

A time varying embedding can be lifted for all time given a lift of initial conditions. A smoothly varying family of embeddings can be filted given an initial lift.

The fact that we work with intervals are of paramount importance. They are compact, and we can thus use induction to path lift.

• Kan extension condition