8.1.4 The encode-decode proof

We begin with the function (LABEL:eq:pi1s1-encode) that maps paths to codes:

Definition 8.1.1.

Define $\mathsf{encode}:\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{base}=x)\rightarrow\mathsf{code}(x)$ by

\mathsf{encode}\>p:\!\!\equiv\mathsf{transport}^{\mathsf{code}}(p,0)

(we leave the argument $x$ implicit).

Encode is defined by lifting a path into the universal cover, which determines an equivalence, and then applying the resulting equivalence to $0$ . The interesting thing about this function is that it computes a concrete number from a loop on the circle, when this loop is represented using the abstract groupoidal framework of homotopy type theory. To gain an intuition for how it does this, observe that by the above lemmas, $\mathsf{transport}^{\mathsf{code}}(\mathsf{loop},x)$ is the successor map and $\mathsf{transport}^{\mathsf{code}}(\mathord{{\mathsf{loop}}^{-1}},x)$ is the predecessor map. Further, $\mathsf{transport}$ is functorial (\autorefcha:basics), so $\mathsf{transport}^{\mathsf{code}}(\mathsf{loop}\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{loop},\mathord{% \hskip 1.0pt\text{--}\hskip 1.0pt})$ is

(\mathsf{transport}^{\mathsf{code}}(\mathsf{loop},-))\circ(\mathsf{transport}^% {\mathsf{code}}(\mathsf{loop},-))

and so on. Thus, when $p$ is a composition like

\mathsf{loop}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}% }}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}\mathord{{\mathsf{loop}}^{-1}}\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{loop}% \mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}\cdots

$\mathsf{transport}^{\mathsf{code}}(p,\mathord{\hskip 1.0pt\text{--}\hskip 1.0% pt})$ will compute a composition of functions like

\mathsf{succ}\circ\mathsf{pred}\circ\mathsf{succ}\circ\cdots

Applying this composition of functions to 0 will compute the winding number of the path—how many times it goes around the circle, with orientation marked by whether it is positive or negative, after inverses have been canceled. Thus, the computational behavior of $\mathsf{encode}$ follows from the reduction rules for higher-inductive types and univalence, and the action of $\mathsf{transport}$ on compositions and inverses.

Note that the instance $\mathsf{encode}^{\prime}:\!\!\equiv\mathsf{encode}_{\mathsf{base}}$ has type $(\mathsf{base}=\mathsf{base})\rightarrow\mathbb{Z}$ . This will be one half of our desired equivalence; indeed, it is exactly the function $g$ defined in \autorefsec:pi1s1-initial-thoughts.

Similarly, the function (LABEL:eq:pi1s1-decode) is a generalization of the function $\mathsf{loop}^{\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}}$ from \autorefsec:pi1s1-initial-thoughts.

Definition 8.1.2.

Define $\mathsf{decode}:\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)\rightarrow(\mathsf{base}=x)$ by circle induction on $x$ . It suffices to give a function ${\mathsf{code}(\mathsf{base})\rightarrow(\mathsf{base}=\mathsf{base})}$ , for which we use $\mathsf{loop}^{\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}}$ , and to show that $\mathsf{loop}^{\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}}$ respects the loop.

Proof.

To show that $\mathsf{loop}^{\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}}$ respects the loop, it suffices to give a path from $\mathsf{loop}^{\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}}$ to itself that lies over $\mathsf{loop}$ . By the definition of dependent paths, this means a path from

\mathsf{transport}^{(x^{\prime}\mapsto\mathsf{code}(x^{\prime})\rightarrow(% \mathsf{base}=x^{\prime}))}(\mathsf{loop},\mathsf{loop}^{\mathord{\hskip 1.0pt% \text{--}\hskip 1.0pt}})

