There is a built-in module for natural numbers, which defines the arithmetic operations and boolean relations, including a boolean-valued equality. We import and augment this with some propositions and predicates. The (unicode-renamed) definition of natural numbers is commented below. \AgdaHide{ \begin{code} module Nat where \end{code} } \begin{code} open import Agda.Builtin.Nat renaming (Nat to ℕ) hiding (_<_) public {- data ℕ : Set where zero : ℕ suc : ℕ → ℕ -} \end{code} \AgdaHide{ \begin{code} open import Decidable \end{code} } The built-in boolean-valued equality \inline{_==_} can be evaluated to check that \inline{1 + 1 == 2} is \inline{true}. However, this is not useful as a lemma. Instead, we would like to have a binary predicate for natural numbers which gives either a proof of equality or a proof of inequality. Such a predicate is itself a proof that equality of natural numbers is decidable, given the definition of \inline{Decidable≡} above. The proof is by case analysis on the arguments. In the case where both numbers are zero, they can be proven equal simply by \inline{refl}. Where only one number is a successor, they can be proven not equal by doing case analysis on what their equality would be. As the only constructor for \inline{_≡_} requires that the left and right sides are the same, and \inline{zero} cannot be unified with \inline{suc _}, the cases are empty. Finally, if both numbers are successors, check if their predecessors are equal. If so, then equality follows. Otherwise, assuming the numbers are equal leads to a contradiction. \begin{code} natEq : Decidable≡ ℕ natEq zero zero = yes refl natEq zero (suc m) = no λ () natEq (suc n) zero = no λ () natEq (suc n) (suc m) with natEq n m ... | yes refl = yes refl ... | no n≢m = no λ { refl → n≢m refl } \end{code} A propositional order relation on the natural numbers can be defined as usual. \begin{code} data _≤_ : ℕ → ℕ → Set where 0≤n : ∀{n} → zero ≤ n sn≤sm : ∀{n m} → n ≤ m → suc n ≤ suc m _<_ : ℕ → ℕ → Set n < m = suc n ≤ m \end{code} In the definition of `$\leq$', the type is \emph{indexed} by a pair of natural numbers, rather than parametrised (given specific names, on the left side of the colon). This is an example of a dependent type. The constructors do not produce values of the same type. Moreover, there are types for which there are no constructors. For example, there is no way of constructing \inline{1 ≤ 0}. In this manner, dependent types can describe predicates. The relation \inline{_≤_} is reflexive and transitive. \begin{code} ≤refl : ∀{n} → n ≤ n ≤refl {zero} = 0≤n ≤refl {suc n} = sn≤sm ≤refl ≤trans : ∀{x y z} → x ≤ y → y ≤ z → x ≤ z ≤trans 0≤n y≤z = 0≤n ≤trans (sn≤sm x≤y) (sn≤sm y≤z) = sn≤sm (≤trans x≤y y≤z) \end{code} If $n < m$ then $m \not\leq n$, and if $m \leq n$ then $n \not< m$. This can be expressed as a single proposition. To derive $\bot$, recurse on $n$ and $m$ until one of them is $0$, at which point there is either no constructor for $n < m$ or no constructor for $m \leq n$. \begin{code} ℕdisorder : ∀{n m} → n < m → m ≤ n → ⊥ ℕdisorder (sn≤sm n