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.