Nope. Okay, thanks for coming.
But seriously, this question is genuinely interesting. Since we as humans understand what we want when we talk about numbers such as 0 or 1, and understand that such notions are distinct, then our theory of natural numbers should also reflect that difference. That is to say, we know that 0 is not equal to 1, but we do not know that our formalization can, or does, differentiate them. In this blog post, we will be using Arend to show something stronger than just 
, that Type Theories (all of the common ones) have decidable equality on the the natural numbers. This means that there is an algorithm, which can either produce a term of (m = n) or (m = n -> Empty).
This property is not trivial either, since there are collections which do not have decidable equality; the reals for instance do not.
To begin, let us define the natural numbers in Arend and discuss their structure.
\data Nat -- The type of natural numbers
| zero : Nat -- zero is a natural number
| S (n : Nat) : Nat -- given a natural number n, we can produce an element S n, which is also a natural number.
We will also want some “helper” types, as follows.
\data Unit -- The Unit Type, which has one constructor. This is analogous to the proposition True.
| t : Unit
\data Empty -- The Empty type, which has no constructors (and thus cannot be introduced). This is analogous to the proposition False. We will also want some basic tools so that our proofs later go smoother.
\func absurdio {A : \Type} (h : Empty) : A \elim h -- If you have an element of the empty type, you can prove anything!
\func transport {A : \Type} (B : A -> \Type) {a a' : A} (p : a = a') (b : B a) : B a' -- If you have a proof of B a, and a proof that a = a', then you have a proof of B a'.
=> coe (\lam i => B (p i)) b right
\func ap {A B : \Type} {a b : A} (f : A -> B) : (a = b)-> (f a = f b) -- If a = b, and f : A -> B is a function, then f a = f b.
=> \lam p => (\lam (t : I) => f (p t))The reader is encouraged to actually run these in Arend but the plain text should also give a good idea of whats going on and being claimed for those who are less interested.
Now we should discuss how we are going to test whether or not natural numbers are equal. That is, we should think about how WE, as human beings, would test whether two numbers were equal.
Consider SSSSSSSSS0 and SSSSSSSS0, are they the same? Well I admit it is hard to tell… so how would we go about solving this issue? Probably your first intuition is the correct one, remove one S from the left, and one from the right, then keep doing that until one term is 0, if they are both zero then you say they are equal, if only one is then you say they are not equal. Let’s put this intuition into a recursive function.
\func isEq (m n : Nat) : \Type -- given two natural numbers, determine if they are equal by:
\elim m,n
| zero,zero => Unit -- noting that if they are both zero then they are equal
| S k, zero => Empty -- noting if one side is a succesor and one is zero then they are not equal
| zero, S l => Empty -- noting if one side is a succesor and one is zero then they are not equal
| S k, S l => isEq k l -- If they are both succesors, then we can remove one S, and then compare them againImportant note here, this is not a proof! This function does not have type m = n or m = n -> Empty! So despite that fact that this algorithm will say that 0 and 1 are distinct, we have not actually shown that to be the case. We could just have easily defined a function which got it wrong.
To remedy this, we need to show that isEq m n -> m =n and that m = n -> isEq m n. Which means that we have categorized the identity type on the naturals (that we know what things are equal and what are not).
Time for some lemmas before that though.
\func isEq_refl {m : Nat} : isEq m m \elim m -- Given any m : Nat, there is a term of isEq m m
| zero => t
| S k => isEq_refl
-- Here is our second implication that we are after!
\func eq_imp_isEq (m n : Nat) : (m = n) -> isEq m n => -- If m = n then isEq m n
\lam h => transport (\lam x => isEq m x) (h) (isEq_refl) -- Observe that this proof is very simple, since m = n implies that Eq m n is in some sense equivalent to Eq m m, which we proved always has a term.
\func succ_eq {m n : Nat} : (m = n) -> (S m = S n) => -- This is also quite a useful lemma, which shows that if two terms are equal, then their succesors are also equal. Again the proof is quite simple.
\lam h => ap (S) (h)Now we will get to the proof we have been waiting for.
\func isEq_imp_eq (m n : Nat) : isEq m n -> (m = n) -- If isEq m n then m = n
\elim m,n
| zero, zero => \lam h => (\lam _ => zero) -- If both m and n are zero then we can show that m = n with the constant path \lam _ => 0. (see blog post on the unit interval and paths for more details).
| S k, zero => \lam h => absurdio h -- In this case isEq m n is false, and so we can derive our conclusion from the priciple of absurdity.
| zero, S k => \lam h => absurdio h -- In this case isEq m n is false, and so we can derive our conclusion from the priciple of absurdity.
| S k, S l => \lam h => succ_eq (isEq_imp_eq k l h) -- This is the only subtle line, but subtle it is! If m = S k, and n = S l, then we are meant to show that is Eq m n 
Eq k l -> S k = S l m = n.
-- Naively, we may wish to take a term h : isEq k l, and return the term isEq_imp_eq k l h but this is a term of type k = l, not of S k = S l! But wait a minute, didn't we have a theorem which said that if k = l then S k = S l, yes! So our actual term has to be succ_eq (isEq_imp_eq k l h).
-- This leads to our last theorem, which we wanted to show. That zero is not equal to S 0 (one)
\func null_not_one : zero = S zero -> Empty => \lam h => eq_imp_isEq (zero) (S zero) (h)Lastly, I promised that this was actually a decidable proposition. That is, that I could construct a term of (m = n) or (m = n -> Empty).
Let’s see that proof now.
\data \infixr 2 or (P Q : \Type) -- The type P or Q, which can be proven by giving a term of P or a term of Q.
| inl (p : P) : P or Q
| inr (q : Q) : P or Q
\func pred (m : Nat) : Nat \elim m -- The predecessor function
| zero => zero -- We adapt the convention that zero has a predecessor, which is itself, this is never called upon
| S k => k -- The predecessor of S k is k
\func pred_eq (m n : Nat) (h : S m = S n) : (m = n) => ap (pred) (h) -- A proof that if m = n then the predecessor of m and n are also equal.
\func decidable_index_adjust {m n : Nat} (h : (m = n) or ((m = n) -> Empty)) : ((S m = S n) or ((S m = S n) -> Empty)) -- The proof that if m = n or m = n -> Empty, then either S m = S n or S m = S n -> Empty. We use this in the next proof similairly to how we use succ_eq in isEq_imp_eq.
\elim h
| inl p => inl (succ_eq p)
| inr l => inr (\lam (h : (S m = S n)) => l (pred_eq m n h))
\func decidable_nat (m n : Nat) : (m = n) or ((m = n) -> Empty) \elim m, n -- The proof that either m = n or m = n -> Empty.
| zero, zero => inl (isEq_imp_eq (zero) (zero) (isEq_refl {zero})) -- If both m and n are zero then they are equal
| S k, zero => inr (\lam h => eq_imp_isEq (S k) (zero) (h)) -- If m = S k and n = zero, then they are not equal
| zero, S k => inr (\lam h => eq_imp_isEq (zero) (S k) (h)) -- If m = S k and n = zero, then they are not equal
| S k, S l => decidable_index_adjust (decidable_nat k l) -- If m = S k and n = S l then decidable_index_adjust (decidable_nat k l) is a proof that either m = n or m = n -> Empty by means of showing that either k = l or k = l -> False.
One who is used to classical mathematics might be a bit underwhelmed by this last theorem but rest assured that in a constructive setting this is really great, since constructivists reject the general law of the excluded middle (LEM). To see why, try and complete the following Arend code (don’t try too hard though).
\func LEM (P : \Type) : P or (P -> Empty) => {?}If you tried this exercise, you have seen why the theorem is interesting. Since we read the above statement as “either we can construct a proof of P or we can construct a proof of not P.” But recall that we cannot, in general, actually do this (there exists propositions which have no proof and whose negations have no proof). Thus, it is actually special that in this case we have a process for which we can produce a proof in one case or the other!
So, to conclude, we have shown the remarkable theorem that 0 and 1 are distinct numbers in our type theory and that the proposition m = n is decidable!