judgmental equality in nLab

> 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]]. 

----

+-- {: .rightHandSide}
+-- {: .toc .clickDown tabindex="0"}
### Context
#### Type theory
+-- {: .hide}
[[!include type theory - contents]]
=--
#### Equality and Equivalence
+--{: .hide}
[[!include equality and equivalence - contents]]
=--
=--
=--

\tableofcontents

## 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](#PML):

> 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)-category theory|(infinity,1)-categorical]] types which could not be coherently defined in vanilla dependent type theory. 

\begin{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. 
\end{remark}

\begin{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]]:

{#ShorthandTypalEquality} 
$$\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.
\end{remark}

\begin{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.
\end{remark}

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 [[infinity-groupoid|$\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 [[equivalence of types|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 [[judgmental equality#ShorthandTypalEquality|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 [[judgmental equality#ShorthandTypalEquality|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](http://uf-ias-2012.wikispaces.com/file/view/deB1.pdf/401388596/deB1.pdf)

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](http://www.sciencedirect.com/science/article/pii/S0049237X09703659) and generalized in Type Theory. He discusses this notion in the paper [About Models for Intuitionistic Type Theory and The notion of Definitional Equality](http://www.sciencedirect.com/science/article/pii/S0049237X08707274).

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](http://uf-ias-2012.wikispaces.com/file/view/turner.pdf/401400700/turner.pdf).

A description of the evaluation algorithm using techniques from functional programming
can be found in [this work of Gregoire and Leroy](http://uf-ias-2012.wikispaces.com/file/view/strong-reduction.pdf/402005168/strong-reduction.pdf). 

## 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](http://dl.acm.org/citation.cfm?id=1114675))

* Vincent Siles, Hugo Herbelin, _Equality is typable in semi-full pure type systems_ ([pdf](http://pauillac.inria.fr/~herbelin/publis/lics-SilHer10-pts-typed-conv.pdf))

* [[Egbert Rijke]], *[[Introduction to Homotopy Type Theory]]*, Cambridge Studies in Advanced Mathematics, Cambridge University Press ([pdf](https://raw.githubusercontent.com/martinescardo/HoTTEST-Summer-School/main/HoTT/hott-intro.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|dependent]]) [[type theory]]:

* {#Thompson91} [[Simon Thompson]], §5.2.1 in: *[[Type Theory and Functional Programming]]*, Addison-Wesley (1991) &lbrack;ISBN:0-201-41667-0, [webpage](http://www.cs.kent.ac.uk/people/staff/sjt/TTFP), [pdf](http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf)&rbrack;

specifically in the [[Coq]] [[proof assistant]]: 

* [[Adam Chlipala]], §10.1 in: _Certified programming with dependent types_, MIT Press 2013 &lbrack;[ISBN:9780262026659 ](https://mitpress.mit.edu/books/certified-programming-dependent-types), [pdf](http://adam.chlipala.net/cpdt/cpdt.pdf),  [book webpage](http://adam.chlipala.net/cpdt/)&rbrack;

[[!redirects judgmental equality]]
[[!redirects judgmental equalities]]

[[!redirects judgemental equality]]
[[!redirects judgemental equalities]]

[[!redirects judgmental equality of terms]]
[[!redirects judgmental equalities of terms]]

[[!redirects judgemental equality of terms]]
[[!redirects judgemental equalities of terms]]

[[!redirects judgmental equality of elements]]
[[!redirects judgmental equalities of elements]]

[[!redirects judgemental equality of elements]]
[[!redirects judgemental equalities of elements]]

[[!redirects judgmental equality of types]]
[[!redirects judgmental equalities of types]]

[[!redirects judgemental equality of types]]
[[!redirects judgemental equalities of types]]

[[!redirects judgmentally equal]]
[[!redirects judgmentally equal terms]]
[[!redirects judgmentally equal elements]]
[[!redirects judgmentally equal types]]

[[!redirects definitional equality]]
[[!redirects definitional equalities]]

[[!redirects explicit definitional equality]]
[[!redirects explicit definitional equalities]]

[[!redirects metatheoretic definitional equality]]
[[!redirects metatheoretic definitional equalities]]

[[!redirects meta-theoretic definitional equality]]
[[!redirects meta-theoretic definitional equalities]]