## You are here

Home8.1.1 Getting started

## Primary tabs

# 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{\text{--}}}}:\mathbb{Z}\rightarrow(\mathsf{base}=%
\mathsf{base})$ defined (loosely speaking) by

$\displaystyle\centerdot$ |

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.

## Mathematics Subject Classification

03B15*no label found*

- Forums
- Planetary Bugs
- HS/Secondary
- University/Tertiary
- Graduate/Advanced
- Industry/Practice
- Research Topics
- LaTeX help
- Math Comptetitions
- Math History
- Math Humor
- PlanetMath Comments
- PlanetMath System Updates and News
- PlanetMath help
- PlanetMath.ORG
- Strategic Communications Development
- The Math Pub
- Testing messages (ignore)

- Other useful stuff
- Corrections