Definitional and Propositional Equality

Two expressions are definitionally equal when the type checker can see it without being asked. Two expressions are propositionally equal when a proof exists, and that proof is a term the program must construct. The split is not a convenience. It is the difference between what the compiler can do automatically and what the programmer must supply, and moving the boundary in either direction changes the language.

Equality by computation

Definitional equality, also called conversion, is the congruence generated by the reduction rules of the language. It holds when two terms have a common reduct: beta reduction for applications, delta reduction for unfolding definitions, iota for eliminating constructors, and the corresponding rules for primitive operations. The relation is reflexive, symmetric, and transitive because it is defined as the equivalence closure of a rewriting relation, and it is a congruence because it holds at every position in a term.

The checker’s job is to decide this relation. In an implementation it is the conversion check that runs inside the kernel, and its algorithm is discussed in Normalisation by Evaluation for Conversion Checking. For a term f (2 + 2) : Vec Bool 4, it must establish that 2 + 2 and 4 are definitionally equal, which it does by reducing the left side. For a term whose type is Vec Bool n where n is a variable bound in the context, no reduction applies and the terms are not definitionally equal unless they are syntactically the same.

That last point is the practical sting. Definitional equality is decidable only because reduction is both confluent and restricted: in a total language every term has a normal form, so comparing normal forms decides the relation, and confluence makes the answer independent of the order in which the normal forms are reached. In a language with general recursion, reduction need not terminate, and the checker would loop. The usual compromise is to reduce only terms built from constants known to be terminating, typically those of a syntactically restricted fragment, and to treat everything else as opaque. A function defined by general recursion does not compute in types, even if its body obviously terminates.

Propositional equality as an indexed family

Propositional equality is a type former. For terms a b : A, the type a = b has exactly one introduction rule: reflexivity, which inhabits a = a. The eliminator, known as J, takes a motive over the second argument, a proof of the motive at reflexivity, a proof of a = b, and produces the motive at b.

J : (P : (b : A) → a = b → Type)
  → P a refl
  → (b : A) → (p : a = b) → P b p

The eliminator encodes the principle that everything true of a by reflexivity is true of anything equal to a. It is the type-theoretic replacement for substitution of equals, and every other equality principle is derived from it. Symmetry, transitivity, and congruence of equality under functions are all definable in a few lines each.

The design consequence is sharp: if the checker cannot see that two things are equal, the program must prove it. For a length-indexed vector, appending an empty vector on the right produces a value indexed by n + 0 rather than by n, so the result cannot be used where Vec A n is expected unless the library provides a lemma n + 0 = n and the program rewrites with it. The rewrite is a computation: eliminating an equality proof substitutes along the motive, and in a total language that substitution is part of the program’s behaviour, not an annotation.

Rewriting as a program transformation

The eliminator’s motive is the program transformation. Given p : n + 0 = n and a value v : Vec A (n + 0), applying J with the motive λk. Vec A k yields Vec A n. Nothing is copied at runtime if the indices are erased; the rewrite is a type-level coercion whose computational content is the identity.

This is why rewriting in dependently typed code looks like function application rather than like a tactic. A helper such as subst takes a family, a proof, and a value, and returns the value at the new index. Tactics in an interactive prover are a notation for building these applications, and the term they build is what the checker sees.

The consequence for library design is the same one that shapes indexed families, where the orientation of an index expression decides how much proving a caller inherits; Dependent Types treats that arithmetic side of the problem.

The subtlety is the orientation of lemmas. A lemma n + 0 = n rewrites occurrences of n + 0 to n, and not the reverse, because the eliminator substitutes the right-hand side for the left in the motive. Libraries therefore orient their lemmas by which direction makes progress in the proofs that use them, and a lemma stated in the wrong direction is not merely inconvenient; it makes some proofs impossible to complete without an additional symmetry step.

Why the two must not be conflated

A checker that treated propositional equality as definitional would be unsound or undecidable, depending on how it was done. The undecidable version allows the checker to use any available proof of equality during conversion; this is equality reflection, discussed below. The unsound version simply assumes that any two types with a proof of equality are interchangeable at the syntax level, which breaks subject reduction.

The distinction also has a computational reading. Definitional equality is equality of meaning: two terms with the same normal form denote the same value. Propositional equality is a statement about a relation, and its proofs carry structure. In the intensional systems that most proof assistants implement, two definitionally equal types are interchangeable in any context, and two propositionally equal types are interchangeable only after transporting along the proof. Transport is an explicit operation with computational content in some systems and none in others.

A concrete consequence: if A and B are propositionally equal but not definitionally equal, a function f : A → C cannot be applied to a value of type B without transporting the value to A first. The transport is the program’s obligation, and the type checker will not do it silently.

Equality reflection and its cost

Extensional type theory adds a rule making the two notions coincide: from a proof p : a = b, conclude that a and b are definitionally equal. Functions are then equal when they agree on all inputs, because function extensionality is derivable, and proofs about equality can be used directly in type checking without transport.

The cost is decidability. If the checker may consult arbitrary proofs during conversion, then type checking requires deciding whether a proof exists, which is undecidable in general. Extensional systems are therefore used as internal languages for reasoning, where the checker can be given hints, rather than as programming languages with automatic checking. NuPRL is the standard example of a system built this way.

Intensional type theory keeps the two apart and pays a different price: the theory does not prove function extensionality or uniqueness of identity proofs, and users must either add them as axioms or work in a system that builds them in. The univalence axiom of homotopy type theory is the most far-reaching such addition, and it is an axiom precisely because it is not derivable from the intensional rules.

What each notion is good for

Definitional equality should cover everything the programmer does not want to think about: arithmetic on literal indices, unfolding of definitions, projection from a constructor. A library that forces users to prove 2 + 2 = 4 is a library with a badly chosen set of reduction rules.

Propositional equality should cover everything that requires a decision: algebraic laws that hold for all inputs, properties of functions defined by recursion, and facts that depend on assumptions. These cannot be decided by computation in general, and pretending otherwise would require the checker to be an oracle.

The engineering question is where to place the boundary, and different systems place it differently. Some compare eta-long forms as well as normal forms, which makes more equalities definitional at the cost of a more expensive comparison. Some add decision procedures for specific theories, such as ring arithmetic, as extensions to conversion. Some restrict the equations that may appear in definitions so that the normaliser stays predictable.

Every choice trades checker complexity against proof burden. A weaker definitional equality means more lemmas for the user and a simpler, faster checker. A stronger one means fewer lemmas and a checker whose behaviour is harder to predict: once the conversion check interleaves reduction with constraint solving, whether a program typechecks can depend on the order in which the solver attacks its constraints. That unpredictability is the reason systems publish their conversion algorithm rather than leaving it implicit; the algorithm is part of the language definition.