 ## By Pavel Panchekha

### 27 November 2017

Share under CC-BY-SA.

Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation.

# 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?11 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.22 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.33 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.44 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?55 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?66 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.77 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.88 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.99 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.1010 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.

## Footnotes:

1

After all, integers, also a complicated concept, can be added cleanly and independently, even though inductive types are pretty complex.

2

Despite their initial simplicity, I think inductive types are confusing and I do not understand them.

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.

4

At best, I can see an argument that equality is the simplest, or at least, a very simple such function.

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.

6

We could order every type (arbitrarily) and use an ordering relation, for example!

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.

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.

9

Dependent types become possible here, and in fact there's no reason not to add them.

10

Non-identical terms can be proven equal, that's different.