8.1.5 The homotopy-theoretic proof
In \autorefsec:pi1s1-universal-cover, we defined the putative universal cover in type theory, and in \autorefsubsec:pi1s1-homotopy-theory we defined a map from the path fibration 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 is contractible. For the other, we have:
The type is contractible.
We apply the flattening lemma (\autorefthm:flattening) with the following values:
is constant at .
is constant at .
Then the type family defined in the flattening lemma is equivalent to . Thus, the flattening lemma tells us that is equivalent to a higher inductive type with the following generators, which we denote :
A function .
For each , a path .
We might call this type the homotopical reals; it plays the same role as the topological space in the classical proof.
Thus, it remains to show that is contractible. As center of contraction we choose ; we must now show that for all . We do this by induction on . Firstly, when is , we must give a path , which we can do by induction on :
Secondly, we must show that for any , the path is transported along to . By transport of paths, this means we want . This is easy by induction on , using the definition of . This completes the proof that is contractible, and thus so is . ∎
The map induced by :
is an equivalence.
Both types are contractible. ∎
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 “reduction” 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|