8.1.1 Getting started

It is not too hard to define functions in both directions between Ω⁒(π•Š1) and β„€. By specializing \autorefthm:looptothe to π—…π—ˆπ—ˆπ—‰:π–»π–Ίπ—Œπ–Ύ=π–»π–Ίπ—Œπ–Ύ, we have a function π—…π—ˆπ—ˆπ—‰β€“:β„€β†’(π–»π–Ίπ—Œπ–Ύ=π–»π–Ίπ—Œπ–Ύ) defined (loosely speaking) by

π—…π—ˆπ—ˆπ—‰n={π—…π—ˆπ—ˆπ—‰β’\centerdotβ’π—…π—ˆπ—ˆπ—‰β’\centerdot⁒⋯⁒\centerdotβ’π—…π—ˆπ—ˆπ—‰βŸnifΒ n>0,π—…π—ˆπ—ˆπ—‰-1⁒\centerdotβ’π—…π—ˆπ—ˆπ—‰-1⁒\centerdot⁒⋯⁒\centerdotβ’π—…π—ˆπ—ˆπ—‰-1⏟-nifΒ n<0,π—‹π–Ύπ–Ώπ—…π–»π–Ίπ—Œπ–ΎifΒ n=0.

Defining a function g:Ω⁒(π•Š1)β†’β„€ in the other direction is a bit trickier. Note that the successor function π—Œπ—Žπ–Όπ–Ό:β„€β†’β„€ is an equivalence, and hence induces a path π—Žπ–Ίβ’(π—Œπ—Žπ–Όπ–Ό):β„€=β„€ in the universePlanetmathPlanetmath 𝒰. Thus, the recursion principle of π•Š1 induces a map c:π•Š1→𝒰 by c(π–»π–Ίπ—Œπ–Ύ):≑℀ and 𝖺𝗉c⁒(π—…π—ˆπ—ˆπ—‰):=π—Žπ–Ίβ’(π—Œπ—Žπ–Όπ–Ό). Then we have 𝖺𝗉c:(π–»π–Ίπ—Œπ–Ύ=π–»π–Ίπ—Œπ–Ύ)β†’(β„€=β„€), and we can define g(p):β‰‘π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—X↦X(𝖺𝗉c(p),0).

With these definitions, we can even prove that g⁒(π—…π—ˆπ—ˆπ—‰n)=n for any n:β„€, using the inductionMathworldPlanetmath principle \autorefthm:sign-induction for n. (We will prove something more general a little later on.) However, the other equality π—…π—ˆπ—ˆπ—‰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:(π–»π–Ίπ—Œπ–Ύ=π–»π–Ίπ—Œπ–Ύ) 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 theoryPlanetmathPlanetmath. We begin with the former.

Title 8.1.1 Getting started