nLab judgmental equality

This article is about the notion of equality as a judgment. For equality as a proposition or predicate, see propositional equality. For equality as a type, see typal equality. For other notions of equality, see equality.

---

Idea

In logic and type theory, there are two related notions of equality, judgmental equality and definitional equality.

• Judgmental equality is a notion of equality in type theory which is defined to be a judgment, as opposed to a proposition (propositional equality) or a type (typal equality).

• Definitional equality is the equivalence relation on syntactic expressions (types, terms, propositions, contexts, whatever) which states that two syntactic expressions are equivalent if they have the same meaning. Definitional equality encompasses both syntactic equality and alpha-equivalence, as well as equivalence of abbreviations and so forth.

According to PML (1980), p. 31:

Definitional equality is intensional equality, or equality of meaning (synonymy). [] It is a relation between linguistic expressions [] Definitional equality is the equivalence relation generated by abbreviatory definitions, changes of bound variables and the principle of substituting equals for equals. [] Definitional equality can be used to rewrite expressions [].

on p. 60:

… intensional (sameness of meaning) …

In a similar manner to the usual implicit notion of meta-theoretic conversion and explicit conversion in dependent type theory, as well as the usual implicit notion of meta-theoretic parametricity and explicit parametricity in parametric dependent type theory, dependent type theories can be distinguished between those with

• explicit definitional equality, which have a separate equality to explicitly represent definitional equality in the syntax of the theory itself. The vast majority of dependent type theories have explicit definitional equality.

• meta-theoretic definitional equality, which do not have a separate equality for definitional equality. Examples of such dependent type theories include some flavors of objective type theory.

Explicit definitional equality is also used in single-level type theories like Martin-Löf type theory or higher observational type theory for the conversion rules of some inductive types and in cubical type theory and simplicial type theory to define probe shapes for (infinity,1)-categorical types which could not be coherently defined in vanilla dependent type theory.

Remark

There are many different ways that one can conceivably represent definitonal equality explicitly in type theory. The most common approach in the literature defines the definitional equality as an equality judgment, hence the name judgmental equality for definitional equality. Other possible approaches to definitional equality include adding a second judgment of propositions to the theory and defining the definitional equality explicitly as a propositional equality in the style of logic over type theory. This article is solely about the first approach of explicitly defining definitional equality using an equality judgment.

Remark

Equality judgments can hypothetically be used in type theory for things other than definitional equality, such as a shorthand for typal equality in a dependent type theory without only meta-theoretic definitional equality, given by a reflection rule into the identity type:

$$\frac{\Gamma \vdash a \equiv a':A}{\Gamma \vdash \delta_{a, a'}:a =_A a'}$$

This article is solely about judgmental equality in dependent type theory in the sense of explicit definitional equality defined in the syntax by an equality judgment.

Remark

One may consider adding material to this article about the use of an equality judgment in untyped theories, such as in Reuben Goodstein’s 1954 formalization of primitive recursive arithmetic without predicate logic. But for the time being, this article is solely about the most common use of an equality judgment in dependent type theory for definitional equality.

In dependent type theory, there are different kinds of judgmental equalities

• Judgmental equality of terms

• Judgmental equality of types, in dependent type theories with a separate type judgment.

• Judgmental equality of contexts

Judgmental equality of terms is additional structure on types which gives every type the structure of a set in addition to the $\infty$-groupoidal structure on a type from the identity type.

Judgmental equality of types could be thought of as making explicit the implicit coercion of equivalent types as subtypes, and is preserved throughout the type theory as congruences.

Judgmental equality of types is not necessary for dependent type theory with a separate type judgment. It behaves similarly to the equality between sets in structural set theory, and the equality between sets is not necessary for structural set theory since one could simply work with bijections or one-to-one correspondences between sets. Similarly, in dependent type theory, one could just work with definitional isomorphisms instead of judgmental equality of types.

Judgmental equality of terms

Judgmental equality of terms is given by the following judgment:

• $\Gamma \vdash a \equiv a' : A$ - $a$ and $a'$ are judgmentally equal well-typed terms of type $A$ in context $\Gamma$.

