Leibniz Equality / Identity

Given any type \(A\) and two of its terms, \(x\) and \(y\), we can construct the equality or identity type \(x \equiv_A y\), and the terms of this type (if any) are proofs of their equality. This is known as Martin Löf (ML) equality in type theory.

There is, however, another way to define equality—the Leibnizian way: “If two objects are indiscernible, meaning they share all properties, then they are the same.” This statement is due to Leibniz and called the Principle of the Identity of Indiscernibles (PII).

Recall that a property or relation is a type family \(P: A\to \mathtt{Set}\), that is, a collection of indexed types \(P\ x\), where \(x:A\). What the PII is saying, then, is that, for every \(P\), if \(P\ x\) implies \(P\ y\), then \(x\) an \(y\) are the same, or L equal, denoted \(x \doteq_A y\).

Here’s the Agda code formalizing the idea:

_≐_ : ∀ {A : Set} (x y : A) → Set₁
_≐_ {A} x y = ∀ (P : A → Set) → P x → P y

Recall that in Agda \(\mathtt{Set}\) is the universe of types. So what is \(\mathtt{Set}_1\)? Here we encounter for the first time the use of levels of universes. In my (limited) understanding of the subject, we must use levels of universes to avoid set-theoretical paradoxes. Notice that \(\_\!\doteq\!\_\) is a function into \(\mathtt{Set}_1\), making it a type family. But this family or collection of indexed types belongs to a universe one level up from the original \(\mathtt{Set}\) (which we can also denote \(\mathtt{Set}_0\)), and the reason for this is on the second line, which contains the definition: we are quantifying over type families \(P\). As you may know, unrestricted self-reference leads to paradoxes like “the set of all sets that do not contain themselves”. If we do not use universe levels, then the definition of \(\_\!\doteq\!\_\) would be impredicative, quantifying over a totality which includes the thing being defined, namely, type families.

With that out of the way, what does the code say? On the first line, it says that, for any type \(A\) and any two of its terms \(x\) and \(y\), the family \(\_\!\doteq\!\_\) is a collection of indexed types of the form \(x \doteq_A y\) belonging to the universe \(\mathtt{Set}_1\), one level up from \(\mathtt{Set}_0\). And (second line) each \(x \doteq_A y\) is a dependent-function type whose terms are, naturally enough, dependent functions, e.g. \(x\!\doteq\!y\) (no spacing!), each of which takes a collection \(P\) of indexed types of the lower level \(\mathtt{Set}_0\), returns another function that takes proof of \(P\ x\) and returns a proof of the type \(P\ y\). In type-theoretical notation, the type \(x \doteq_A y\) is defined as:

\[ \prod_{P: A \to \mathtt{Set}} P\ x \to P\ y \]

And each term of this type is a function of the form \(x\!\doteq\!y\), such that:

\[\begin{align*} x\!\doteq\!y &: \textstyle\prod_{P:A \to \mathtt{Set}} P\ x \to P\ y\\ x\!\doteq\!y\ P &: P\ x \to P\ y\\ x\!\doteq\!y\ P\ px &: P\ y \end{align*}\]

The new type \(x \doteq_A y\) is equivalent to the proposition “\(x\) is L-equal to \(y\)”. What does that mean? We’ve just defined \(x\doteq_A y\) as being the dependent function type \(\prod_{P:A\to \mathtt{Set}} P\ x \to P\ y\). The latter, interpreted as a proposition, says: “For any property/relation \(P\), a proof that \(P\) holds of \(x\) implies that \(P\) also holds of \(y\).” So a proof of \(x\doteq_A y\) is a proof of \(\prod_{P:A\to \mathtt{Set}} P\ x \to P\ y\), i.e., a function \(f\) that takes \(P\) and a proof that \(P\) holds of \(x\) (i.e., \(px : P\ x\)), and returns a proof that \(P\) also holds of \(y\) (that is, a term of \(P\ y\)).

Like ML equality, Leibnizian (L) equality is also reflexive, transitive, and symmetric. We turn to this now.

Reflexivity