to $\mathsf{loop}^{\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}}$ . We define such a path as follows:

	$\displaystyle\MoveEqLeft\mathsf{transport}^{(x^{\prime}\mapsto\mathsf{code}(x^% {\prime})\rightarrow(\mathsf{base}=x^{\prime}))}(\mathsf{loop},\mathsf{loop}^{% \mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}})$
		$\displaystyle=\mathsf{transport}^{x^{\prime}\mapsto(\mathsf{base}=x^{\prime})}% (\mathsf{loop})\circ{\mathsf{loop}^{\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt% }}}\circ\mathsf{transport}^{\mathsf{code}}({\mathord{{\mathsf{loop}}^{-1}}})$
		$\displaystyle=(-\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{loop})\circ(\mathsf{loop}^{% \mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}})\circ\mathsf{transport}^{\mathsf{% code}}({\mathord{{\mathsf{loop}}^{-1}}})$
		$\displaystyle=(-\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{loop})\circ(\mathsf{loop}^{% \mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}})\circ\mathsf{pred}$
		$\displaystyle=(n\mapsto\mathsf{loop}^{n-1}\mathchoice{\mathbin{\raisebox{2.15% pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{loop}).$

On the first line, we apply the characterization of $\mathsf{transport}$ when the outer connective of the fibration is $\rightarrow$ , which reduces the $\mathsf{transport}$ to pre- and post-composition with $\mathsf{transport}$ at the domain and codomain types. On the second line, we apply the characterization of $\mathsf{transport}$ when the type family is $x\mapsto\mathsf{base}=x$ , which is post-composition of paths. On the third line, we use the action of $\mathsf{code}$ on $\mathord{{\mathsf{loop}}^{-1}}$ from \autoreflem:transport-s1-code. And on the fourth line, we simply reduce the function composition. Thus, it suffices to show that for all $n$ , $\mathsf{loop}^{n-1}\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{loop}=\mathsf{loop}^{n}$ , which is an easy induction, using the groupoid laws. ∎

We can now show that $\mathsf{encode}$ and $\mathsf{decode}$ are quasi-inverses. What used to be the difficult direction is now easy!

Lemma 8.1.3.

For all for all $x:\mathbb{S}^{1}$ and $p:\mathsf{base}=x$ , $\mathsf{decode}_{x}({{\mathsf{encode}_{x}(p)}})=p$ .

Proof.

By path induction, it suffices to show that $\mathsf{decode}_{\mathsf{base}}({{\mathsf{encode}_{\mathsf{base}}(\mathsf{refl% }_{\mathsf{base}})}})=\mathsf{refl}_{\mathsf{base}}.$ But $\mathsf{encode}_{\mathsf{base}}(\mathsf{refl}_{\mathsf{base}})\equiv\mathsf{% transport}^{\mathsf{code}}(\mathsf{refl}_{\mathsf{base}},0)\equiv 0,$ and $\mathsf{decode}_{\mathsf{base}}(0)\equiv\mathsf{loop}^{0}\equiv\mathsf{refl}_{% \mathsf{base}}$ . ∎

The other direction is not much harder.

Lemma 8.1.4.

For all $x:\mathbb{S}^{1}$ and $c:\mathsf{code}(x)$ , we have $\mathsf{encode}_{x}({{\mathsf{decode}_{x}(c)}})=c$ .

Proof.

The proof is by circle induction. It suffices to show the case for $\mathsf{base}$ , because the case for $\mathsf{loop}$ is a path between paths in $\mathbb{Z}$ , which is immediate because $\mathbb{Z}$ is a set.

Thus, it suffices to show, for all $n:\mathbb{Z}$ , that

\mathsf{encode}^{\prime}(\mathsf{loop}^{n})=n

The proof is by induction, using \crefthm:looptothe.

•

In the case for $0$ , the result is true by definition.

•

In the case for $n+1$ ,

$\displaystyle{\mathsf{encode}^{\prime}(\mathsf{loop}^{n+1})}$	$\displaystyle={\mathsf{encode}^{\prime}(\mathsf{loop}^{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{loop})% }{}$	(by definition of $\mathsf{loop}^{\mathord{\hskip1.0pt\text{--}\hskip1.0pt}}$)
	$\displaystyle=\mathsf{transport}^{\mathsf{code}}((\mathsf{loop}^{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{% loop}),0){}$	(by definition of $\mathsf{encode}$)
	$\displaystyle=\mathsf{transport}^{\mathsf{code}}(\mathsf{loop},(\mathsf{% transport}^{\mathsf{code}}(\mathsf{loop}^{n},0))){}$	(by functoriality)
	$\displaystyle={(\mathsf{transport}^{\mathsf{code}}(\mathsf{loop}^{n},0))}+1{}$	(by \autoreflem:transport-s1-code)
	$\displaystyle=n+1.{}$	(by the inductive hypothesis)

•

The case for negatives is analogous. ∎

Finally, we conclude the theorem.

Theorem 8.1.5.

There is a family of equivalences $\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{base}=x)\simeq\mathsf{code}(x))$ .

Proof.

The maps $\mathsf{encode}$ and $\mathsf{decode}$ are quasi-inverses by \autoreflem:s1-decode-encode,\autoreflem:s1-decode-encode. ∎

Instantiating at $\mathsf{base}$ gives

Corollary 8.1.6.

$\Omega(\mathbb{S}^{1},\mathsf{base})\simeq\mathbb{Z}$ .

A simple induction shows that this equivalence takes addition to composition, so that $\Omega(\mathbb{S}^{1})=\mathbb{Z}$ as groups.

Corollary 8.1.7.

$\pi_{1}(\mathbb{S}^{1})=\mathbb{Z}$ , while $\pi_{n}(\mathbb{S}^{1})=0$ for $n>1$ .

Proof.

For $n=1$ , we sketched the proof from \autorefcor:omega-s1 above. For $n>1$ , we have $\mathopen{}\left\|\Omega^{n}(\mathbb{S}^{1})\right\|_{0}\mathclose{}=\mathopen% {}\left\|\Omega^{n-1}(\Omega{\mathbb{S}^{1}})\right\|_{0}\mathclose{}=% \mathopen{}\left\|\Omega^{n-1}(\mathbb{Z})\right\|_{0}\mathclose{}$ . And since $\mathbb{Z}$ is a set, $\Omega^{n-1}(\mathbb{Z})$ is contractible, so this is trivial. ∎

Title	8.1.4 The encode-decode proof
\metatable