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

$$\mathrm{𝖼𝗈𝖽𝖾}:\mathbb{N}\to \mathbb{N}\to 𝒰,$$

defined by double recursion over $\mathbb{N}$ as follows:

$\mathrm{𝖼𝗈𝖽𝖾}(0,0)$$:\equiv \mathrm{𝟏}$

$\mathrm{𝖼𝗈𝖽𝖾}(\mathrm{𝗌𝗎𝖼𝖼}(m),0)$$:\equiv \mathrm{𝟎}$

$\mathrm{𝖼𝗈𝖽𝖾}(0,\mathrm{𝗌𝗎𝖼𝖼}(n))$$:\equiv \mathrm{𝟎}$

$\mathrm{𝖼𝗈𝖽𝖾}(\mathrm{𝗌𝗎𝖼𝖼}(m),\mathrm{𝗌𝗎𝖼𝖼}(n))$$:\equiv \mathrm{𝖼𝗈𝖽𝖾}(m,n).$

We also define by recursion a dependent function $r:{\prod }_{(n:\mathbb{N})}\mathrm{𝖼𝗈𝖽𝖾}(n,n)$, with

$r(0)$$:\equiv \star$

$r(\mathrm{𝗌𝗎𝖼𝖼}(n))$$:\equiv r(n).$

Theorem 2.13.1.

For all $m\mathrm{,}n\mathrm{:}\mathrm{N}$ we have $\mathrm{(}m\mathrm{=}n\mathrm{)}\mathrm{\simeq }\mathrm{code}\mathrm{(}m\mathrm{,}n\mathrm{)}$.

Proof.

We define

$$\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}:\prod _{m,n:\mathbb{N}}(m=n)\to \mathrm{𝖼𝗈𝖽𝖾}(m,n)$$

by transporting, $\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}(m,n,p):\equiv {\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{\mathrm{𝖼𝗈𝖽𝖾}(m,\text{–})}(p,r(m))$.And we define

$$\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}:\prod _{m,n:\mathbb{N}}\mathrm{𝖼𝗈𝖽𝖾}(m,n)\to (m=n)$$

by double induction on $m,n$.When $m$ and $n$ are both $0$, we need a function $\mathrm{𝟏}\to (0=0)$, which we define to send everything to ${\mathrm{𝗋𝖾𝖿𝗅}}_0$.When $m$ is a successor and $n$ is $0$ or vice versa, the domain $\mathrm{𝖼𝗈𝖽𝖾}(m,n)$ is $\mathrm{𝟎}$, so the eliminator for $\mathrm{𝟎}$ suffices.And when both are successors, we can define $\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}(\mathrm{𝗌𝗎𝖼𝖼}(m),\mathrm{𝗌𝗎𝖼𝖼}(n))$ to be the composite

$$\mathrm{𝖼𝗈𝖽𝖾}(\mathrm{𝗌𝗎𝖼𝖼}(m),\mathrm{𝗌𝗎𝖼𝖼}(n))\equiv \mathrm{𝖼𝗈𝖽𝖾}(m,n)\stackrel{\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}(m,n)}{\to }(m=n)\stackrel{{\mathrm{𝖺𝗉}}_{\mathrm{𝗌𝗎𝖼𝖼}}}{\to }(\mathrm{𝗌𝗎𝖼𝖼}(m)=\mathrm{𝗌𝗎𝖼𝖼}(n)).$$

Next we show that $\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}(m,n)$ and $\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}(m,n)$ are quasi-inverses for all $m,n$.

On one hand, if we start with $p:m=n$, then by induction on $p$ it suffices to show

$$\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}(n,n,\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}(n,n,{\mathrm{𝗋𝖾𝖿𝗅}}_n))={\mathrm{𝗋𝖾𝖿𝗅}}_n.$$

But $\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}(n,n,{\mathrm{𝗋𝖾𝖿𝗅}}_n)\equiv r(n)$, so it suffices to show that $\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}(n,n,r(n))={\mathrm{𝗋𝖾𝖿𝗅}}_n$.We can prove this by induction on $n$.If $n\equiv 0$, then $\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}(0,0,r(0))={\mathrm{𝗋𝖾𝖿𝗅}}_0$ by definition of $\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}$.And in the case of a successor, by the inductive hypothesis we have $\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}(n,n,r(n))={\mathrm{𝗋𝖾𝖿𝗅}}_n$, so it suffices to observe that ${\mathrm{𝖺𝗉}}_{\mathrm{𝗌𝗎𝖼𝖼}}({\mathrm{𝗋𝖾𝖿𝗅}}_n)\equiv {\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝗌𝗎𝖼𝖼}(n)}$.

On the other hand, if we start with $c:\mathrm{𝖼𝗈𝖽𝖾}(m,n)$, then we proceed by double induction on $m$ and $n$.If both are $0$, then $\mathrm{𝖽𝖾𝖼𝗈𝖽𝖾}(0,0,c)\equiv {\mathrm{𝗋𝖾𝖿𝗅}}_0$, while $\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}(0,0,{\mathrm{𝗋𝖾𝖿𝗅}}_0)\equiv r(0)\equiv \star$.Thus, it suffices to recall from §2.8 (http://planetmath.org/28theunittype) that every inhabitant of $\mathrm{𝟏}$ is equal to $\star$.If $m$ is $0$ but $n$ is a successor, or vice versa, then $c:\mathrm{𝟎}$, so we are done.And in the case of two successors, we have

using the inductive hypothesis.∎

In particular, we have

$$\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}(\mathrm{𝗌𝗎𝖼𝖼}(m),0):(\mathrm{𝗌𝗎𝖼𝖼}(m)=0)\to \mathrm{𝟎}$$(2.13.2)

which shows that “$0$ is not the successor of any natural number”.We also have the composite

$$(\mathrm{𝗌𝗎𝖼𝖼}(m)=\mathrm{𝗌𝗎𝖼𝖼}(n))\stackrel{𝖾𝗇𝖼𝗈𝖽𝖾}{\to }\mathrm{𝖼𝗈𝖽𝖾}(\mathrm{𝗌𝗎𝖼𝖼}(m),\mathrm{𝗌𝗎𝖼𝖼}(n))\equiv \mathrm{𝖼𝗈𝖽𝖾}(m,n)\stackrel{𝖽𝖾𝖼𝗈𝖽𝖾}{\to }(m=n)$$(2.13.3)

which shows that the function $\mathrm{𝗌𝗎𝖼𝖼}$ 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 $\mathbb{N}$ can also be used to calculate homotopy groups of spheres.