In ML equality, reflexivity is baked into the definition, that is, we always have proof that a thing is equal to itself: \(\mathtt{refl}\). In L equality, a proof of reflexivity, \(x \doteq_A x\), means that we have a dependent function, call it \(\mathtt{refl}\text{-}\!\doteq\), such that, given some type family \(P\), if we have a proof that \(P\) holds of \(x : A\), then \(\mathtt{refl}\text{-}\!\doteq\) gives us a proof that \(P\) holds of \(x: A\), i.e., returns that same term. In Agda code:

refl-≐ : ∀ {A : Set} {x : A} → x ≐ x
refl-≐ P px  =  px

With currying:

\[\begin{align*} \mathtt{ref}\text{-}\!\doteq &: x \doteq_A x\\ \mathtt{ref}\text{-}\!\doteq &: \textstyle\prod_{P:A\to \mathtt{Set}} \to P\ x \to P\ x \quad (\text{definition}) \\ \mathtt{ref}\text{-}\!\doteq P &: P\ x \to P\ x\\ \mathtt{ref}\text{-}\!\doteq P\ px &: P\ x\\ \mathtt{ref}\text{-}\!\doteq P\ px &= px \end{align*}\]

Transitivity

To prove transitivity in L equality, we will define a new function, \(\mathtt{trans}\text{-}\!\doteq\), which takes a proof \(f: x\doteq y\), a proof \(g: y\doteq z\), and returns proof of \(x\doteq z\).

Now, recall that this is very similar to transitivity in ML equality: if we have proof that \(x \equiv_A y\), and proof that \(y \equiv_A z\), then we have proof that \(x \equiv_A z\). Except that the proofs in ML equality are constants, \(\mathtt{refl}\), making the proof of ML transitivity trivial:

trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl  =  refl

Because a proof of L equality is not a singular “thing” like \(\mathtt{refl}\), but “binary” functions that have to take a type family and a term of an indexed type, saying how \(\mathtt{trans}\text{-}\!\doteq\) works is a little more involved. The Agda code is as follows:

trans-≐ : ∀ {A : Set} {x y z : A} → x ≐ y → y ≐ z → x ≐ z
trans-≐ f g P px  =  g P (f P px)

The PLFA states that the proof follows by a variant of function composition. To see this, let’s use currying first:

\[\begin{align*} \mathtt{trans}\text{-}\!≐ &: x \doteq y \to y \doteq z \to x \doteq z\\ \mathtt{trans}\text{-}\!≐ f &: y \doteq z \to x \doteq z\\ \mathtt{trans}\text{-}\!≐ f\ g &: x \doteq z\\ \end{align*}\]

Our new function \(\mathtt{trans}\text{-}\!\doteq\) takes a proof \(f\) of \(x\doteq y\), that is, a proof that, for any property \(P\), \(P\ x\) implies \(P\ y\), and then a proof \(g\) of \(y\doteq z\), i.e., that for any \(P\), \(P\ y\) implies \(P\ z\), and then returns \(\mathtt{trans}\text{-}\!\doteq f\ g\) as proof of \(x\doteq z\), i.e., proof that, for any \(P\), \(P\ x\) implies \(P\ z\). From here the goal is now to take a particular type family \(P\), a proof \(px\) that \(P\ x\), and return proof that \(P\ z\) follows. So, replacing \(x \doteq z\) by its definition:

\[\begin{align*} \mathtt{trans}\text{-}\!≐ f\ g &: \textstyle\prod_{P:A\to \mathtt{Set}} \to P\ x \to P\ z\\ \mathtt{trans}\text{-}\!≐ f\ g\ P &: P\ x \to P\ z\\ \mathtt{trans}\text{-}\!≐ f\ g\ P\ px &: P\ z \end{align*}\]

Therefore, the proof that \(P\ z\) is implied by \(P\ x\) is \(\mathtt{trans}\text{-}\!≐ f\ g\ P\ px\). But how do we define this value? Remember, \(\mathtt{trans}\text{-}\!≐\) is taking functions \(f\) and \(g\), but we still don’t know what it’s doing with them. The PLFA gives us the clue—function composition:

\[ \mathtt{trans}\text{-}\!≐ f\ g\ P\ px = g\ P\ (f\ P\ px) \]

