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 $\mathrm{encode}\mathrm{:}{\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}{\mathrm{S}}^{\mathrm{1}}\mathrm{)}}\mathrm{(}\mathrm{base}\mathrm{=}x\mathrm{)}\mathrm{\to }\mathrm{code}\mathrm{(}x\mathrm{)}$ by

$$\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}p:\equiv {\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖼𝗈𝖽𝖾}}(p,0)$$

(we leave the argument $x$ implicit).

Encode is defined by lifting a path into the universal cover, whichdetermines an equivalence, and then applying the resulting equivalenceto $0$.The interesting thing about this function is that it computes a concretenumber from a loop on the circle, when this loop is represented usingthe abstract groupoidal framework of homotopy type theory. To gain anintuition for how it does this, observe that by the above lemmas,${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖼𝗈𝖽𝖾}}(\mathrm{𝗅𝗈𝗈𝗉},x)$ is the successor map and ${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖼𝗈𝖽𝖾}}({\mathrm{𝗅𝗈𝗈𝗉}}^{-1},x)$ is the predecessor map.Further, $\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}$ is functorial (cha:basics), so${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖼𝗈𝖽𝖾}}(\mathrm{𝗅𝗈𝗈𝗉}\mathrm{𝗅𝗈𝗈𝗉},\text{–})$ is

$$({\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖼𝗈𝖽𝖾}}(\mathrm{𝗅𝗈𝗈𝗉},-))\circ ({\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖼𝗈𝖽𝖾}}(\mathrm{𝗅𝗈𝗈𝗉},-))$$

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

$$\mathrm{𝗅𝗈𝗈𝗉}{\mathrm{𝗅𝗈𝗈𝗉}}^{-1}\mathrm{𝗅𝗈𝗈𝗉}\mathrm{\cdots }$$

${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖼𝗈𝖽𝖾}}(p,\text{–})$ will compute a composition of functions like

$$\mathrm{𝗌𝗎𝖼𝖼}\circ \mathrm{𝗉𝗋𝖾𝖽}\circ \mathrm{𝗌𝗎𝖼𝖼}\circ \mathrm{\cdots }$$

Applying this composition of functions to 0 will compute thewinding number of the path—how many times it goes around thecircle, with orientation marked by whether it is positive or negative,after inverses have been canceled. Thus, the computational behavior of$\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}$ follows from the reduction rules for higher-inductive types andunivalence, and the action of $\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}$ on compositions and inverses.

Note that the instance ${\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}}^{\prime }:\equiv {\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}}_{\mathrm{𝖻𝖺𝗌𝖾}}$ has type$(\mathrm{𝖻𝖺𝗌𝖾}=\mathrm{𝖻𝖺𝗌𝖾})\to \mathbb{Z}$.This will be one half of our desired equivalence; indeed, it is exactly the function $g$ defined in sec:pi1s1-initial-thoughts.

Similarly, the function (LABEL:eq:pi1s1-decode) is a generalization of the function ${\mathrm{𝗅𝗈𝗈𝗉}}^{\text{–}}$ from sec:pi1s1-initial-thoughts.

Definition 8.1.2.

Define $\mathrm{decode}\mathrm{:}{\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}{\mathrm{S}}^{\mathrm{1}}\mathrm{)}}\mathrm{code}\mathrm{(}x\mathrm{)}\mathrm{\to }\mathrm{(}\mathrm{base}\mathrm{=}x\mathrm{)}$ bycircle induction on $x$. It suffices to give a function$\mathrm{code}\mathrm{(}\mathrm{base}\mathrm{)}\mathrm{\to }\mathrm{(}\mathrm{base}\mathrm{=}\mathrm{base}\mathrm{)}$, for which we use ${\mathrm{loop}}^{\mathit{\text{–}}}$, andto show that ${\mathrm{loop}}^{\mathit{\text{–}}}$ respects the loop.

Proof.

