8.1.6 The universal cover as an identity system

Note that the fibration $\mathsf{code}:\mathbb{S}^{1}\to\mathcal{U}$ together with $0:\mathsf{code}(\mathsf{base})$ 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 $\mathsf{code}$ 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.

Theorem 8.1.1.

The pair $(\mathsf{code},0)$ is an identity system at $\mathsf{base}:\mathbb{S}^{1}$ in the sense of \autorefdefn:identity-systems.

Proof.

Let $D:\mathchoice{\prod_{x:\mathbb{S}^{1}}\,}{\mathchoice{{\textstyle\prod_{(x:% \mathbb{S}^{1})}}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{% \prod_{(x:\mathbb{S}^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}% }}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S% }^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}}}{\prod_{(x:% \mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}}% \mathsf{code}(x)\to\mathcal{U}$ and $d:D(\mathsf{base},0)$ be given; we want to define a function $f:\mathchoice{\prod_{(x:\mathbb{S}^{1})}\,}{\mathchoice{{\textstyle\prod_{(x:% \mathbb{S}^{1})}}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{% \prod_{(x:\mathbb{S}^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}% }}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S% }^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}}}{\prod_{(x:% \mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}}% \mathchoice{\prod_{(c:\mathsf{code}(x))}\,}{\mathchoice{{\textstyle\prod_{(c:% \mathsf{code}(x))}}}{\prod_{(c:\mathsf{code}(x))}}{\prod_{(c:\mathsf{code}(x))% }}{\prod_{(c:\mathsf{code}(x))}}}{\mathchoice{{\textstyle\prod_{(c:\mathsf{% code}(x))}}}{\prod_{(c:\mathsf{code}(x))}}{\prod_{(c:\mathsf{code}(x))}}{\prod% _{(c:\mathsf{code}(x))}}}{\mathchoice{{\textstyle\prod_{(c:\mathsf{code}(x))}}% }{\prod_{(c:\mathsf{code}(x))}}{\prod_{(c:\mathsf{code}(x))}}{\prod_{(c:% \mathsf{code}(x))}}}D(x,c)$ . By circle induction, it suffices to specify $f(\mathsf{base}):\mathchoice{\prod_{c:\mathsf{code}(\mathsf{base})}\,}{% \mathchoice{{\textstyle\prod_{(c:\mathsf{code}(\mathsf{base}))}}}{\prod_{(c:% \mathsf{code}(\mathsf{base}))}}{\prod_{(c:\mathsf{code}(\mathsf{base}))}}{% \prod_{(c:\mathsf{code}(\mathsf{base}))}}}{\mathchoice{{\textstyle\prod_{(c:% \mathsf{code}(\mathsf{base}))}}}{\prod_{(c:\mathsf{code}(\mathsf{base}))}}{% \prod_{(c:\mathsf{code}(\mathsf{base}))}}{\prod_{(c:\mathsf{code}(\mathsf{base% }))}}}{\mathchoice{{\textstyle\prod_{(c:\mathsf{code}(\mathsf{base}))}}}{\prod% _{(c:\mathsf{code}(\mathsf{base}))}}{\prod_{(c:\mathsf{code}(\mathsf{base}))}}% {\prod_{(c:\mathsf{code}(\mathsf{base}))}}}D(\mathsf{base},c)$ and verify that ${\mathsf{loop}}_{*}\mathopen{}\left({f(\mathsf{base})}\right)\mathclose{}=f(% \mathsf{base})$ .

Of course, $\mathsf{code}(\mathsf{base})\equiv\mathbb{Z}$ . By \autoreflem:transport-s1-code and induction on $n$ , we may obtain a path $p_{n}:\mathsf{transport}^{\mathsf{code}}(\mathsf{loop}^{n},0)=n$ for any integer $n$ . Therefore, by paths in $\Sigma$ -types, we have a path $\mathsf{pair}^{\mathord{=}}(\mathsf{loop}^{n},p_{n}):(\mathsf{base},0)=(% \mathsf{base},n)$ in $\mathchoice{\sum_{x:\mathbb{S}^{1}}\,}{\mathchoice{{\textstyle\sum_{(x:\mathbb% {S}^{1})}}}{\sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:% \mathbb{S}^{1})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbb{S}^{1})}}}{\sum_{(x% :\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}}{% \mathchoice{{\textstyle\sum_{(x:\mathbb{S}^{1})}}}{\sum_{(x:\mathbb{S}^{1})}}{% \sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}}\mathsf{code}(x)$ . Transporting $d$ along this path in the fibration $\widehat{D}:(\mathchoice{\sum_{x:\mathbb{S}^{1}}\,}{\mathchoice{{\textstyle% \sum_{(x:\mathbb{S}^{1})}}}{\sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1}% )}}{\sum_{(x:\mathbb{S}^{1})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbb{S}^{1}% )}}}{\sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}% ^{1})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbb{S}^{1})}}}{\sum_{(x:\mathbb{S% }^{1})}}{\sum_{(x:\mathbb{S}^{1})}}{\sum_{(x:\mathbb{S}^{1})}}}\mathsf{code}(x% ))\to\mathcal{U}$ associated to $D$ , we obtain an element of $D(\mathsf{base},n)$ for any $n:\mathbb{Z}$ . We define this element to be $f(\mathsf{base})(n)$ :

$f(\mathsf{base})(n):\!\!\equiv\mathsf{transport}^{\widehat{D}}(\mathsf{pair}^{% \mathord{=}}(\mathsf{loop}^{n},p_{n}),d).$

