8.1.1 Getting started

It is not too hard to define functions in both directions between $\mathrm{\Omega }({𝕊}^1)$ and $\mathbb{Z}$.By specializing thm:looptothe to $\mathrm{𝗅𝗈𝗈𝗉}:\mathrm{𝖻𝖺𝗌𝖾}=\mathrm{𝖻𝖺𝗌𝖾}$, we have a function ${\mathrm{𝗅𝗈𝗈𝗉}}^{\text{–}}:\mathbb{Z}\to (\mathrm{𝖻𝖺𝗌𝖾}=\mathrm{𝖻𝖺𝗌𝖾})$ defined (loosely speaking) by

Defining a function $g:\mathrm{\Omega }({𝕊}^1)\to \mathbb{Z}$ in the other direction is a bit trickier.Note that the successor function $\mathrm{𝗌𝗎𝖼𝖼}:\mathbb{Z}\to \mathbb{Z}$ is an equivalence,and hence induces a path $\mathrm{𝗎𝖺}(\mathrm{𝗌𝗎𝖼𝖼}):\mathbb{Z}=\mathbb{Z}$ in the universe $𝒰$.Thus, the recursion principle of ${𝕊}^1$ induces a map $c:{𝕊}^1\to 𝒰$ by $c(\mathrm{𝖻𝖺𝗌𝖾}):\equiv \mathbb{Z}$ and ${\mathrm{𝖺𝗉}}_c(\mathrm{𝗅𝗈𝗈𝗉}):=\mathrm{𝗎𝖺}(\mathrm{𝗌𝗎𝖼𝖼})$.Then we have ${\mathrm{𝖺𝗉}}_c:(\mathrm{𝖻𝖺𝗌𝖾}=\mathrm{𝖻𝖺𝗌𝖾})\to (\mathbb{Z}=\mathbb{Z})$, and we can define $g(p):\equiv {\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{X\mapsto X}({\mathrm{𝖺𝗉}}_c(p),0)$.

With these definitions, we can even prove that $g({\mathrm{𝗅𝗈𝗈𝗉}}^n)=n$ for any $n:\mathbb{Z}$, using the induction principle thm:sign-induction for $n$.(We will prove something more general a little later on.)However, the other equality ${\mathrm{𝗅𝗈𝗈𝗉}}^{g(p)}=p$ is significantly harder.The obvious thing to try is path induction, but path induction does not apply to loops such as $p:(\mathrm{𝖻𝖺𝗌𝖾}=\mathrm{𝖻𝖺𝗌𝖾})$ that have both endpoints fixed!A new idea is required, one which can be explained both in terms of classical homotopy theory and in terms of type theory.We begin with the former.