To show that ${\mathrm{𝗅𝗈𝗈𝗉}}^{\text{–}}$ respects the loop, it suffices to give a pathfrom ${\mathrm{𝗅𝗈𝗈𝗉}}^{\text{–}}$ to itself that lies over $\mathrm{𝗅𝗈𝗈𝗉}$.By the definition of dependent paths, this means a path from

$${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{(x^{\prime }\mapsto \mathrm{𝖼𝗈𝖽𝖾}(x^{\prime })\to (\mathrm{𝖻𝖺𝗌𝖾}=x^{\prime }))}(\mathrm{𝗅𝗈𝗈𝗉},{\mathrm{𝗅𝗈𝗈𝗉}}^{\text{–}})$$

to ${\mathrm{𝗅𝗈𝗈𝗉}}^{\text{–}}$. We define such apath as follows:

${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{(x^{\prime }\mapsto \mathrm{𝖼𝗈𝖽𝖾}(x^{\prime })\to (\mathrm{𝖻𝖺𝗌𝖾}=x^{\prime }))}(\mathrm{𝗅𝗈𝗈𝗉},{\mathrm{𝗅𝗈𝗈𝗉}}^{\text{–}})$

$={\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{x^{\prime }\mapsto (\mathrm{𝖻𝖺𝗌𝖾}=x^{\prime })}(\mathrm{𝗅𝗈𝗈𝗉})\circ {\mathrm{𝗅𝗈𝗈𝗉}}^{\text{–}}\circ {\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖼𝗈𝖽𝖾}}({\mathrm{𝗅𝗈𝗈𝗉}}^{-1})$

$=(-\mathrm{𝗅𝗈𝗈𝗉})\circ ({\mathrm{𝗅𝗈𝗈𝗉}}^{\text{–}})\circ {\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖼𝗈𝖽𝖾}}({\mathrm{𝗅𝗈𝗈𝗉}}^{-1})$

$=(-\mathrm{𝗅𝗈𝗈𝗉})\circ ({\mathrm{𝗅𝗈𝗈𝗉}}^{\text{–}})\circ \mathrm{𝗉𝗋𝖾𝖽}$

$=(n\mapsto {\mathrm{𝗅𝗈𝗈𝗉}}^{n-1}\mathrm{𝗅𝗈𝗈𝗉}).$

On the first line, we apply the characterization of $\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}$when the outer connective of the fibration is $\to$, whichreduces the $\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}$ to pre- and post-composition with$\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}$ at the domain and codomain types. On the second line,we apply the characterization of $\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}$ when the type familyis $x\mapsto \mathrm{𝖻𝖺𝗌𝖾}=x$, which is post-composition of paths. On the third line,we use the action of $\mathrm{𝖼𝗈𝖽𝖾}$ on ${\mathrm{𝗅𝗈𝗈𝗉}}^{-1}$ fromlem:transport-s1-code. And on the fourth line, we simplyreduce the function composition. Thus, it suffices to show that for all$n$, ${\mathrm{𝗅𝗈𝗈𝗉}}^{n-1}\mathrm{𝗅𝗈𝗈𝗉}={\mathrm{𝗅𝗈𝗈𝗉}}^n$, which is an easyinduction, using the groupoid laws.∎

We can now show that $\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}$ and $\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}$ are quasi-inverses.What used to be the difficult direction is now easy!

Lemma 8.1.3.

For allfor all $x\mathrm{:}{\mathrm{S}}^{\mathrm{1}}$ and $p\mathrm{:}\mathrm{base}\mathrm{=}x$, ${\mathrm{decode}}_x\mathit{}\mathrm{(}{\mathrm{encode}}_x\mathit{}\mathrm{(}p\mathrm{)}\mathrm{)}\mathrm{=}p$.

Proof.

By path induction, it suffices to show that${\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}}_{\mathrm{𝖻𝖺𝗌𝖾}}({\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}}_{\mathrm{𝖻𝖺𝗌𝖾}}({\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝖻𝖺𝗌𝖾}}))={\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝖻𝖺𝗌𝖾}}.$But${\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}}_{\mathrm{𝖻𝖺𝗌𝖾}}({\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝖻𝖺𝗌𝖾}})\equiv {\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖼𝗈𝖽𝖾}}({\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝖻𝖺𝗌𝖾}},0)\equiv 0,$and ${\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}}_{\mathrm{𝖻𝖺𝗌𝖾}}(0)\equiv {\mathrm{𝗅𝗈𝗈𝗉}}^0\equiv {\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝖻𝖺𝗌𝖾}}$.∎

