2.13 Natural numbers
We use the encode-decode method to characterize the path space of the natural numbers, which are also a positive type. In this case, rather than fixing one endpoint, we characterize the two-sided path space all at once. Thus, the codes for identities are a type family
defined by double recursion over as follows:
For all we have .
by transporting, . And we define
by double induction on . When and are both , we need a function , which we define to send everything to . When is a successor and is or vice versa, the domain is , so the eliminator for suffices. And when both are successors, we can define to be the composite
Next we show that and are quasi-inverses for all .
On one hand, if we start with , then by induction on it suffices to show
But , so it suffices to show that . We can prove this by induction on . If , then by definition of . And in the case of a successor, by the inductive hypothesis we have , so it suffices to observe that .
On the other hand, if we start with , then we proceed by double induction on and . If both are , then , while . Thus, it suffices to recall from §2.8 (http://planetmath.org/28theunittype) that every inhabitant of is equal to . If is but is a successor, or vice versa, then , so we are done. And in the case of two successors, we have
using the inductive hypothesis. ∎
In particular, we have
which shows that “ is not the successor of any natural number”. We also have the composite
which shows that the function is injective.
We will study more general positive types in http://planetmath.org/node/87578Chapter 5,http://planetmath.org/node/87579Chapter 6. In http://planetmath.org/node/87582Chapter 8, we will see that the same technique used here to characterize the identity types of coproducts and can also be used to calculate homotopy groups of spheres.
|Title||2.13 Natural numbers|