8.1.2 The classical proof
In classical homotopy theory, there is a standard proof of using universal covering spaces. Our proof can be regarded as a type-theoretic version of this proof, with covering spaces appearing here as fibrations whose fibers are sets. Recall that fibrations over a space in homotopy theory correspond to type families in type theory. In particular, for a point , the type family corresponds to the path fibration , in which the points of are paths in starting at , and the map to selects the other endpoint of such a path. This total space is contractible, since we can “retract” any path to its initial endpoint — we have seen the type-theoretic version of this as \autorefthm:contr-paths. Moreover, the fiber over is the loop space — in type theory this is obvious by definition of the loop space.
Now in classical homotopy theory, where is regarded as a topological space, we may proceed as follows. Consider the “winding” map , which looks like a helix projecting down onto the circle (see \autoreffig:winding). This map sends each point on the helix to the point on the circle that it is “sitting above”. It is a fibration, and the fiber over each point is isomorphic to the integers. If we lift the path that goes counterclockwise around the loop on the bottom, we go up one level in the helix, incrementing the integer in the fiber. Similarly, going clockwise around the loop on the bottom corresponds to going down one level in the helix, decrementing this count. This fibration is called the universal cover of the circle.
Now a basic fact in classical homotopy theory is that a map of fibrations over which is a homotopy equivalence between and induces a homotopy equivalence on all fibers. (We have already seen the type-theoretic version of this as well in \autorefthm:total-fiber-equiv.) Since and are both contractible topological spaces, they are homotopy equivalent, and thus their fibers and over the basepoint are also homotopy equivalent.
|Title||8.1.2 The classical proof|