Total Order

Let’s recap: the natural numbers system, \(\mathbb{N}\), can have its elements ordered by inequality, \(\leq\), which, as a relation, has the properties of reflexivity, transitivity and antisymmetry. This makes \(\mathbb{N}\) a partial order. In type-theoretical terms, this means 1) that we can construct a term or proof of the type \(n \leq n\) (reflexivity), 2) that if we have the inhabited types \(m \leq n\) and \(n \leq p\), then we can construct a term or proof of \(m \leq p\) (transitivity), and 3) that if we have the inhabited types \(m \leq n\) and \(n \leq m\), then we can construct a term or proof of the identity type \(m \equiv n\) (antisymmetry).

There’s another property that \(\mathbb{N}\) has: any two naturals can be compared with \(\leq\). Not all partial orders have this property. Consider a genealogical tree ordered by the ancestor relation: siblings and cousins cannot be compared with the ancestor relation. But all natural numbers can be compared with respect to \(\leq\). So, for any two naturals \(n\) and \(m\), it must be the case that \(m \leq n\) or \(n \leq m\) or both. Type-theoretically, one or the other is inhabited, or both are inhabited in the case where \(m \equiv n\) is inhabited. Partial orders that satisfy this property are called total orders.

In type theory we translate the property of total order for \(\mathbb{N}\) by defining a new type family \(\mathtt{Total}'\).¹ In Agda code:

data Total′ : ℕ → ℕ → Set where

  forward′ : ∀ {m n : ℕ} → m ≤ n → Total′ m n

  flipped′ : ∀ {m n : ℕ} → n ≤ m → Total′ m n

As a reminder, a type family is a collection of types, and each member type of the family is indexed by two numbers: \(\mathtt{Total}'\ m\ n\). Since a type can be interpreted as a proposition, a type family can also be interpreted as a collection of propositions that says: “either \(m\leq n\) or \(n\leq m\) (or both)”, with each member proposition/type expressing one of the disjuncts.

How exactly does each member type express one of the disjuncts? The definition tells us that each type \(\mathtt{Total}'\ m\ n\) is proved/inhabited by one of two constructors: \(\mathtt{forward}'\), which provides the term/proof for the case when \(m\leq n\); and \(\mathtt{flipped}'\), which provides the term/proof for the case when \(n\leq m\).

For instance, we have the concrete type \(\mathtt{Total}\ 5\ 6\), whose term/proof is constructed with \(\mathtt{forward}'\):

\[\begin{align*} \mathtt{forward}' &: \forall \{m\ n : \mathbb{N}\} \to m \leq n \to \mathtt{Total}'\ m\ n\\ \mathtt{forward}'\ \{5\ 6\} &: 5 \leq 6 \to \mathtt{Total}'\ 5\ 6\\ \mathtt{forward}'\ \{5\ 6\}\ 5\!\!\leq\!\! 6 &: \mathtt{Total}'\ 5\ 6 \end{align*}\]

We also have \(\mathtt{Total}\ 8\ 7\), whose term/proof is constructed with \(\mathtt{flipped}'\):

\[\begin{align*} \mathtt{flipped}' &: \forall \{m\ n : \mathbb{N}\} \to n \leq m \to \mathtt{Total}'\ m\ n\\ \mathtt{flipped}'\ \{8\ 7\} &: 7 \leq 8 \to \mathtt{Total}'\ 8\ 7\\ \mathtt{flipped}'\ \{8\ 7\}\ 7\!\!\leq\!\! 8 &: \mathtt{Total}'\ 8\ 7 \end{align*}\]

In the case of \(\mathtt{Total}\ 9\ 9\), the proof/term is constructed with either constructor, since the order of their arguments is irrelevant.

To show that every indexed type \(\mathtt{Total}'\ m\ n\) of the type family \(\mathtt{Total}'\) is inhabited, we can check number by number. But to make things easier, we can use induction over both variables \(m\) and \(n\) and do a case analysis. For that, we use another function, call it \(\text{≤-total}\), that, given two base cases and one inductive case, will return a term of \(\mathtt{Total}'\ m\ n\) constructed by either \(\mathtt{forward}'\) or \(\mathtt{flipped}'\):

≤-total : ∀ (m n : ℕ) → Total′ m n
≤-total 0    n                         =  forward′ z≤n
≤-total (suc m) 0                      =  flipped′ z≤n
≤-total (suc m) (suc n) with ≤-total m n
...                        | forward′ m≤n  =  forward′ (s≤s m≤n)
...                        | flipped′ n≤m  =  flipped′ (s≤s n≤m)

First base case: \(\text{≤-total}\) takes \(0\) and any number \(n\) (including zero):

\[\begin{align*} \text{≤-total} &: \forall\ (m\ n : \mathbb{N}) \to \mathtt{Total}'\ m\ n\\ \text{≤-total}\ 0\ n &: \mathtt{Total}'\ 0\ n\\ \text{≤-total}\ 0\ n &= \mathtt{forward}'\ \text{z≤n}\\ \end{align*}\]

That is, \(\text{≤-total}\ 0\ n\) is a term of \(\mathtt{Total}'\ 0\ n\), judgmentally equivalent to the term constructed with \(\text{forward}'\) applied to \(\text{z≤n}: 0 \leq n\).

The second base case is when \(\text{≤-total}\) takes any successor \(suc\ m\) and \(0\).²

\[\begin{align*} \text{≤-total} &: \forall\ (m\ n : \mathbb{N}) \to \mathtt{Total}'\ m\ n\\ \text{≤-total}\ (suc\ m)\ 0 &: \mathtt{Total}'\ (suc\ m)\ 0\\ \text{≤-total}\ (suc\ m)\ 0 &= \mathtt{flipped}'\ \text{z≤n}\\ \end{align*}\]

Example:

\[\begin{align*} \text{≤-total}\ 1\ 0 &: \mathtt{Total}'\ 1\ 0\\ \text{≤-total}\ 1\ 0 &= \mathtt{flipped}'\ \text{z≤n}\\ \end{align*}\]

where

\[\begin{align*} \mathtt{flipped}' &: \forall \{m\ n : ℕ\} \to n ≤ m \to \mathtt{Total}'\ m\ n\\ \mathtt{flipped}'\ \{1\ 0\} &: 0 ≤ 1 \to \mathtt{Total}'\ 1\ 0\\ \mathtt{flipped}'\ \{1\ 0\}\ \text{z≤n} &: \mathtt{Total}'\ 1\ 0\\ \mathtt{flipped}'\ \text{z≤n} &: \mathtt{Total}'\ 1\ 0 \end{align*}\]

As before, we then proceed with the inductive case “assuming” a inductive hypothesis. But here we face something new: because we have two base cases on account of there being two constructors, we will also have two inductive hypotheses; that is, the term \(\text{≤-total}\ m\ n\) is computed with either \(\mathtt{forward}'\) or \(\mathtt{flipped}'\). As a consequence, the inductive step will depend on two inductive hypotheses.

This is expressed in Agda with the following syntax:

≤-total (suc m) (suc n) with ≤-total m n
...                        | forward′ m≤n  =  forward′ (s≤s m≤n)
...                        | flipped′ n≤m  =  flipped′ (s≤s n≤m)

This took me a while to read properly. Here’s one way to interpret the code:

1. The inductive-step term ≤-total (suc m) (suc n), which is on the extreme left, is judgmentally the same as forward′ (s≤s m≤n), on the extreme right, provided the inductive hypothesis ≤-total m n (center) is computed with forward′ m≤n (center, second line).
2. The inductive-step term ≤-total (suc m) (suc n), is judgmentally the same as flipped′ (s≤s n≤m), provided the inductive hypothesis ≤-total m n is computed with flipped′ n≤m (center, third line).

The middle column, where we use the keyword “with”, has the inductive hypothesis and (below it) the two ways it can be constructed. For more of an explanation on the syntax, refer to the PLFA or the Agda documentation.

With the induction proof completed, we conclude that for any natural numbers \(m\) and \(n\), each indexed type \(\mathtt{Total}'\ m\ n\) of the type family \(\mathtt{Total}'\) is inhabited, meaning that, for \(\mathbb{N}\), the proposition “either \(m\leq n\) or \(n\leq m\) (or both)” holds. Therefore, \(\mathbb{N}\) is a total order. \(\blacksquare\)