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