Judgmental equality of terms can be contrasted with propositional equality of terms, where equality is a proposition in the sense of first-order logic, and typal equality of terms, where equality is a type.

Inference rules

Judgmental equality is an equivalence relation:

• Reflexivity of judgmental equality

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A}{\Gamma \vdash a \equiv a:A}$$

• Symmetry of judgmental equality

  $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a \equiv b:A}{\Gamma \vdash b \equiv a:A}$$

• Transitivity of judgmental equality

  $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a \equiv b:A \quad b \equiv c:A }{\Gamma \vdash a \equiv c:A}$$

In addition, judgmental equality of terms has congruence rules for substitution, the principle of substitution:

• Principle of substitution for judgmentally equal terms:
  $$\frac{\Gamma \vdash a \equiv b : A \quad \Gamma, x:A, \Delta \vdash c(x):B}{\Gamma, \Delta(a) \vdash c(a) \equiv c(b): B}$$

If there is a separate type judgment, then there is also a separate rule for the principle of substitution into type families.

If one has judgmental equality of types, then the principle of substitution into type families is given by

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a \equiv b : A \quad \Gamma, x:A, \Delta \vdash B(x) \; \mathrm{type}}{\Gamma, \Delta(a) \vdash B(a) \equiv B(b) \; \mathrm{type}}$$

This implies the reflection rule of the equality judgment as shorthand for typal equality because one could derive the following rule:

$$\frac{\Gamma \vdash a \equiv b:A}{\Gamma \vdash \mathrm{refl}_A(a):a =_A b}$$

Otherwise, the principle of substitution into type families is given by definitional transport across judgmental equality as explicit conversion:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a \equiv b : A \quad \Gamma, x:A, \Delta \vdash B(x) \; \mathrm{type}}{\Gamma, \Delta(a) \vdash \mathrm{tr}_{B(-)}^{a \equiv b}:B(a) \cong B(b)}$$

where $A \cong B$ is the definitional isomorphism type defined using natural deduction inference rules. If one doesn’t have a type of definitional isomorphisms, one could define it by components

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a \equiv b : A \quad \Gamma, x:A, \Delta \vdash B(x) \; \mathrm{type}}{\Gamma, y:B(a), \Delta(a) \vdash \mathrm{tr}_{B(-)}^{a \equiv b}(y):B(b)}$$

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a: A \quad \Gamma, x:A, \Delta \vdash B(x) \; \mathrm{type}}{\Gamma, y:B(a), \Delta(a) \vdash \mathrm{tr}_{B(-)}^{a \equiv a}(y) \equiv y:B(a)}$$

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a \equiv b : A \quad \Gamma, x:A, \Delta \vdash B(x) \; \mathrm{type}}{\Gamma, y:B(a), \Delta(a) \vdash \mathrm{tr}_{B(-)}^{b \equiv a}(\mathrm{tr}_{B(-)}^{a \equiv b}(y)) \equiv y:B(a)}$$

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a \equiv b : A \quad \Gamma \vdash b \equiv c : A \quad \Gamma, x:A, \Delta \vdash B(x) \; \mathrm{type}}{\Gamma, y:B(a), \Delta(a) \vdash \mathrm{tr}_{B(-)}^{b \equiv c}(\mathrm{tr}_{B(-)}^{a \equiv b}(y)) \equiv \mathrm{tr}_{B(-)}^{a \equiv c}(y):B(c)}$$

This shows that transport across judgmental equality forms a groupoid.

Either way, this also implies the reflection rule of the equality judgment as shorthand for typal equality because one could derive the following rule

$$\frac{\Gamma \vdash a \equiv b:A}{\Gamma \vdash \mathrm{tr}_{a =_A (-)}^{a \equiv b}(\mathrm{refl}_A(a)):a =_A b}$$

Similarly, for a term $c(x):B(x)$ dependent upon $x:A$, if one has judgmental equality of types, then the principle of substitution across $c(x)$ is given by the rule:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a \equiv b : A \quad \Gamma, x:A, \Delta \vdash c(x):B(x)}{\Gamma, \Delta(b) \vdash c(a) \equiv c(b):B(b)}$$

