8.1.5 The homotopy-theoretic proof

In \autorefsec:pi1s1-universal-cover, we defined the putative universal coverMathworldPlanetmath π–Όπ—ˆπ–½π–Ύ:π•Š1→𝒰 in type theoryPlanetmathPlanetmath, and in \autorefsubsec:pi1s1-homotopy-theory we defined a map π–Ύπ—‡π–Όπ—ˆπ–½π–Ύ:∏(x:π•Š1)(π–»π–Ίπ—Œπ–Ύ=x)β†’π–Όπ—ˆπ–½π–Ύ(x) from the path fibrationMathworldPlanetmath to the universal cover. What remains for the classical proof is to show that this map induces an equivalence on total spaces because both are contractible, and to deduce from this that it must be an equivalence on each fiber.

In \autorefthm:contr-paths we saw that the total space βˆ‘(x:π•Š1)(π–»π–Ίπ—Œπ–Ύ=x) is contractible. For the other, we have:

Lemma 8.1.1.

The type βˆ‘(x:S1)code⁒(x) is contractible.


We apply the flattening lemma (\autorefthm:flattening) with the following values:

  • β€’

    A:β‰‘πŸ and B:β‰‘πŸ, with f and g the obvious functions. Thus, the base higher inductive type W in the flattening lemma is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to π•Š1.

  • β€’

    C:A→𝒰 is constant at β„€.

  • β€’

    D:∏(b:B)(℀≃℀) is constant at π—Œπ—Žπ–Όπ–Ό.

Then the type family P:π•Š1→𝒰 defined in the flattening lemma is equivalent to π–Όπ—ˆπ–½π–Ύ:π•Š1→𝒰. Thus, the flattening lemma tells us that βˆ‘(x:π•Š1)π–Όπ—ˆπ–½π–Ύβ’(x) is equivalent to a higher inductive type with the following generatorsPlanetmathPlanetmathPlanetmath, which we denote R:

  • β€’

    A function 𝖼:β„€β†’R.

  • β€’

    For each z:β„€, a path 𝗉z:𝖼⁒(z)=𝖼⁒(π—Œπ—Žπ–Όπ–Όβ’(z)).

We might call this type the homotopical reals; it plays the same role as the topological spaceMathworldPlanetmath ℝ in the classical proof.

Thus, it remains to show that R is contractible. As center of contraction we choose 𝖼⁒(0); we must now show that x=𝖼⁒(0) for all x:R. We do this by inductionMathworldPlanetmath on R. Firstly, when x is 𝖼⁒(z), we must give a path qz:𝖼⁒(0)=𝖼⁒(z), which we can do by induction on z:β„€:

q0 :≑𝗋𝖾𝖿𝗅𝖼⁒(0)
qn+1 :≑qn\centerdot𝗉n for nβ‰₯0
qn-1 :≑qn\centerdot𝗉n-1-1 for n≀0.

Secondly, we must show that for any z:β„€, the path qz is transported along 𝗉z to qz+1. By transport of paths, this means we want qz⁒\centerdot⁒𝗉z=qz+1. This is easy by induction on z, using the definition of qz. This completesPlanetmathPlanetmathPlanetmathPlanetmath the proof that R is contractible, and thus so is βˆ‘(x:π•Š1)π–Όπ—ˆπ–½π–Ύβ’(x). ∎

Corollary 8.1.2.

The map induced by encode:


is an equivalence.


Both types are contractible. ∎

Theorem 8.1.3.



Apply \autorefthm:total-fiber-equiv to π–Ύπ—‡π–Όπ—ˆπ–½π–Ύ, using \autorefthm:encode-total-equiv. ∎

In essence, the two proofs are not very different: the encode-decode one may be seen as a β€œreductionPlanetmathPlanetmathPlanetmath” or β€œunpackaging” of the homotopy-theoretic one. Each has its advantages; the interplay between the two points of view is part of the interest of the subject.

Title 8.1.5 The homotopy-theoretic proof