Why Equality?

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.³ [³ 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.⁴ [⁴ 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?⁵ [⁵ 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?⁶ [⁶ 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?

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.⁷ [⁷ 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.⁸ [⁸ 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.

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.⁹ [⁹ 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.¹⁰ [¹⁰ 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.