Now we need $\mathsf{transport}^{{\lambda}x.\,\mathchoice{\prod_{c:\mathsf{code}(x)}\,}{% \mathchoice{{\textstyle\prod_{(c:\mathsf{code}(x))}}}{\prod_{(c:\mathsf{code}(% x))}}{\prod_{(c:\mathsf{code}(x))}}{\prod_{(c:\mathsf{code}(x))}}}{\mathchoice% {{\textstyle\prod_{(c:\mathsf{code}(x))}}}{\prod_{(c:\mathsf{code}(x))}}{\prod% _{(c:\mathsf{code}(x))}}{\prod_{(c:\mathsf{code}(x))}}}{\mathchoice{{% \textstyle\prod_{(c:\mathsf{code}(x))}}}{\prod_{(c:\mathsf{code}(x))}}{\prod_{% (c:\mathsf{code}(x))}}{\prod_{(c:\mathsf{code}(x))}}}D(x,c)}(\mathsf{loop},f(% \mathsf{base}))=f(\mathsf{base})$ . By \autorefthm:dpath-forall, this means we need to show that for any $n:\mathbb{Z}$ ,

$\mathsf{transport}^{\widehat{D}}(\mathsf{pair}^{\mathord{=}}(\mathsf{loop},% \mathsf{refl}_{{\mathsf{loop}}_{*}\mathopen{}\left({n}\right)\mathclose{}}),f(% \mathsf{base})(n))=_{D(\mathsf{base},{\mathsf{loop}}_{*}\mathopen{}\left({n}% \right)\mathclose{})}f(\mathsf{base})({\mathsf{loop}}_{*}\mathopen{}\left({n}% \right)\mathclose{}).$

Now we have a path $q:{\mathsf{loop}}_{*}\mathopen{}\left({n}\right)\mathclose{}=n+1$ , so transporting along this, it suffices to show

$\displaystyle\mathsf{transport}^{D(\mathsf{base})}(q,\mathsf{transport}^{% \widehat{D}}(\mathsf{pair}^{\mathord{=}}(\mathsf{loop},\mathsf{refl}_{{\mathsf% {loop}}_{*}\mathopen{}\left({n}\right)\mathclose{}}),f(\mathsf{base})(n)))\\ \displaystyle=_{D(\mathsf{base},n+1)}\mathsf{transport}^{D(\mathsf{base})}(q,f% (\mathsf{base})({\mathsf{loop}}_{*}\mathopen{}\left({n}\right)\mathclose{})).$

By a couple of lemmas about transport and dependent application, this is equivalent to

$\mathsf{transport}^{\widehat{D}}(\mathsf{pair}^{\mathord{=}}(\mathsf{loop},q),% f(\mathsf{base})(n))=_{D(\mathsf{base},n+1)}f(\mathsf{base})(n+1).$

However, expanding out the definition of $f(\mathsf{base})$ , we have

$\mathsf{transport}^{\widehat{D}}(\mathsf{pair}^{\mathord{=}}(\mathsf{loop},q),% f(\mathsf{base})(n))\begin{aligned} &\displaystyle=\mathsf{transport}^{% \widehat{D}}(\mathsf{pair}^{\mathord{=}}(\mathsf{loop},q),\mathsf{transport}^{% \widehat{D}}(\mathsf{pair}^{\mathord{=}}(\mathsf{loop}^{n},p_{n}),d))\\ &\displaystyle=\mathsf{transport}^{\widehat{D}}(\mathsf{pair}^{\mathord{=}}(% \mathsf{loop}^{n},p_{n})\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathsf{pair}^{\mathord{=}}(\mathsf{loop},% q),d)\\ &\displaystyle=\mathsf{transport}^{\widehat{D}}(\mathsf{pair}^{\mathord{=}}(% \mathsf{loop}^{n+1},p_{n+1}),d)\\ &\displaystyle=f(\mathsf{base})(n+1).\end{aligned}$

We have used the functoriality of transport, the characterization of composition in $\Sigma$ -types (which was an exercise for the reader), and a lemma relating $p_{n}$ and $q$ to $p_{n+1}$ which we leave it to the reader to state and prove.

This completes the construction of $f:\mathchoice{\prod_{(x:\mathbb{S}^{1})}\,}{\mathchoice{{\textstyle\prod_{(x:% \mathbb{S}^{1})}}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{% \prod_{(x:\mathbb{S}^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}% }}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S% }^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}}}{\prod_{(x:% \mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}}% \mathchoice{\prod_{(c:\mathsf{code}(x))}\,}{\mathchoice{{\textstyle\prod_{(c:% \mathsf{code}(x))}}}{\prod_{(c:\mathsf{code}(x))}}{\prod_{(c:\mathsf{code}(x))% }}{\prod_{(c:\mathsf{code}(x))}}}{\mathchoice{{\textstyle\prod_{(c:\mathsf{% code}(x))}}}{\prod_{(c:\mathsf{code}(x))}}{\prod_{(c:\mathsf{code}(x))}}{\prod% _{(c:\mathsf{code}(x))}}}{\mathchoice{{\textstyle\prod_{(c:\mathsf{code}(x))}}% }{\prod_{(c:\mathsf{code}(x))}}{\prod_{(c:\mathsf{code}(x))}}{\prod_{(c:% \mathsf{code}(x))}}}D(x,c)$ . Since

$f(\mathsf{base},0)\equiv{\mathsf{pair}^{\mathord{=}}(\mathsf{loop}^{0},p_{0})}% _{*}\mathopen{}\left({d}\right)\mathclose{}={\mathsf{refl}_{\mathsf{base}}}_{*% }\mathopen{}\left({d}\right)\mathclose{}=d,$

we have shown that $(\mathsf{code},0)$ is an identity system. ∎

Corollary 8.1.2.

For any $x:\mathbb{S}^{1}$ , we have $(\mathsf{base}=x)\simeq\mathsf{code}(x)$ .

Proof.

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
\metatable