8.1.2 The classical proof

In classical homotopy theory, there is a standard proof of Ο€1⁒(π•Š1)=β„€ using universal covering spaces. Our proof can be regarded as a type-theoretic version of this proof, with covering spaces appearing here as fibrationsMathworldPlanetmath whose fibers are sets. Recall that fibrations over a space B in homotopy theory correspond to type families B→𝒰 in type theory. In particular, for a point x0:B, the type family (x↦(x0=x)) corresponds to the path fibration Px0⁒Bβ†’B, in which the points of Px0⁒B are paths in B starting at x0, and the map to B selects the other endpoint of such a path. This total space Px0⁒B is contractibleMathworldPlanetmath, since we can β€œretractMathworldPlanetmath” any path to its initial endpoint x0 β€” we have seen the type-theoretic version of this as \autorefthm:contr-paths. Moreover, the fiber over x0 is the loop spaceMathworldPlanetmath Ω⁒(B,x0) β€” in type theory this is obvious by definition of the loop space.


[xscale=1.4,yscale=.6] \node(R) at (2,1) ℝ; \node(S1) at (2,-2) S1; \draw[-ΒΏ] (R) – node[auto] w (S1); \draw(0,-2) ellipse (1 and .4); \draw[dotted] (1,0) arc (0:-30:1 and .8); \draw(1,0) arc (0:90:1 and .8) arc (90:270:1 and .3) coordinate (t1); \draw[white,line width=4pt] (t1) arc (-90:90:1 and .8); \draw(t1) arc (-90:90:1 and .8) arc (90:270:1 and .3) coordinate (t2); \draw[white,line width=4pt] (t2) arc (-90:90:1 and .8); \draw(t2) arc (-90:90:1 and .8) arc (90:270:1 and .3) coordinate (t3); \draw[white,line width=4pt] (t3) arc (-90:90:1 and .8); \draw(t3) arc (-90:-30:1 and .8) coordinate (t4); \draw[dotted] (t4) arc (-30:0:1 and .8); \node[fill,circle,inner sep=1pt,label=below:π–»π–Ίπ—Œπ–Ύ] at (0,-2.4) ; \node[fill,circle,inner sep=1pt,label=above left:0] at (0,.2) ; \node[fill,circle,inner sep=1pt,label=above left:1] at (0,1.2) ; \node[fill,circle,inner sep=1pt,label=above left:2] at (0,2.2) ;

FigureΒ 1: The winding map in classical topologyMathworldPlanetmath

Now in classical homotopy theory, where π•Š1 is regarded as a topological space, we may proceed as follows. Consider the β€œwinding” map w:β„β†’π•Š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 E1β†’E2 of fibrations over B which is a homotopy equivalenceMathworldPlanetmathPlanetmath between E1 and E2 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 Pπ–»π–Ίπ—Œπ–Ύβ’S1 are both contractible topological spaces, they are homotopy equivalent, and thus their fibers β„€ and Ω⁒(π•Š1) over the basepoint are also homotopy equivalent.

Title 8.1.2 The classical proof