8.1.1 Getting started
It is not too hard to define functions in both directions between and . By specializing \autorefthm:looptothe to , we have a function defined (loosely speaking) by
Defining a function in the other direction is a bit trickier. Note that the successor function is an equivalence, and hence induces a path in the universe . Thus, the recursion principle of induces a map by and . Then we have , and we can define .
With these definitions, we can even prove that for any , using the induction principle \autorefthm:sign-induction for . (We will prove something more general a little later on.) However, the other equality is significantly harder. The obvious thing to try is path induction, but path induction does not apply to loops such as 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|