Otherwise, it is given by a judgmental version of function application to identifications:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a \equiv b : A \quad \Gamma, x:A, \Delta \vdash c(x):B(x)}{\Gamma, \Delta(b) \vdash \mathrm{tr}_{B(-)}^{a \equiv b}(c(a)) \equiv c(b):B(b)}$$

In computation and uniqueness rules

Judgmental equality of terms can be used in the computation rules and uniqueness rules of types:

• Computation rules for dependent product types:

$$\frac{\Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash \lambda(x:A).b(x)(a) \equiv b(a):B(a)}$$

• Uniqueness rules for dependent product types:

$$\frac{\Gamma \vdash f:\prod_{x:A} B(x)}{\Gamma \vdash f \equiv \lambda(x).f(x):\prod_{x:A} B(x)}$$

• Computation rules for negative dependent sum types:

$$\frac{\Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:B(a)}{\Gamma \vdash \pi_1(a, b) \equiv a:A} \qquad \frac{\Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:B(a)}{\Gamma \vdash \pi_2(a, b) \equiv b:B(a)}$$

If one does not have judgmental equality of types, then one would have to use transport across judgmental equality for the second computation rule:

$$\frac{\Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:B(a)}{\Gamma \vdash \mathrm{tr}_{B(-)}^{\pi_1(a, b) \equiv a}(\pi_2(a, b)) \equiv b:B(a)}$$

• Uniqueness rules for negative dependent sum types:

$$\frac{\Gamma \vdash z:\sum_{x:A} B(x)}{\Gamma \vdash z \equiv (\pi_1(z), \pi_2(z)):\sum_{x:A} B(x)}$$

• Computation rules for identity types:

$$\frac{\Gamma, a:A, b:A, p:a =_A b \vdash C(a, b, p) \; \mathrm{type} \quad \Gamma \vdash t:\prod_{c:A} C(c, c, \mathrm{refl}_A(c))}{\Gamma, c:A \vdash J(t, c, c, \mathrm{refl}(c)) \equiv t:C(c, c, \mathrm{refl}_A(c))}$$

Judgmental equality of types

In dependent type theory with a separate type judgment, judgmental equality of types is given by the following judgment:

• $\Gamma \vdash A \equiv A' \; \mathrm{type}$ - $A$ and $A'$ are judgmentally equal well-typed types in context $\Gamma$.

Inference rules

The variable conversion rule for judgmentally equal types:

$$\frac{\Gamma \vdash A \equiv B \; \mathrm{type} \quad \Gamma, x:A, \Delta \vdash \mathcal{J}}{\Gamma, x:B, \Delta \vdash \mathcal{J}}$$

In addition to the variable conversion rule, there are reflexivity, symmetry, and transitivity rules making judgmental equality for types an equivalence relation:

• Reflexivity of judgmental equality

$$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash A \equiv A \; \mathrm{type}}$$

• Symmetry of judgmental equality

  $$\frac{\Gamma \vdash A \equiv B \; \mathrm{type}}{\Gamma \vdash B \equiv A \; \mathrm{type}}$$

• Transitivity of judgmental equality

  $$\frac{\Gamma \vdash A \equiv B \; \mathrm{type} \quad \Gamma \vdash B \equiv C \; \mathrm{type} }{\Gamma \vdash A \equiv C \; \mathrm{type}}$$

Congruence rules for judgmental equality of types

In addition, judgmental equalities have congruence rules for every type in the type theory.

• Congruence rules for dependent function types