The other direction is not much harder.

Lemma 8.1.4.

For all$x\mathrm{:}{\mathrm{S}}^{\mathrm{1}}$ and $c\mathrm{:}\mathrm{code}\mathit{}\mathrm{(}x\mathrm{)}$, we have ${\mathrm{encode}}_x\mathit{}\mathrm{(}{\mathrm{decode}}_x\mathit{}\mathrm{(}c\mathrm{)}\mathrm{)}\mathrm{=}c$.

Proof.

The proof is by circle induction. It suffices to show the case for$\mathrm{𝖻𝖺𝗌𝖾}$, because the case for $\mathrm{𝗅𝗈𝗈𝗉}$ 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

$${\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}}^{\prime }({\mathrm{𝗅𝗈𝗈𝗉}}^n)=n$$

The proof is by induction, using thm:looptothe.

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

• In the case for $n+1$,

  ${\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}}^{\prime }({\mathrm{𝗅𝗈𝗈𝗉}}^{n+1})$$={\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}}^{\prime }({\mathrm{𝗅𝗈𝗈𝗉}}^n\mathrm{𝗅𝗈𝗈𝗉})$(by definition of $\\mathsf{loop}^{\\mathord{\\hskip1.0pt\\text{--}\\hskip1.0pt}}$)

  $={\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖼𝗈𝖽𝖾}}(({\mathrm{𝗅𝗈𝗈𝗉}}^n\mathrm{𝗅𝗈𝗈𝗉}),0)$(by definition of $\\mathsf{encode}$)

  $={\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖼𝗈𝖽𝖾}}(\mathrm{𝗅𝗈𝗈𝗉},({\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖼𝗈𝖽𝖾}}({\mathrm{𝗅𝗈𝗈𝗉}}^n,0)))$(by functoriality)

  $=({\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖼𝗈𝖽𝖾}}({\mathrm{𝗅𝗈𝗈𝗉}}^n,0))+1$(by \\autoreflem:transport-s1-code)

  $=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 ${\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}{\mathrm{S}}^{\mathrm{1}}\mathrm{)}}\mathrm{(}\mathrm{(}\mathrm{base}\mathrm{=}x\mathrm{)}\mathrm{\simeq }\mathrm{code}\mathrm{(}x\mathrm{)}\mathrm{)}$.

Proof.

The maps $\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}$ and $\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}$ are quasi-inverses bylem:s1-decode-encode,lem:s1-decode-encode.∎

Instantiating at $\mathrm{𝖻𝖺𝗌𝖾}$ gives

Corollary 8.1.6.

$\mathrm{\Omega }({𝕊}^1,\mathrm{𝖻𝖺𝗌𝖾})\simeq \mathbb{Z}$.

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

Corollary 8.1.7.

${\pi }_1({𝕊}^1)=\mathbb{Z}$, while ${\pi }_n\mathit{}\mathrm{(}{\mathrm{S}}^{\mathrm{1}}\mathrm{)}\mathrm{=}\mathrm{0}$ for $n\mathrm{>}\mathrm{1}$.

Proof.

For $n=1$, we sketched the proof from cor:omega-s1 above.For $n>1$, we have $\parallel {\mathrm{\Omega }}^n({𝕊}^1){\parallel }_0=\parallel {\mathrm{\Omega }}^{n-1}(\mathrm{\Omega }{𝕊}^1){\parallel }_0=\parallel {\mathrm{\Omega }}^{n-1}(\mathbb{Z}){\parallel }_0$.And since $\mathbb{Z}$ is a set, ${\mathrm{\Omega }}^{n-1}(\mathbb{Z})$ is contractible, so this is trivial.∎