One of the most fundamental notions in type theory is equality. There are various forms of equality, including propositional equality, judgmental equality, typal equality, extensional equality, intensional equality, path equality (a key concept in homotopy type theory), among others. The list goes on, and any deep exploration of the concept of equality could easily expand to book length. Instead of attempting to cover all these notions at once, I believe it’s best to build this blog post incrementally.

Martin-Löf Equality

The Swedish logician Per Martin-Löf pretty much introduced¹ the notion of dependent typing (eponymously known as Martin-Löf type theory) to the world. Every theorem prover/proof assistant in existence owes its origin to Martin-Löf’s seminal work.

A key concept in his type theory is what we call Martin-Löf equality, a dependent type that takes a fixed term x : A and maps any term y : A to the type x ≡ y. I will be using Agda in this blog post. The equality definition in Agda looks like the following:

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

The {A : Set} is a type parameter, meaning the equality type is polymorphic over any type A in the universe Set. refl : x ≡ x is the sole constructor of the equality type. It states that the only way to construct a proof of equality is by showing that a term is equal to itself (reflexivity).

Leibniz Equality

One of the earliest notions of equality was given by the philosopher and mathematician Gottfried Wilhelm Leibniz. Leibniz in his 1686 treatise², Discourse on Metaphysics, asserted the identity of indiscernibles - two objects are equal if and only if they satisfy the same properties.

The above is known as Leibniz Equality. Leibniz equality is usually formalised to state that x ≐ y holds if every property P that holds of x also holds of y. Or,

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

Note the use of Set₁, which represents a hierarchy of types where Set : Set₁, Set₁ : Set₂, etc to bypass Russell’s Paradox and Girard’s Paradox. A recently published work showed that Leibniz Equality is isomorphic to Martin-Löf Equality. The fact that Martin-Löf equality implies Leibniz equality, and vice versa is short enough to be shown here as follows:

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

≐-implies-≡ : ∀ {A : Set} {x y : A}
  → x ≐ y
    -----
  → x ≡ y
≐-implies-≡ {A} {x} {y} x≐y = Qy
  where
    Q : A → Set
    Q z = x ≡ z
    Qx : Q x
    Qx = refl
    Qy : Q y
    Qy = x≐y Q Qx

Footnotes

1. Work by Howard and de Bruijn predates Martin-Löf's work, however, Martin-Löf is credited with formalising dependent types into a coherent framework for constructive mathematics ↩
2. A work from 1686 is by far the oldest paper that I have referred to in my academic career ↩