8.1.1 Getting started

It is not too hard to define functions in both directions between $\Omega(\mathbb{S}^{1})$ and $\mathbb{Z}$ . By specializing \autorefthm:looptothe to $\mathsf{loop}:\mathsf{base}=\mathsf{base}$ , we have a function $\mathsf{loop}^{\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}}:\mathbb{Z}% \rightarrow(\mathsf{base}=\mathsf{base})$ defined (loosely speaking) by

$\mathsf{loop}^{n}=\begin{cases}\underbrace{\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}% \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\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}}_{n}&\text{if $n>0$,}\\ \underbrace{\mathord{{\mathsf{loop}}^{-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\,$}}}\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\,$% }}}\cdots\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}}}_{-n}&\text{if $n<0$,}\\ \mathsf{refl}_{\mathsf{base}}&\text{if $n=0$.}\end{cases}$

Defining a function $g:\Omega(\mathbb{S}^{1})\to\mathbb{Z}$ in the other direction is a bit trickier. Note that the successor function $\mathsf{succ}:\mathbb{Z}\to\mathbb{Z}$ is an equivalence, and hence induces a path $\mathsf{ua}(\mathsf{succ}):\mathbb{Z}=\mathbb{Z}$ in the universe $\mathcal{U}$ . Thus, the recursion principle of $\mathbb{S}^{1}$ induces a map $c:\mathbb{S}^{1}\to\mathcal{U}$ by $c(\mathsf{base}):\!\!\equiv\mathbb{Z}$ and $\mathsf{ap}_{c}(\mathsf{loop}):=\mathsf{ua}(\mathsf{succ})$ . Then we have $\mathsf{ap}_{c}:(\mathsf{base}=\mathsf{base})\to(\mathbb{Z}=\mathbb{Z})$ , and we can define $g(p):\!\!\equiv\mathsf{transport}^{X\mapsto X}(\mathsf{ap}_{c}(p),0)$ .

With these definitions, we can even prove that $g(\mathsf{loop}^{n})=n$ for any $n:\mathbb{Z}$ , using the induction principle \autorefthm:sign-induction for $n$ . (We will prove something more general a little later on.) However, the other equality $\mathsf{loop}^{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:(\mathsf{base}=\mathsf{base})$ 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.

Title	8.1.1 Getting started
\metatable