So we can say that, roughly, \(\mathtt{trans}\text{-}\!\doteq\) is taking functions \(f\) and \(g\) and composing them. That is, we can take \(\mathtt{trans}\text{-}\!≐ f\ g\) as being like \(g\circ f\). It makes sense because the codomain of \(f\) (er, \(f\ P\)) is \(P\ y\), which is the domain of \(g\) (or, rather, \(g\ P\)). So when we apply \(f\), we get \(f\ P\ px\) as a term of \(P\ y\), which is something that \(g\ P\) can take to give use a term \(g\ P\ (f\ P\ px)\) of \(P\ z\), which we are identifying with the term \(\mathtt{trans}\text{-}\!≐ f\ g\ P\ px\):

Symmetry

sym-≐ : ∀ {A : Set} {x y : A} → x ≐ y → y ≐ x
sym-≐ {A} {x} {y} f P  =  qy
  where
    Q : A → Set
    Q z = P z → P x
    qx : Q x
    qx = refl-≐ P
    qy : Q y
    qy = f Q qx

If \(x\) is L-equal to \(y\), then we should expect that \(y\) is L-equal to \(x\). More formally, this means that we can construct a function that takes proof of \(x\doteq y\) and returns proof of \(y \doteq x\). We call it \(\mathtt{sym}\text{-}\!\doteq\):

\[\begin{align*} \mathtt{sym}\text{-}\!\doteq &: x\doteq y \to y \doteq x \\ \mathtt{sym}\text{-}\!\doteq f &: y \doteq x \\ \mathtt{sym}\text{-}\!\doteq f &: \textstyle\prod_{P: A \to \mathtt{Set}} P\ y \to P\ x \\ \mathtt{sym}\text{-}\!\doteq f\ P &: P\ y \to P\ x \\ \mathtt{sym}\text{-}\!\doteq f\ P &=\ ? \\ \end{align*}\]

Here comes the tricky part. For now, I’ve put a question mark where we would put the value of \(\mathtt{sym}\text{-}\!\doteq f\ P\). Note that the latter is a function of type \(P\ y \to P\ x\). Recall that in defining \(x \doteq_A y\), we had \(f\ P\) of type \(P\ x \to P\ y\), with the arrow going in the opposite direction of \(\mathtt{sym}\text{-}\!\doteq f\ P\) (or, if you like, with the domain and codomain swapped).

To reverse the arrow, we first declare a new family \(Q\), such that for any \(z\), we define the indexed type \(Q\ z\) to be itself the function type \(P\ z \to P\ x\), with the arrow now going into \(P\ x\). This way, when we give \(f: \textstyle\prod_{P: A \to \mathtt{Set}} P\ x \to P\ y\) the family \(Q\) as argument, we now have \(f\ Q\) as a higher function of type \(Q\ x \to Q\ y\), i.e.:

\[\begin{align*} f\ Q &: Q\ x \to Q\ y \\ f\ Q &: (P\ x \to P\ x) \to (P\ y \to P\ x) \end{align*}\]

That is where the code after the keyword \(\mathtt{where}\) comes in. It does exactly what we’ve just done:

\[\begin{align*} Q &: A \to \mathtt{Set} \\ Q\ z &= P\ z \to P\ x \end{align*}\]

The next two lines in the code identify the term that \(f\ Q\) takes:

\[\begin{align*} qx &: Q\ x \\ qx &= \mathtt{refl}\text{-}\!\doteq P \end{align*}\]

It says taht \(qx\) is a term of the indexed type \(Q\ x\), which by definition is the same as \(P\ x \to P\ x\). But we just saw above, in the section on Reflexivity, that a term of \(P\ x \to P\ x\) is \(\mathtt{refl}\text{-}\!\doteq P\). So \(qx\) is \(\mathtt{refl}\text{-}\!\doteq P\). Now we have:

\[\begin{align*} f\ Q\ qx &: Q\ y\\ f\ Q\ qx &: P\ y \to P\ x \end{align*}\]

and we identify this term with \(qy\):

\[\begin{align*} qy &: Q\ y \\ qy &= f\ Q\ qx \end{align*}\]