$$\frac{ \begin{array}{c} \Gamma \vdash A \equiv A' \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \equiv B'(x) \; \mathrm{type} \end{array} }{\Gamma \vdash \prod_{x:A} B(x) \equiv \prod_{x:A'} B'(x)\; \mathrm{type}}$$

$$\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash b(x):B(x) \quad \Gamma, x:A \vdash b'(x):B(x) \\ \Gamma, x:A \vdash b(x) \equiv b'(x):B(x) \end{array} }{\Gamma \vdash \lambda x:A.b(x) \equiv \lambda x:A.b'(x):\prod_{x:A}.B(x)}$$

$$\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash f:\prod_{x:A} B(x) \quad f':\prod_{x:A} B(x) \\ \Gamma \vdash f \equiv f':\prod_{x:A} B(x) \end{array} }{\Gamma, x:A \vdash f(x) \equiv f'(x):B(x)}$$

$$\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash b(x):B(x) \quad \Gamma, x:A \vdash b'(x):B(x) \\ \Gamma, x:A \vdash b(x) \equiv b'(x):B(x) \end{array} }{\Gamma \vdash \beta_{\prod}^{A, B} x:A.b(x) \equiv \beta_{\prod}^{A, B} x:A.b'(x):\prod_{x:A} b(x) =_{B(x)} (\lambda x:A.b(x))(x)}$$

$$\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A \vdash B'(x) \; \mathrm{type} \\ \Gamma, x:A \vdash B(x) \equiv B'(x) \; \mathrm{type} \end{array} }{\Gamma \vdash \eta_{\prod}^{A, B} \equiv \eta_{\prod}^{A, B'}:\prod_{f:\prod_{x:A} B(x)} f =_{\prod_{x:A} B(x)} \lambda x:A.f(x)}$$

• Congruence rules for dependent pair types:

$$\frac{ \begin{array}{c} \Gamma \vdash A \equiv A' \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \equiv B'(x) \; \mathrm{type} \end{array} }{\Gamma \vdash \sum_{x:A} B(x) \equiv \sum_{x:A'} B'(x)\; \mathrm{type}}$$

$$\frac{ \begin{array}{c} \Gamma \vdash A \equiv A' \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \equiv B'(x) \; \mathrm{type} \end{array} }{\Gamma, x:A, y:B(x) \vdash \mathrm{pair}_{\sum}^{A, B} \equiv \mathrm{pair}_{\sum}^{A', B'}:\sum_{x:A} B(x)}$$

$$\frac{ \begin{array}{c} \Gamma \vdash A \equiv A' \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \equiv B'(x) \; \mathrm{type} \quad \Gamma, z:\sum_{x:A} B(x) \vdash C(z) \equiv C'(z) \; \mathrm{type} \end{array} }{\Gamma \vdash \mathrm{ind}_{\sum}^{A, B, C} \equiv \mathrm{ind}_{\sum}^{A', B', C'}:\prod_{g:\prod_{x:A} \prod_{y:B(x)} C(\mathrm{pair}_{\sum}^{A, B}(x, y))} \prod_{z:\sum_{x:A} B(x)} C(z)}$$

$$\frac{ \begin{array}{c} \Gamma \vdash A \equiv A' \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \equiv B'(x) \; \mathrm{type} \quad \Gamma, z:\sum_{x:A} B(x) \vdash C(z) \equiv C'(z) \; \mathrm{type} \end{array} }{\Gamma \vdash \beta_{\sum}^{A, B, C} \equiv \beta_{\sum}^{A', B', C'}:\prod_{g:\prod_{x:A} \prod_{y:B(x)} C(\mathrm{pair}_{\sum}^{A, B}(x, y))} \prod_{x:A} \prod_{y:B(x)} \mathrm{ind}_{\sum}^{A, B, C}(g, \mathrm{pair}_{\sum}^{A, B}(x, y)) =_{C(\mathrm{pair}_{\sum}^{A, B}(x, y))} g(x, y)}$$

• Congruence rules for identity types:

$$\frac{\Gamma \vdash A \equiv A' \; \mathrm{type}}{\Gamma, x:A, y:A \vdash x =_A y \equiv x =_{A'} y}$$

$$\frac{\Gamma \vdash A \equiv A' \; \mathrm{type}}{\Gamma \vdash \mathrm{refl}_A \equiv \mathrm{refl}_{A'}:\prod_{x:A} x =_A x}$$

$$\frac{ \begin{array}{c} \Gamma \vdash A \equiv A' \; \mathrm{type} \quad \Gamma, x:A, y:A, p:x =_A y \vdash C(x, y, p) \equiv C'(x, y, p) \; \mathrm{type} \end{array} }{\Gamma \vdash \mathrm{ind}_{=}^{A, C} \equiv \mathrm{ind}_{=}^{A', C'}:\prod_{t:\prod_{x:A} C(x, x, \mathrm{refl}_A(x))} \prod_{x:A} \prod_{y:A} \prod_{p:x =_A y} C(x, y, p)}$$

