8.1.6 The universal cover as an identity system
Note that the fibration together with is a pointed predicate in the sense of \autorefdefn:identity-systems. From this point of view, we can see that the encode-decode proof in \autorefsubsec:pi1s1-encode-decode consists of proving that satisfies \autorefthm:identity-systemsLABEL:item:identity-systems3, while the homotopy-theoretic proof in \autorefsubsec:pi1s1-homotopy-theory consists of proving that it satisfies \autorefthm:identity-systemsLABEL:item:identity-systems4. This suggests a third approach.
The pair is an identity system at in the sense of \autorefdefn:identity-systems.
Of course, . By \autoreflem:transport-s1-code and induction on , we may obtain a path for any integer . Therefore, by paths in -types, we have a path in . Transporting along this path in the fibration associated to , we obtain an element of for any . We define this element to be :
Now we need . By \autorefthm:dpath-forall, this means we need to show that for any ,
Now we have a path , so transporting along this, it suffices to show
By a couple of lemmas about transport and dependent application, this is equivalent to
However, expanding out the definition of , we have
We have used the functoriality of transport, the characterization of composition in -types (which was an exercise for the reader), and a lemma relating and to which we leave it to the reader to state and prove.
This completes the construction of . Since
we have shown that is an identity system. ∎
For any , we have .
By \autorefthm:identity-systems. ∎
Of course, this proof also contains essentially the same elements as the previous two. Roughly, we can say that it unifies the proofs of \autorefthm:pi1s1-decode,\autoreflem:s1-encode-decode, performing the requisite inductive argument only once in a generic case.
|Title||8.1.6 The universal cover as an identity system|