We can now go back to currying our function:

\[\begin{align*} \mathtt{sym}\text{-}\!\doteq f\ P &: P\ y \to P\ x\\ \mathtt{sym}\text{-}\!\doteq f\ P &: Q\ y\\ \mathtt{sym}\text{-}\!\doteq f\ P &= qy = f\ Q\ qx \end{align*}\]

Expressed differently, \(\mathtt{sym}\text{-}\!\doteq\) is a function that, when taking \(f\ P\), it acts the same as when \(f\) by itself takes the family \(Q\) and the term \(qx\), returning proof \(qy\) that whenever \(P\ y\) holds, then \(P\ x\) follows.

Leibniz equality iff Martin Löf equality

The two kinds of equality are equivalent. We prove this by first showing that ML equality implies L equality, or that if \(x\) is ML-equal to \(y\), then \(x\) is L-equal to \(y\). For this we use a function suggestively named \(\equiv\text{-implies-}\!\doteq\):

≡-implies-≐ : ∀ {A : Set} {x y : A} → x ≡ y → x ≐ y
≡-implies-≐ f P  =  subst P f

With currying:

\[\begin{align*} \equiv\text{-implies-}\!\doteq &: x \equiv_A y \to x \doteq_A y\\ \equiv\text{-implies-}\!\doteq f &: x\doteq_A y\\ \equiv\text{-implies-}\!\doteq f &: \textstyle\prod_{P:A\to \mathtt{Set}} P\ x \to P\ y\\ \equiv\text{-implies-}\!\doteq f\ P &: P\ x \to P\ y\\ \equiv\text{-implies-}\!\doteq f\ P &= \mathtt{subst}\ P\ f \end{align*}\]

Recall that we had already constructed a term of \(P\ x \to P\ y\) with substitution.

The other half of the proof involves a function taking proof of \(x\doteq_A y\) and returning a proof of \(x\equiv_A y\). We likewise call it \(\doteq\text{-implies-}\!\equiv\):

≐-implies-≡ : ∀ {A : Set} {x y : A} → x ≐ y → x ≡ y
≐-implies-≡ {A} {x} {y} f  =  qy
  where
    Q : A → Set
    Q z = x ≡ z
    qx : Q x
    qx = refl
    qy : Q y
    qy = f Q qx

Since equality is a relation, and in type theory a relation is a type family, then for the function \(\doteq\text{-implies-}\!\equiv f\) to return proof of the equality \(x\equiv_A y\), it must be defined in terms of \(f\) taking some type family. Like in the proof for symmetry above, we introduce a new type family \(Q\), but this time we define it such that, for any \(z\), the indexed type \(Q\ z\) is the identity type \(x \equiv_A z\).

\[\begin{align*} Q &: A \to \mathtt{Set} \\ Q\ z &= x \equiv_A z \\ \end{align*}\]

Following the definition of \(f: x\doteq_A y\), when \(f\) takes a family \(Q\), it returns a function of type \(Q\ x \to Q\ y\), which is equivalent to \(x\equiv_A x \to x\equiv_A y\). This means that, for terms \(qx\) and \(qy\), we have:

\[\begin{align*} qx &: Q\ x \\ qx &: x \equiv_A x \\ qx &= \mathtt{refl} \\ qy &: Q\ y \\ qy &: x \equiv_A y \\ \end{align*}\]

Therefore, \(f\) is a function that, for any property or relation \(Q\), returns a function \(f\ Q\) that takes proof that \(Q\) holds of \(x\) and returns proof that \(Q\) holds for \(y\) as well. In the present case, we’ve defined \(Q\) to be the relation of ML equality. Thus \(f\ Q\) is the function that takes a proof \(qx\) that \(x\) is ML-equal to itself and returns a proof \(qy\) that \(x\) is likewise ML-equal to \(y\). Thus \(f\ Q\ qx = qy : Q\ y\). 😵‍💫

\[\begin{align*} f\ Q &: Q\ x \to Q\ y \\ f\ Q &: x \equiv x \to x \equiv y\\ f\ Q\ qx &: x \equiv y\\ f\ Q\ qx &= qy \end{align*}\]