Identity Types and Addition in Agda

We saw that one potential difficulty in understanding addition in Agda, following the book PLFA, is that the propositional equality symbol \(\equiv\) is not really explained until much later in the book. If one is not careful, one might think that it works the same as the definitional (also called judgmental) equality symbol \(=\).

To recap, when we use \(\equiv\), we are introducing a new type—the identity type. And we form an identity type on the basis of a judgmental equality. For example, if we know that the terms \(a,b\) of type \(A\) are definitionally/judgmentally equal, i.e., \(a = b\), then we can form the type \(a \equiv b\). And the terms of \(a \equiv b\) are different from the terms of \(A\). In the literature on type theory, terms of identity types are called identifications or even paths (because it is helpful to think of identity types as spaces).

I won’t go into the intricate (and confusing!) details of identity types, because I don’t think, at this stage, I’m capable enough to make 100% sense of them. Suffice to say that when we have an identity type of the form \(a \equiv x\),¹ where \(a: A\) and \(x\) is a variable standing for any other term of type \(A\), the only term we can confidently assert exists is the term \(\mathtt{refl}: a \equiv a\).²

\(\mathtt{refl}\) (short for reflexivity) is the shortest identification or path from any term to itself. We can think of \(\mathtt{refl}\) as the obvious proof that anything is equal to itself.

Thus, returning to our previous example of addition, what we need to do to prove the proposition/type \(3 + 4 ≡ 7\) is show that it is equivalent to the identity type \(7 \equiv 7\), whose guaranteed proof/term is \(\mathtt{refl}\). That is the purpose of equational reasoning in Agda.

Let’s take a look again at the code we encountered last time:

_ : 3 + 4 ≡ 7
_ = 
  begin
  3 + 4
  ≡⟨⟩
  (suc (suc (suc zero))) + (suc (suc (suc (suc zero))))
  ≡⟨⟩
  suc (suc (suc (suc (suc (suc (suc zero))))))
  ≡⟨⟩
  7
  ∎

To repeat, since the type \(3 + 4 \equiv 7\) is formed from the terms \(3 + 4: \mathbb{N}\) and \(7: \mathbb{N}\), we need to show that the one can be reduced to the other. If we are successful, then we’ve shown that the type \(3 + 4 \equiv 7\) is the same as the type \(7 \equiv 7\). We know from the entry building the naturals that \(3: \mathbb{N}\) is \(\mathtt{ (suc (suc (suc\ zero)))}\) and that \(4: \mathbb{N}\) is \(\mathtt{(suc (suc (suc (suc\ zero))))}\). Therefore, the term \(3 + 4\) is the same as the term:

(suc (suc (suc zero))) + (suc (suc (suc (suc zero))))

Next, we apply the definition of addition, and we end up with the term:³

suc (suc (suc (suc (suc (suc (suc zero))))))

But the latter is just the long form of \(7\). Our reduction was successful, and the proof ends. Therefore, we can conclude that \(3 + 4 ≡ 7\) is just another way of writing \(7 ≡ 7\), which as a proposition says “7 is equal to itself”. An obvious and tautologous proposition, whose proof is trivial. Our dummy term \((\_)\) is that proof.

But, recall that for any type of the form \(a \equiv a\), we are guaranteed the term/proof \(\mathtt{refl}\), and since \(7 \equiv 7\) is of that form, we could also have written the above as:

_ : 3 + 4 ≡ 7
_ = refl

If you enter that in Agda and compile, it will go through! The conclusion here is that our dummy term \((\_)\) is definitionally (or judgmentally) the same as \(\mathtt{refl}\).

At first, it might seem that we can write \(\mathtt{refl}\) for any identity type, but this is not the case. Suppose we attempt the following:

_ : 3 + 3 ≡ 7
_ = refl

This will not work. Let’s work it out using equational reasoning:

_ : 3 + 3 ≡ 7
_ = 
  begin
  3 + 3
  ≡⟨⟩
  (suc (suc (suc zero))) + (suc (suc (suc zero)))
  ≡⟨⟩
  (suc (suc (suc (suc (suc (suc zero)))))
  ≢
  7
  ∎

In this pseudo-code, we can see that our attempt at reduction gives us \(\mathtt{(suc (suc (suc (suc (suc (suc\ zero)))))}\), which is the long form of \(6\), not of \(7\). Thus, \(3 + 3 \equiv 7\) is not equivalent to \(7 \equiv 7\). Since the reduction fails, our dummy term \((\_)\) cannot be any term of the type \(3 + 3 \equiv 7\). In fact, this identity type is empty. Interpreted as a proposition, this means the proposition “3 plus 3 equals 7” is false.

Did any of that make sense?