8.1.2 The classical proof

In classical homotopy theory, there is a standard proof of $\pi_{1}(\mathbb{S}^{1})=\mathbb{Z}$ 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 $B$ in homotopy theory correspond to type families $B\to\mathcal{U}$ in type theory. In particular, for a point $x_{0}:B$ , the type family $(x\mapsto(x_{0}=x))$ corresponds to the path fibration $P_{x_{0}}B\to B$ , in which the points of $P_{x_{0}}B$ are paths in $B$ starting at $x_{0}$ , and the map to $B$ selects the other endpoint of such a path. This total space $P_{x_{0}}B$ is contractible, since we can “retract” any path to its initial endpoint $x_{0}$ — we have seen the type-theoretic version of this as \autorefthm:contr-paths. Moreover, the fiber over $x_{0}$ is the loop space $\Omega(B,x_{0})$ — in type theory this is obvious by definition of the loop space.

Mathworld — Figure 1: The winding map in classical topology

Now in classical homotopy theory, where $\mathbb{S}^{1}$ is regarded as a topological space, we may proceed as follows. Consider the “winding” map $w:\mathbb{R}\to\mathbb{S}^{1}$ , which looks like a helix projecting down onto the circle (see \autoreffig:winding). This map $w$ 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 $E_{1}\to E_{2}$ of fibrations over $B$ which is a homotopy equivalence between $E_{1}$ and $E_{2}$ 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 $\mathbb{R}$ and $P_{\mathsf{base}}S^{1}$ are both contractible topological spaces, they are homotopy equivalent, and thus their fibers $\mathbb{Z}$ and $\Omega(\mathbb{S}^{1})$ over the basepoint are also homotopy equivalent.

Title	8.1.2 The classical proof
\metatable