Definitional Equality

Definition

In type theory, definitional equality (or judgmental equality) is a metatheoretic relation between terms of the same type, denoted by the metatheoretic judgment $\Gamma ⊢a\equiv b:A$. It represents equality by definition or computational reduction. If two terms are definitionally equal, they are treated as identical by the type checker.

Equivalence Relation

Definitional equality forms an equivalence relation on well typed terms, satisfying reflexivity, symmetry, and transitivity.

$$\frac{\Gamma ⊢a:A}{\Gamma ⊢a\equiv a:A}\frac{\Gamma ⊢a\equiv b:A}{\Gamma ⊢b\equiv a:A}\frac{\Gamma ⊢a\equiv b:A\Gamma ⊢b\equiv c:A}{\Gamma ⊢a\equiv c:A}$$

Congruence

It satisfies congruence, meaning equality is preserved under all type formers and term formers. Applying definitionally equal functions to definitionally equal arguments yields definitionally equal results.

Computational Rules

Definitional equality is generated by structural rules and computational rules, primarily beta reduction and eta conversion.

Beta Reduction

Beta reduction specifies the computational behavior of an eliminator applied to a constructor. For function types, applying a lambda abstraction to an argument definitionally reduces to substitution.

$(\lambda x.t)u\equiv t[u/x]$

Eta Conversion

Eta conversion enforces uniqueness principles for elements of a type. For function types, it asserts a function is definitionally equal to its pointwise application.

$f\equiv \lambda x.fx$

Relation to Propositional Equality

Definitional equality is a metatheoretic property of the deductive system. Propositional equality is represented internally by the identity type.

By the reflection rule, definitional equality implies propositional equality. If $\Gamma ⊢a\equiv b:A$, we can construct a term of type $a{=}_{A}b$ using the reflexivity constructor.

The converse holds in extensional type theory but fails in intensional type theory and homotopy type theory.

Decidability

In standard intensional type theory, definitional equality is designed to be strongly normalizing and decidable, guaranteeing algorithmic type checking. In extensional systems, definitional equality is undecidable because it collapses with propositional equality.

References

hott2013-book

References

hott2013-book

In Higher Observational Type Theory, definitional equality is where syntactically one term can be replaced by another simply by substituting definitions.