$$\frac{ \begin{array}{c} \Gamma \vdash A \equiv A' \; \mathrm{type} \quad \Gamma, x:A, y:A, p:x =_A y \vdash C(x, y, p) \equiv C'(x, y, p) \; \mathrm{type} \end{array} }{\Gamma \vdash \beta_{ \mathrm{ind}_=}^{A, C} \equiv \beta_{\mathrm{ind}_=}^{A', C'}:\prod_{t:\prod_{x:A} C(x, x, \mathrm{refl}_A(x))} \prod_{x:A} \mathrm{ind}_{=}^{A, C}(t, x, x, \mathrm{refl}_A(x)) =_{C(x, x, \mathrm{refl}_A(x))} t(x)}$$

• Congruence rules for the empty type:

$$\frac{\Gamma, x:\emptyset \vdash C(x) \equiv C'(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{ind}_\emptyset^C \equiv \mathrm{ind}_\emptyset^{C'}:\prod_{x:\emptyset} C(x) \; \mathrm{type}}$$

• Congruence rules for the type of booleans:

$$\frac{\Gamma, x:\mathbb{2} \vdash C(x) \equiv C'(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{ind}_\mathbb{2}^C \equiv \mathrm{ind}_\mathbb{2}^{C'}:\prod_{a:C(0)} \prod_{b:C(1)} \prod_{x:\mathbb{2}} C(x)}$$

$$\frac{\Gamma, x:\mathbb{2} \vdash C(x) \equiv C'(x) \; \mathrm{type}}{\Gamma \vdash \beta_\mathbb{2}^{0, C} \equiv \beta_\mathbb{2}^{0, C'}:\prod_{a:C(0)} \prod_{b:C(1)} \mathrm{ind}_\mathbb{2}^C(a, b, 0) =_{C(0)} a}$$

$$\frac{\Gamma, x:\mathbb{2} \vdash C(x) \equiv C'(x) \; \mathrm{type}}{\Gamma \vdash \beta_\mathbb{2}^{1, C} \equiv \beta_\mathbb{2}^{1, C'}:\prod_{a:C(0)} \prod_{b:C(1)} \mathrm{ind}_\mathbb{2}^C(a, b, 1) =_{C(1)} b}$$

• Congruence rules for the natural numbers type:

$$\frac{\Gamma, x:\mathbb{N} \vdash C(x) \equiv C'(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{ind}_\mathbb{N}^C \equiv \mathrm{ind}_\mathbb{N}^{C'}:\prod_{c_0:C(0)} \prod_{c_s:\prod_{x:\mathbb{N}} C(x) \to C(s(x))} \prod_{x:\mathbb{N} C(x)}}$$

$$\frac{\Gamma, x:\mathbb{N} \vdash C(x) \equiv C'(x) \; \mathrm{type}}{\Gamma \vdash \beta_\mathbb{N}^{0, C} \equiv \beta_\mathbb{N}^{0, C'}:\prod_{c_0:C(0)} \prod_{c_s:\prod_{x:\mathbb{N}} C(x) \to C(s(x))} \mathrm{ind}_\mathbb{N}^C(c_0, c_s, 0) =_{C(0)} c_0}$$

$$\frac{\Gamma, x:\mathbb{N} \vdash C(x) \equiv C'(x) \; \mathrm{type}}{\Gamma \vdash \beta_\mathbb{N}^{s, C} \equiv \beta_\mathbb{N}^{s, C'}:\prod_{c_0:C(0)} \prod_{c_s:\prod_{x:\mathbb{N}} C(x) \to C(s(x))} \prod_{x:\mathbb{N}} \mathrm{ind}_\mathbb{N}^C(c_0, c_s, s(x)) =_{C(s(x))} c_s(x)(\mathrm{ind}_\mathbb{N}^C(c_0, c_s, x))}$$

Similarly, we have congruence rules for every axiom in the dependent type theory, such as

• congruence rule for function extensionality:

$$\frac{\Gamma \vdash A \equiv A' \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \equiv B'(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{funext}_{A, B} \equiv \mathrm{funext}_{A', B'}:\prod_{f;\prod_{x:A} B(x)} \prod_{g:\prod_{x:A} B(x)} (f =_{\prod_{x:A} B(x)} g) \simeq \prod_{x:A} f(x) =_{B(x)} g(x)}$$

• congruence rule for the axiom of choice:

$$\frac{\Gamma \vdash A \equiv A' \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \equiv B'(x) \; \mathrm{type} \quad \Gamma, x:A, y:B(x) \vdash C(x, y) \equiv C'(x, y) \; \mathrm{type}}{\Gamma \vdash \mathrm{choice}_{A, B, C} \equiv \mathrm{choice}_{A', B', C'}:\left(\mathrm{isSet}(A) \times \prod_{x:A} \mathrm{isSet}(B(x))\right) \to \forall x:A.\exists y:B(x).C(x, y) \to \exists g:\prod_{x:A} B(x).\forall x:A.C(x, g(x))}$$

Judgmental equality of contexts

In some dependent type theories, there is also judgmental equality of contexts, which is given by the following judgment:

• $\Gamma \equiv \Gamma' \; \mathrm{ctx}$ - $\Gamma$ and $\Gamma'$ are judgmentally equal contexts.

There are reflexivity, symmetry, and transitivity rules making judgmental equality for contexts an equivalence relation:

• Reflexivity of judgmental equality

$$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \equiv \Gamma \; \mathrm{ctx}}$$

• Symmetry of judgmental equality

  $$\frac{\Gamma \equiv \Delta \; \mathrm{ctx}}{\Delta \equiv \Gamma \; \mathrm{ctx}}$$

• Transitivity of judgmental equality

  $$\frac{\Gamma \equiv \Delta \; \mathrm{ctx} \quad \Delta \equiv \Xi \; \mathrm{ctx}}{\Gamma \equiv \Xi \; \mathrm{ctx}}$$

 History

The notion of judgmental or definitional equality was introduced first in AUTOMATH. The following paper presents a suggestive explanation of this notion and how proof-checking was designed in this system (especially section 10):

On the roles of types in mathematics

The notion of judgmental or definitional equality was later introduced by Per Martin-Löf, first in the context of normalization proofs for higher-order logic in the paper Hauptsatz for Intuitionistic Simple Type Theory and generalized in Type Theory. He discusses this notion in the paper About Models for Intuitionistic Type Theory and The notion of Definitional Equality.

The extension from AUTOMATH is that one adds the notion of data type (natural number), of constructors (zero and successor) and primitive recursion as definitional equality. The motivation is that one can consider the schema of primitive recursion as a definition of a function.

This was also influenced by natural deduction, where constructors correspond to introduction rules and the work of Gödel on system T.

With this extension, one obtains a programming language with dependent types and where computations correspond to unfolding of definitions (that can be primitive recursive definitions). This programming language has the feature that all computations terminate. This has been also considered in functional programming, see e.g. the discussion in this paper.

A description of the evaluation algorithm using techniques from functional programming can be found in this work of Gregoire and Leroy.

See also

• equality, equality in type theory

• propositional equality, typal equality

• coercion

References

• Robin Adams, Pure type systems with judgemental equality, Journal of Functional Programming, Volume 16 Issue 2(2006) (web)

• Vincent Siles, Hugo Herbelin, Equality is typable in semi-full pure type systems (pdf)

• Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (pdf) (478 pages)

The first paper to mention intensional equality (and the fact that it should be decidable) may be:

• Kurt Gödel, Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica (1958), pp. 280–287,

The distinction between definitional equality and “book” equality:

• Nicolaas de Bruijn, Automath,

The notion of definitional equality in the context of (dependent) type theory:

• Simon Thompson, §5.2.1 in: Type Theory and Functional Programming, Addison-Wesley (1991) [ISBN:0-201-41667-0, webpage, pdf]

specifically in the Coq proof assistant:

• Adam Chlipala, §10.1 in: Certified programming with dependent types, MIT Press 2013 [ISBN:9780262026659, pdf, book webpage]