A common way to define equality in type theories, attributed to Per Martin-Löf, is as follows: a == b is a type with two parameters a and b, and it has a single constructor refl x with type x == x.

You might find this weird: the two parameters feel a bit useless since they’ll always be the same. And you’d be right: them being the same is the whole point of this being an equality. The way this works is that if you need a proof that two types are equal then you just take a a == b a argument.

So what can you do with an a == b? My favorite definition is the one from the HoTT book: from the definition of the type, we automatically get a “destructor” function1 :

transport: (a: Type) -> (b: Type) -> (f: Type -> Type) -> a == b -> f a -> f b

This function says: if a == b, then I can turn a f a into a f b for any function f. What I find insanely cute, and what compelled me to write this, is that this single function is enough to define a reasonable notion of equality.

Here is a proof of symmetry, in a suspiciously Rust-looking dependent lambda-calculus:

let symmetry(a: Type, b: Type, ab: a == b) -> b == a =
    transport a b (|x: Type| x == a) ab (refl a)

Here’s how it works: the function being transported is |x| x == a. So given a == b, transport will turn a == a into b == a. We can build a a == a using refl, so we win!

Here is transitivity:

let transitivity(a: Type, b: Type, c: Type, ab: a == b, bc: b == c) -> a == c =
    (transport b c (|x: Type| a == x) bc) ab

The idea is similar: we transport |x| a == x from b to c.

That’s all I had to say, I don’t know why this feels so good to my brain but now you can taste it too! If you enjoyed this, go read the HoTT book.

  1. Apparently this turns the type into its Church encoding. You may enjoy this related fun paper. ↩