When we created the natural numbers, we noted that, except for the number zero, every other number is an immediate successor of another number. This qualification is important because \(5\) is a successor of \(0\) down the number line, but it is not an immediate successor. The immediate and unique successor to \(0\) is \(1\). Thus, a logical arrangement of the natural numbers places \(0\) in first place, followed immediately by \(1\), which is then followed immediately by \(2\), etc. From this arrangement or ordering we can define relations between the numbers.

One of the most elementary relations is the “less than” relation, which allows us to say that because \(1\) is the immediate successor to \(0\), then \(0\) is less than \(1\), i.e., \(0 < 1\). However, this relation—sometimes called strict inequality—doesn’t have a nice property that we want, namely, reflexivity. That is to say, we cannot truthfully assert \(n < n\), for any number \(n\). Therefore, we will focus on a more general relation called “less than or equal to”, \(\leq\), which is reflexive and allows us to write \(n \leq n\), for any \(n\), and which is always true.

And note right away that since any instance of \(m \leq n\) (for any natural numbers \(m\) and \(n\)) is either a true (e.g. \(0 \leq 1\)) or a false (e.g. \(1\leq 0\)) proposition, it follows by the types-as-propositions interpretation that every instance of \(m \leq n\) is a type. Since we are concerned only with the true kind, we will want a way to generate all inhabited types of the form \(m \leq n\).

Because this is an infinite task, we will define the relation \(\leq\) so that it encompasses all instances. In Agda code, the inductive definition is as follows:

data _≤_ : ℕ → ℕ → Set where

  z≤n : ∀ {n : ℕ} → zero ≤ n
  s≤s : ∀ {m n : ℕ} → m ≤ n → suc m ≤ suc n

There are several things going on here.

First, the relation \(\leq\) is declared as a type former. We haven’t seen this yet. In the signature, the type former \(\_\leq\_\) is an operator that takes a natural number, returns another operator that takes a natural number that then returns a type of the form \(m \leq n\). In short, it’s a curried function:

\[\begin{align*} \_\leq\_ &: \mathbb{ℕ → (ℕ} → \mathtt{Set})\\ n \leq\_ &: \mathbb{ℕ} → \mathtt{Set}\\ n \leq m &: \mathtt{Set} \end{align*}\]

As simple as this is, I admit I initially struggled with it. I just couldn’t read it properly. Here’s a more detailed way of looking at it if you’re having trouble: \(\_\leq\_\) is a term of the function type \(\mathbb{N \to (N} \to \mathtt{Set})\), i.e., it’s a function. As such, \(\_\leq\_\) takes a natural number \(n: \mathbb{N}\), and returns the function \(n \leq\_\) of type \(\mathbb{N} \to \mathtt{Set}\). This new function then takes another natural number \(m: \mathbb{N}\) and returns the term \(n \leq m\), whose type is \(\mathtt{Set}\). Yes, that’s right! A type is also a term! It is a term of the type of types or, equivalently, of the universe of types \(\mathtt{Set}\). But for simplicity, we just call a term of \(\mathtt{Set}\) a type.

We can make our lives easier and just say that, \(\_\leq\_\) is a “binary” operator that takes two natural numbers from \(\mathbb{N \times N}\) and returns a type. Thus, when \(\_\leq\_\) takes \((1,2): \mathbb{N\times N}\), it returns the type \(1 \leq 2 : \mathtt{Set}\).

Below the signature, we have the term constructors, that is, the functions that generate the terms of each instance of \(\_ \leq \_\). Since we are using induction, we need a base case and an inductive step, which in turn depends on an inductive hypothesis.

The first constructor, \(\text{z≤n}\) (note the lack of spacing, which indicates that this a constructor name and not a type!), takes any number \(n\) (including \(0\)) and returns a term \(\text{z≤n}\ \{n\}\) of any type whose form is \(0 \leq n\). The use of curly braces means that \(\{n\}\) is an implicit argument, which Agda allows us to omit because it can guess it. So we can simply write \(\text{z≤n} : 0 \leq n\). This means that, any type of the form \(0 ≤ n\) has a term, namely, the constructor \(\text{z≤n}\) itself.

