# Why Equality?

When I started studying dependent types a few years ago, one question I never got a good answer to was: why is equality such a big deal?

Equality types are, of course, practically important. They're
practically important because we want to prove stuff equal to other
stuff a lot! But why does adding equality types necessitate so much
deep theory about how a dependent type system works?^{1}^{1} After all,
integers, also a complicated concept, can be added cleanly and
independently, even though inductive types are pretty complex.

At first, I came up with an answer based on the importance of identity, but it was unsatisfying. I now think about equality as being about computation. I'd like to explain both views.

Assume for this post a dependently-typed language with equality but
without inductive types.^{2}^{2} Despite their initial simplicity, I think
inductive types are confusing and I do not understand them.

## Identity

My first explanation of the importance of equality is that equality is
the only built-in function of type `A → Prop`

, and therefore is
necessary to give meaning to values.

For any formal system, it is important to ask, what constrains the system to make it correspond to the real world? For dependent type systems, all differences stem from differences between types.

Imagine for a moment a “hostile” dependent type system. How do you know that what it calls the type of natural numbers is the type of natural numbers? Possibly what it calls the type of natural numbers has extra members; or possibly extra properties; or possibly two different numbers are actually equal. How can you tell otherwise?

I discussed this a bit in my post on function extensionality, where I
pointed out that we prove things unequal (a value-level difference) by
mapping one of the values to `⊤`

and the other to `⊥`

(a type-level
difference).

Mapping one value to `⊤`

and one to `⊥`

proves they are different because
those two types are different, and those differences stem from the
fact that one can write `x : ⊤`

but one can never write `x : ⊥`

. Note that
`a : A`

, the basic judgment in dependent type theory, is controlled by
the inference rules we write down. So it makes sense to say that the
fact that those rules treat `⊤`

and `⊥`

differently creates type-level
differences, and those type-level differences create value-level
differences.^{3}^{3} Those value-level differences also rely on the right
elimination rule for values, of course. Different elimination rules
define different types with values that are different in different
ways.

This viewpoint goes some way toward explaining why, in theorem
proving, functions `A → Prop`

are seen as more fundamentally meaningful
than functions `A → bool`

. We write down and prove propositions in `Prop`

;
we don't compute `bool`

values.

So how does equality enter into this?

Equality is important is because it is the type constructor that has value-level arguments and thus allows raising value-level reasoning to the type level. Raising value-level reasoning to the type level allows differences in values to turn into differences in types, and differences in types are the fundamental differences, so equality is what creates differences at the value level. In short form, you would say that the equality type defines value identity.

The equality type is an especially good way to raise value-level
reasoning to type-level reasoning: it is a function `A → Prop`

for all `A`

simultaneously, and it is also very simple, just comparing two
objects.

Without an equality type, the only functions `A → Prop`

would apply only
to particular `A`

and would be user-defined functions like:

(x ↦ if x then ⊤ else ⊥) : bool → Prop

This would be inconvenient, because there would be no generic equality function and no general notion of value identity (just type-specific notions).

This was my first answer, but it wasn't satisfying. It explains why we
need some type from `A → Prop`

to come built-in, but not the peculiar ```
A
→ A → Prop
```

signature of equality.^{4}^{4} At best, I can see an argument
that equality is the simplest, or at least, a very simple such
function. And why define a uniform proposition? I can think of lots
of `nat → Prop`

functions, why aren't those enough?^{5}^{5} Type-specific
functions wouldn't establish a type-generic notion of value identity,
but why is that so important? Perhaps one can argue that if you want
type abstraction and identity, you need an generic `A → Prop`

function.
And if we are going to have two arguments, why equality?^{6}^{6} We could
order every type (arbitrarily) and use an ordering relation, for
example! Even if we think equality is just practically important, why
not add define equality differently, maybe like the following
inductive type:

type (=) {A} (a b : A) ≔ inductive | refl A a : a = a | funext (A → B) f g : (∀ x : A, f x = g x) → f = g

If we use this definition, we get an ugly induction principle (because
`A`

is an index, not a parameter) but why does that matter in a
fundamental sense if all we really want is a function `A → Prop`

?

## Computation

I have a new answer to why equality is important: equality internalizes substitution, which is the core principle of computation in a dependent type system.

Computation in a dependent type system happens by reducing eliminators
applied to known constructors, until no eliminators are left. For
example, if you define `add`

like so:

def add (x : ℕ) : ℕ → ℕ ≔ induct x | 0 ⇒ (y ↦ y) | S x' ⇒ (y ↦ S (add x' y))

and then run `add 3 2`

, we end up applying the eliminator `induct`

for
natural numbers to a constructor `3`

for natural numbers. All
computation happens by rewriting combinations of eliminators and
constructors.

As we know, the most important data type in a dependently typed
language is functions, and they have a constructor, `λ`

, and an
eliminator, application, `(? ?)`

. So when I write `add 3 2`

, actually what
I have is the eliminator for functions, application, applied to a
constructor for functions, `add`

. This eliminator requires a special
sauce: substitution. Since functions are the most important data type,
their computation rule, substitution, is the most important
computation rule.

In most presentations of dependent type systems, substitution is
presented with a relation `a ≡ b`

on terms, which means
"intersubstitutible" and which includes at least all of the
eliminator-constructor reductions. It participates in a bunch of
important rules in the dependent type system, such as the rule that if
`a : A`

and `A ≡ B`

then `a : B`

. This rule is a consequence of the fact
that if `A ≡ B`

, then they can be substituted for one another in the
judgment `a : ?`

.

So far I've described a particular way to look at how a dependent type system is built. Now let's look at equality.

My view is that the equality type is an internalization of
substitution, and therefore an internalization of the main form of
computation. In this view, equality is the combination of a
constructor, where if `a ≡ b`

then you can write `a = b`

, and an
eliminator, where if `a = b`

then you can substitute them in an
arbitrary context.^{7}^{7} At this point, details might require separate
type-level and value-level equality functions, and separate type-level
and value-level eliminators, depending on how your dependent type
system is set up.

In this view, the fact that the constructor can be written in the
cutesy form `(a : A) → a = a`

it a confusing shorthand, and the fact
that the elimination principle is exactly the induction principle for
an inductive type with that one constructor is a strange
coincidence.^{8}^{8} The coincidence must be related to the fact that if
we have *only* this one constructor, we have no *values* that are equal
except for the syntactically equal ones. It's still a little magical
that the constructor gives us the right induction principle, and this
all likely has something to do with parametricity. So some mysteries
remain, but I think linking equality to substitution and thus to
computation is crucial here. It suggests that an equality is a natural
consequence of having functions, the product of a drive to internalize
the meta-theory.

## Future directions

To summarize, my current view of a dependent type system is something like this:

- We start by defining constructors and eliminators; computation proceeds by recognizing eliminator-constructor pairs and rewriting them according to various rules, which we choose to correspond to the real world.
- We then add functions because we want to add hypothetical
reasoning.
^{9}^{9}Dependent types become possible here, and in fact there's no reason not to add them. We pretend that functions work using a similar eliminator-constructor mechanism, but this mechanism includes the new substitution operation, which, because functions are so important, becomes the most important form of computation. - To internalize this form of computation, which unlike the previous forms is tricky enough to warrant internalization, we add equality.

There's a few questions which right now I can't answer:

- Why do the constructor and eliminator for equality types match so
well? The work on HoTT and cubical type theory suggest that this is
not an easy question, since they involve adding new constructors
without changing the eliminator. I suspect the coincidence between
constructor and eliminator is an illusion, and derives from the
fact that pure substitution never "does anything" in some vague
sense; after all, without adding new equality constructors, the
only values that can be proven equal are identical
values.
^{10}^{10}Non-identical*terms*can be proven equal, that's different. - What could it mean to internalize the eliminator-constructor structure of computation that existed before we added functions? Is it trivial? Is it hiding somewhere in the structure of a dependent type theory, such as the fact that eliminator-constructor pairs are considered intersubstitutible? If that's it, how would we internalize eliminator-constructor pairs if we didn't have functions and thus didn't have substitution?
- Are there other ways to define function elimination that don't involve substitution and thus do not require equality? I wrote up one attempt in my Fine language, where functions are given multiple constructors and where elimination does not require substitution.

The framework I presented here for understanding equality and its place is, I think, one good way to structure your understanding of dependent type systems. Let me know if you like it and have any thoughts.

^{1}

^{2}

^{3}

^{4}

^{5}

`A → Prop`

function.^{6}

^{7}

^{8}

*only*this one constructor, we have no

*values*that are equal except for the syntactically equal ones. It's still a little magical that the constructor gives us the right induction principle, and this all likely has something to do with parametricity.

^{9}

^{10}

*terms*can be proven equal, that's different.