open import 1Lab.Path.IdentitySystem open import 1Lab.HLevel.Retracts open import 1Lab.HLevel open import 1Lab.Path open import 1Lab.Type open import Data.Dec.Base module Data.Nat.Base where

# Natural Numbersπ

The natural numbers are the inductive type generated by zero and closed under taking successors. Thus, they satisfy the following induction principle, which is familiar:

Nat-elim : β {β} (P : Nat β Type β) β P 0 β ({n : Nat} β P n β P (suc n)) β (n : Nat) β P n Nat-elim P pz ps zero = pz Nat-elim P pz ps (suc n) = Nat-elim (Ξ» z β P (suc z)) (ps pz) ps n iter : β {β} {A : Type β} β Nat β (A β A) β A β A iter zero f = id iter (suc n) f = f β iter n f

Translating from type theoretic notation to mathematical English, the
type of Nat-elim says that if a predicate
`P`

holds of zero, and the truth of
`P(suc n)`

follows from `P(n)`

, then
`P`

is true for every natural number.

## Discretenessπ

An interesting property of the natural numbers, type-theoretically,
is that they are `discrete`

: given
any pair of natural numbers, there is an algorithm that can tell you
whether or not they are equal. First, observe that we can distinguish zero from successor:

zeroβ suc : {n : Nat} β Β¬ zero β‘ suc n zeroβ suc path = subst distinguish path tt where distinguish : Nat β Type distinguish zero = β€ distinguish (suc x) = β₯

The idea behind this proof is that we can write a predicate which is true for zero, and false for any successor. Since we know that β€ is inhabited (by tt), we can transport that along the claimed path to get an inhabitant of β₯, i.e., a contradiction.

suc-inj : {x y : Nat} β suc x β‘ suc y β x β‘ y suc-inj = ap pred where pred : Nat β Nat pred (suc x) = x pred zero = zero

Furthermore, observe that the `successor`

operation is injective, i.e.,
we can βcancelβ it on paths. Putting these together, we get a proof that
equality for the natural numbers is decidable:

Discrete-Nat : Discrete Nat Discrete-Nat zero zero = yes refl Discrete-Nat zero (suc y) = no Ξ» zeroβ‘suc β absurd (zeroβ suc zeroβ‘suc) Discrete-Nat (suc x) zero = no Ξ» sucβ‘zero β absurd (zeroβ suc (sym sucβ‘zero)) Discrete-Nat (suc x) (suc y) with Discrete-Nat x y ... | yes xβ‘y = yes (ap suc xβ‘y) ... | no Β¬xβ‘y = no Ξ» sucxβ‘sucy β Β¬xβ‘y (suc-inj sucxβ‘sucy)

Hedbergβs theorem implies that Nat is a set, i.e., it only has trivial paths.

Nat-is-set : is-set Nat Nat-is-set = Discreteβis-set Discrete-Nat instance H-Level-Nat : β {n} β H-Level Nat (2 + n) H-Level-Nat = basic-instance 2 Nat-is-set

## Arithmeticπ

**Heads up!** The arithmetic properties of operations on
the natural numbers are in the module `1Lab.Data.Nat.Properties`

.

Agda already comes with definitions for addition and multiplication of natural numbers. They are reproduced below, using different names, for the sake of completeness:

plus : Nat β Nat β Nat plus zero y = y plus (suc x) y = suc (plus x y) times : Nat β Nat β Nat times zero y = zero times (suc x) y = y + times x y

These match up with the built-in definitions of _+_ and _*_:

plusβ‘+ : plus β‘ _+_ plusβ‘+ i zero y = y plusβ‘+ i (suc x) y = suc (plusβ‘+ i x y) timesβ‘* : times β‘ _*_ timesβ‘* i zero y = zero timesβ‘* i (suc x) y = y + (timesβ‘* i x y)

The exponentiation operator ^ is defined by recursion on the exponent.

_^_ : Nat β Nat β Nat x ^ zero = 1 x ^ suc y = x * (x ^ y) infixr 8 _^_

## Orderingπ

We define the order relation _β€_ on the natural numbers as an inductive predicate. We could also define the relation by recursion on the numbers to be compared, but the inductive version has much better properties when it comes to type inference.

data _β€_ : Nat β Nat β Type where instance 0β€x : β {x} β 0 β€ x sβ€s : β {x y} β x β€ y β suc x β€ suc y

We define the strict ordering on Nat as well, re-using the definition of _β€_.

_<_ : Nat β Nat β Type m < n = suc m β€ n infix 3 _<_ _β€_

As an βordering combinatorβ, we can define the *maximum* of
two natural numbers by recursion: The maximum of zero and a successor
(on either side) is the successor, and the maximum of successors is the
successor of their maximum.

max : Nat β Nat β Nat max zero zero = zero max zero (suc y) = suc y max (suc x) zero = suc x max (suc x) (suc y) = suc (max x y)

Similarly, we can define the minimum of two numbers:

min : Nat β Nat β Nat min zero zero = zero min zero (suc y) = zero min (suc x) zero = zero min (suc x) (suc y) = suc (min x y)