\[\begin{align*} \text{z≤n} &: \forall \{n : \mathbb{N}\} \to 0 \leq n \\ \text{z≤n}\ \{n\} &: 0 \leq n\\ \text{z≤n} &: 0 \leq n \end{align*}\]

The second constructor, \(\text{s≤s}\) (again, no spacing), will take any two numbers \(m\) and \(n\), and will return a term (a function) \(\text{s≤s}\ \{m\ n\}\) of the function type \(m \leq n \to \mathtt{suc}\, m \leq \mathtt{suc}\, n\). We can read this function type as the conditional proposition “if \(m \leq n\) is true, then so is \(\mathtt{suc}\, m \leq \mathtt{suc}\, n\)”. Therefore, we must give \(\text{s≤s}\ \{m\ n\}\) a proof of \(m \leq n\) (the inductive hypothesis, which requires a recursive call), which then gives us a proof of \(\mathtt{suc}\, m \leq \mathtt{suc}\, n\). Again, we can see this more clearly if we use currying:

\[\begin{align*} \text{s≤s} &: \forall \{m\ n : \mathbb{N}\} \to m \leq n \to \mathtt{suc}\ m \leq \mathtt{suc}\ n\\ \text{s≤s}\ \{m\ n\} &: m \leq n \to \mathtt{suc}\ m \leq \mathtt{suc}\ n\\ \text{s≤s}\ \{m\ n\}\ \text{m≤n} &: \mathtt{suc}\ m \leq \mathtt{suc}\ n\\ \text{s≤s m≤n} &: \mathtt{suc}\ m \leq \mathtt{suc}\ n \end{align*}\]

In the last line, the proof/term of \(\mathtt{suc}\ m \leq \mathtt{suc}\ n\) is \(\text{s≤s}\ \{m\ n\}\ \text{m≤n}\) or, more simply, \(\text{s≤s m≤n}\), because we can omit the implicit arguments in curly braces. (Note that the proof of \(m \leq n\) is also written without spaces, like so \(\text{m≤n}\), although it could by any other name as long as it doesn’t have any spaces, to distinguish it from a type.)

Examples

We prove that the type \(0 \leq 1\) is true/inhabited. This is the base case. The type is of the form \(0 \leq n\), so the term we have to exhibit is constructed with \(\text{z≤n}\), which takes as an implicit argument any number \(n\), in this case \(1\), and returns the term \(\text{z≤n}\ \{1\}\) of type \(0 \leq 1\). Omitting the implicit argument, the term reduces to \(\text{z≤n} : 0 \leq 1\). In Agda code the proof is as follows:

_ : 0 ≤ 1
_ = z≤n

The first line claims that \(0 \leq 1\) is inhabited by some term to which we give a dummy name (an underscore). The second line tells us what this dummy term is equivalent to, namely, \(\text{z≤n}\), the constructor itself. Think of the second line as revealing the identity of the mysterious underscore.

Next, we prove that \(1 \leq 2\) is inhabited. This type has two successors on each side (i.e., the successor to \(0\) and the successor to \(1\), respectively), so we have to use the \(\text{s≤s}\) constructor, which will give us a term of \(\mathtt{suc}\, 0 \leq \mathtt{suc}\, 1\), or, which is the same \(1 \leq 2\). We’ll use currying to see how the constructor works:

\[\begin{align} \text{s≤s} &: \forall \{m\ n : \mathbb{N}\} \to m \leq n \to \mathtt{suc}\ m \leq \mathtt{suc}\ n \\ \text{s≤s}\ \{0\ 1\} &: 0 \leq 1 \to \mathtt{suc}\ 0 \leq \mathtt{suc}\ 1\\ \text{s≤s}\ \{0\ 1\}\ \text{z≤n} &: \mathtt{suc}\ 0 \leq \mathtt{suc}\ 1 \\ \text{s≤s z≤n} &: \mathtt{suc}\ 0 \leq \mathtt{suc}\ 1 \\ \text{s≤s z≤n} &: 1 \leq 2 \end{align}\]

Note how on line 2, the function \(\text{s≤s} \{0 1\}\) requires a term of \(0 \leq 1\), which is both the base case we just proved and also the inductive hypothesis. So on line 3 we give it \(\text{z≤n}\). Now we can write the proof in Agda:

