nLab
judgmental equality
Context
Type theory
Equality and Equivalence
equivalence
equality (definitional , propositional , computational , judgemental , extensional , intensional , decidable )
identity type , equivalence in homotopy type theory
isomorphism , weak equivalence , homotopy equivalence , weak homotopy equivalence , equivalence in an (∞,1)-category
natural equivalence , natural isomorphism
gauge equivalence
Examples.
principle of equivalence
equation
fiber product , pullback
homotopy pullback
Examples.
linear equation , differential equation , ordinary differential equation , critical locus
Euler-Lagrange equation , Einstein equation , wave equation
Schrödinger equation , Knizhnik-Zamolodchikov equation , Maurer-Cartan equation , quantum master equation , Euler-Arnold equation , Fuchsian equation , Fokker-Planck equation , Lax equation
Contents
Idea
In any type theory , judgmental equality is the notion of equality which is defined to be a judgment . Judgmental equality is most commonly used in single-level type theories like Martin-Löf type theory or higher observational type theory for making inductive definitions , but it is also used 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.
Judgmental equality can be contrasted with propositional equality , where equality is a proposition , and typal equality , where equality is a type .
Judgments
In the model of dependent type theory which uses judgmental equality for definitional equality , judgmental equality of types, terms, and contexts are given by the following judgments :
Γ ⊢ A ≡ A ′ type \Gamma \vdash A \equiv A' \; \mathrm{type} - A A and A ′ A' are judgementally equal well-typed types in context Γ \Gamma .
Γ ⊢ a ≡ a ′ : A \Gamma \vdash a \equiv a' : A - a a and a ′ a' are judgementally equal well-typed terms of type A A in context Γ \Gamma .
Γ ≡ Γ ′ ctx \Gamma \equiv \Gamma' \; \mathrm{ctx} - Γ \Gamma and Γ ′ \Gamma' are judgementally equal contexts.
Structural rules
Judgmental equality has its own structural rules: reflexivity, symmetry, transitivity, the principle of substitution, and the variable conversion rule.
Reflexivity of judgmental equality
Γ ⊢ A type Γ ⊢ A ≡ A type \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash A \equiv A \; \mathrm{type}} Γ ⊢ A type Γ ⊢ a : A Γ ⊢ a ≡ a : A \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A}{\Gamma \vdash a \equiv a:A} Γ ctx Γ ≡ Γ ctx \frac{\Gamma \; \mathrm{ctx}}{\Gamma \equiv \Gamma \; \mathrm{ctx}}
Symmetry of judgmental equality
Γ ⊢ A ≡ B type Γ ⊢ B ≡ A type \frac{\Gamma \vdash A \equiv B \; \mathrm{type}}{\Gamma \vdash B \equiv A \; \mathrm{type}} Γ ⊢ A type Γ ⊢ a ≡ b : A Γ ⊢ b ≡ a : A \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a \equiv b:A}{\Gamma \vdash b \equiv a:A} Γ ≡ Δ ctx Δ ≡ Γ ctx \frac{\Gamma \equiv \Delta \; \mathrm{ctx}}{\Delta \equiv \Gamma \; \mathrm{ctx}}
Transitivity of judgmental equality
Γ ⊢ A ≡ B type Γ ⊢ B ≡ C type Γ ⊢ A ≡ C type \frac{\Gamma \vdash A \equiv B \; \mathrm{type} \quad \Gamma \vdash B \equiv C \; \mathrm{type} }{\Gamma \vdash A \equiv C \; \mathrm{type}} Γ ⊢ A type Γ ⊢ a ≡ b : A b ≡ c : A Γ ⊢ a ≡ c : A \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a \equiv b:A \quad b \equiv c:A }{\Gamma \vdash a \equiv c:A} Γ ≡ Δ ctx Δ ≡ Ξ ctx Γ ≡ Ξ ctx \frac{\Gamma \equiv \Delta \; \mathrm{ctx} \quad \Delta \equiv \Xi \; \mathrm{ctx}}{\Gamma \equiv \Xi \; \mathrm{ctx}}
Principle of substitution for judgmentally equal terms:
Γ ⊢ A type Γ ⊢ a ≡ b : A Γ , x : A , Δ ⊢ B type Γ , Δ [ b / x ] ⊢ B [ a / x ] ≡ B [ b / x ] type \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a \equiv b : A \quad \Gamma, x:A, \Delta \vdash B \; \mathrm{type}}{\Gamma, \Delta[b/x] \vdash B[a/x] \equiv B[b/x] \; \mathrm{type}} Γ ⊢ A type Γ ⊢ a ≡ b : A Γ , x : A , Δ ⊢ c : B Γ , Δ [ b / x ] ⊢ c [ a / x ] ≡ c [ b / x ] : B [ b / x ] \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a \equiv b : A \quad \Gamma, x:A, \Delta \vdash c:B}{\Gamma, \Delta[b/x] \vdash c[a/x] \equiv c[b/x]: B[b/x]}
The variable conversion rule for judgmentally equal types:
Γ ⊢ A ≡ B type Γ , x : A , Δ ⊢ 𝒥 Γ , x : B , Δ ⊢ 𝒥 \frac{\Gamma \vdash A \equiv B \; \mathrm{type} \quad \Gamma, x:A, \Delta \vdash \mathcal{J}}{\Gamma, x:B, \Delta \vdash \mathcal{J}}
The context conversion rule for judgmentally equal contexts
Γ ⊢ 𝒥 Γ ≡ Δ ctx Δ ⊢ 𝒥 \frac{\Gamma \vdash \mathcal{J} \quad \Gamma \equiv \Delta \; \mathrm{ctx}}{\Delta \vdash \mathcal{J}}
In addition, if the dependent type theory has type definition judgments B ≔ A type B \coloneqq A \; \mathrm{type} term definition judgments b ≔ a : A b \coloneqq a:A , and context definition judgments Δ ≔ Γ ctx \Delta \coloneqq \Gamma \; \mathrm{ctx} then judgmental equality is used in the following rules:
Formation and judgmental equality reflection rules for type definition:
Γ ⊢ B ≔ A type Γ ⊢ B type Γ ⊢ B ≔ A type Γ ⊢ B ≡ A type \frac{\Gamma \vdash B \coloneqq A \; \mathrm{type}}{\Gamma \vdash B \; \mathrm{type}} \qquad \frac{\Gamma \vdash B \coloneqq A \; \mathrm{type}}{\Gamma \vdash B \equiv A\; \mathrm{type}}
Introduction and judgmental equality reflection rules for term definition:
Γ ⊢ b ≔ a : A Γ ⊢ b : A Γ ⊢ b ≔ a : A Γ ⊢ b ≡ a : A \frac{\Gamma \vdash b \coloneqq a:A}{\Gamma \vdash b:A} \qquad \frac{\Gamma \vdash b \coloneqq a:A}{\Gamma \vdash b \equiv a:A}
Formation and judgmental equality reflection rules for context definition:
Δ ≔ Γ ctx Δ ctx Δ ≔ Γ ctx Δ ≡ Γ ctx \frac{\Delta \coloneqq \Gamma \; \mathrm{ctx}}{\Delta \; \mathrm{ctx}} \qquad \frac{\Delta \coloneqq \Gamma \; \mathrm{ctx}}{\Delta \equiv \Gamma \; \mathrm{ctx}}
In computation and uniqueness rules
Judgmental equality can be used in the computation rules and uniqueness rules of types:
Computation rules for dependent product types:
Γ , x : A ⊢ b ( x ) : B ( x ) Γ ⊢ a : A Γ ⊢ λ ( x : A ) . b ( x ) ( a ) ≡ b [ a / x ] : B [ a / x ] \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/x]:B[a/x]}
Uniqueness rules for dependent product types:
Γ ⊢ f : ∏ x : A B ( x ) Γ ⊢ f ≡ λ ( x ) . f ( x ) : ∏ x : A B ( x ) \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 dependent sum types:
Γ , x : A ⊢ b ( x ) : B ( x ) Γ ⊢ a : A Γ ⊢ π 1 ( a , b ) ≡ a : A Γ , x : A ⊢ b : B Γ ⊢ a : A Γ ⊢ π 2 ( a , b ) ≡ b : B ( π 1 ( a , b ) ) \frac{\Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash \pi_1(a, b) \equiv a:A} \qquad \frac{\Gamma, x:A \vdash b:B \quad \Gamma \vdash a:A}{\Gamma \vdash \pi_2(a, b) \equiv b:B(\pi_1(a, b))}
Uniqueness rules for dependent sum types:
Γ ⊢ z : ∑ x : A B ( x ) Γ ⊢ z ≡ ( π 1 ( z ) , π 2 ( z ) ) : ∑ x : A B ( x ) \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:Γ , a : A , b : A , p : a = A b ⊢ C type Γ , c : A ⊢ t : C [ c / a , c / b , refl A ( c ) / p ] Γ , c : A ⊢ J ( t , c , c , refl ( c ) ) ≡ t : C [ c / a , c / b , refl A ( c ) / p ] \frac{\Gamma, a:A, b:A, p:a =_A b \vdash C \; \mathrm{type} \quad \Gamma, c:A \vdash t:C[c/a, c/b, \mathrm{refl}_A(c)/p]}{\Gamma, c:A \vdash J(t, c, c, \mathrm{refl}(c)) \equiv t:C[c/a, c/b, \mathrm{refl}_A(c)/p]}
See also
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)
Last revised on December 1, 2022 at 03:38:56.
See the history of this page for a list of all contributions to it.