_ : 1 ≤ 2
_ = s≤s z≤n

Like before, we start by claiming that the term \(\_\) inhabits \(1\leq 2\). Then we reveal the identity of \(\_\), which is \(\text{s≤s z≤n}\).

Inversion

Since a term/proof of \(\mathtt{suc}\ m \leq \mathtt{suc}\ n\) depends on \(m \leq n\), we can invert the order of the proof by going back from \(\mathtt{suc}\ m \leq \mathtt{suc}\ n\) to \(m \leq n\). For that, we define a new function, call it \(\text{inv-s≤s}\), that, for any numbers \(m\) and \(n\), takes a proof of \(\mathtt{suc}\ m \leq \mathtt{suc}\ n\) and returns a proof of \(m \leq n\). In Agda code:

inv-s≤s : ∀ {m n : ℕ} → suc m ≤ suc n → m ≤ n
inv-s≤s (s≤s m≤n) = m≤n

With currying:

\[\begin{align} \text{inv-s≤s} &: \forall \{m\ n : \mathbb{N}\} \to \mathtt{suc}\ m \leq \mathtt{suc}\ n \to m \leq n\\ \text{inv-s≤s}\ \{m\ n\} &: \mathtt{suc}\ m \leq \mathtt{suc}\ n \to m \leq n\\ \text{inv-s≤s}\ \{m\ n\}\ (\text{s≤s m≤n}) &: m \leq n\\ \text{inv-s≤s}\ (\text{s≤s m≤n}) &: m \leq n\\ \text{inv-s≤s}\ (\text{s≤s m≤n}) &= \text{m≤n} \end{align}\]

What about inverting for \(\text{z≤n}\)? Well, with our \(\text{inv-s≤s}\) we went from “bigger things” to “smaller things”. This is not possible for \(\text{z≤n}\) since in the natural numbers system nothing is smaller than \(0\). However, what we can do is show that, for any number \(m\), if \(m \leq 0\), then \(m\) can only be \(0\) itself. We define a new function, \(\mathtt{inv\text{-}\text{z≤n}}\), for this purpose:

inv-z≤n : ∀ {m : ℕ} → m ≤ 0 → m ≡ 0
inv-z≤n z≤n = refl

Let’s use currying to see why this is the case, setting \(m = 1\):

\[\begin{align} \mathtt{inv\text{-}\text{z≤n}} &: \forall \{m : \mathbb{N}\} \to m \leq 0 \to m \equiv 0\\ \mathtt{inv\text{-}\text{z≤n}}\ \{1\} &: 1 ≤ 0 \to 1 \equiv 0\\ \end{align}\]

We see that if we set \(m\) to be the smallest of the successors, i.e., \(1\), then our function \(\mathtt{inv\text{-}\text{z≤n}}\ \{1\}\) will require a proof of \(1 \leq 0\), for which there is none. If we had set \(m = 2\), then \(\mathtt{inv\text{-}\text{z≤n}}\ \{2\}\) will require a proof of \(2 \leq 0\), which again has none. This will happen if \(m\) is any successor number. Therefore, \(m\) can only be \(0\).

\[\begin{align} \mathtt{inv\text{-}\text{z≤n}} &: \forall \{m : \mathbb{N}\} \to m \leq 0 \to m \equiv 0\\ \mathtt{inv\text{-}\text{z≤n}}\ \{0\} &: 0 ≤ 0 → 0 \equiv 0\\ \mathtt{inv\text{-}\text{z≤n}}\ \{0\}\ \text{z≤n} &: 0 \equiv 0\\ \mathtt{inv\text{-}\text{z≤n}}\ \text{z≤n} &: 0 \equiv 0\\ \mathtt{inv\text{-}\text{z≤n}}\ \text{z≤n} &= \mathtt{refl} \end{align}\]

Recall that any identity type of the form \(n \equiv n\) is always inhabited by a term we call \(\mathtt{refl}\) (reflexivity). It is the proof that anything is equal or identical to itself. The next-to-last line above tells us that \(\mathtt{inv\text{-}\text{z≤n}}\ \text{z≤n}\) is a term of \(0\equiv 0\), and the last line reveals that this term must be \(\mathtt{refl}\) itself.