nLab
propositional 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 predicate logic over type theory , propositional equality is the notion of equality which is defined to be a proposition. Propositional equality is most commonly used in set theories like ZFC and ETCS , but it could also be used for definitional equality and conversional equality in some presentations of dependent type theories like Martin-Löf type theory or cubical type theory in place of judgmental equality .
Propositional equality can be contrasted with judgmental equality , where equality is a judgment , and typal equality , where equality is a type .
Note on terminology
Historically in the dependent type theory community, the term propositional equality was used for typal equality . This was because under the principle of propositions as types , one interprets all types in a single-layer type theory as being propositions. However, we choose to make a distinction between propositional equality and typal equality. First, propositional equality as defined in this article is used in the most common foundations of mathematics , such as ZFC and ETCS , and is clearly not a type. Additionally, in some logics over type theory , one can have three distinct notions of equality: judgmental equality , propositional equality , and typal equality . Finally, in the advent of homotopy type theory and other type theoretic higher foundations , typal equality is no longer required to be a subsingleton or h-proposition , and the alternative principle of propositions as some types has become the primary interpretation of dependent type theory , where only the subsingletons or h-propositions are interpreted as propositions .
Definition and structural rules
Propositional equality of types and terms is formed by the following rules:
Γ ⊢ A type Γ ⊢ B type Γ ⊢ A ≡ B prop \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \equiv B \; \mathrm{prop}} Γ ⊢ A type Γ ⊢ a : A Γ ⊢ b : A Γ ⊢ a ≡ A b prop \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A}{\Gamma \vdash a \equiv_A b \; \mathrm{prop}}
Propositional equality has its own structural rules: reflexivity, symmetry, transitivity, the principle of substitution, and the variable conversion rule.
Reflexivity of propositional equality
Γ ⊢ A type Γ ⊢ A ≡ A true \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash A \equiv A \; \mathrm{true}} Γ ⊢ A type Γ ⊢ a : A Γ ⊢ a ≡ A a true \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A}{\Gamma \vdash a \equiv_A a \; \mathrm{true}}
Symmetry of propositional equality
Γ ⊢ A type Γ ⊢ B type Γ ⊢ A ≡ B true Γ ⊢ B ≡ A true \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash A \equiv B \; \mathrm{true}}{\Gamma \vdash B \equiv A \; \mathrm{true}} Γ ⊢ A type Γ ⊢ a : A Γ ⊢ b : A Γ ⊢ a ≡ A b true Γ ⊢ b ≡ A a true \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash a \equiv_A b \; \mathrm{true}}{\Gamma \vdash b \equiv_A a \; \mathrm{true}}
Transitivity of propositional equality
Γ ⊢ A type Γ ⊢ B type Γ ⊢ C type Γ ⊢ A ≡ B true Γ ⊢ B ≡ C true Γ ⊢ A ≡ C true \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash A \equiv B \; \mathrm{true} \quad \Gamma \vdash B \equiv C \; \mathrm{true}}{\Gamma \vdash A \equiv C \; \mathrm{true}} Γ ⊢ A type Γ ⊢ a : A Γ ⊢ b : A Γ ⊢ c : A Γ ⊢ a ≡ A b true Γ ⊢ b ≡ A c true Γ ⊢ a ≡ A c true \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash c:A \quad \Gamma \vdash a \equiv_A b \; \mathrm{true} \quad \Gamma \vdash b \equiv_A c \; \mathrm{true}}{\Gamma \vdash a \equiv_A c \; \mathrm{true}}
Γ ⊢ A type Γ ⊢ B type Γ ⊢ A ≡ B true Γ , x : A , Δ ⊢ 𝒥 Γ , x : B , Δ ⊢ 𝒥 \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash A \equiv B \; \mathrm{true} \quad \Gamma, x:A, \Delta \vdash \mathcal{J}}{\Gamma, x:B, \Delta \vdash \mathcal{J}}
In addition, if the dependent type theory has type definition judgments B ≔ A type B \coloneqq A \; \mathrm{type} and term definition judgments b ≔ a : A b \coloneqq a:A , then propositional equality is used in the following rules:
In computation and uniqueness rules
Propositional equality can be used in the computation rules and uniqueness rules of types in dependent type theory :
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 ] true \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] \; \mathrm{true}}
Uniqueness rules for dependent product types:
Γ ⊢ f : ∏ x : A B ( x ) Γ ⊢ f ≡ ∏ x : A B ( x ) λ ( x ) . f ( x ) true \frac{\Gamma \vdash f:\prod_{x:A} B(x)}{\Gamma \vdash f \equiv_{\prod_{x:A} B(x)} \lambda(x).f(x) \; \mathrm{true}}
Computation rules for dependent sum types:
Γ , x : A ⊢ b ( x ) : B ( x ) Γ ⊢ a : A Γ ⊢ π 1 ( a , b ) ≡ A a true Γ , x : A ⊢ b : B Γ ⊢ a : A Γ ⊢ π 2 ( a , b ) ≡ B ( π 1 ( a , b ) ) b true \frac{\Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash \pi_1(a, b) \equiv_A a \; \mathrm{true}} \qquad \frac{\Gamma, x:A \vdash b:B \quad \Gamma \vdash a:A}{\Gamma \vdash \pi_2(a, b) \equiv_{B(\pi_1(a, b))} b \; \mathrm{true}}
Uniqueness rules for dependent sum types:
Γ ⊢ z : ∑ x : A B ( x ) Γ ⊢ z ≡ ∑ x : A B ( x ) ( π 1 ( z ) , π 2 ( z ) ) true \frac{\Gamma \vdash z:\sum_{x:A} B(x)}{\Gamma \vdash z \equiv_{\sum_{x:A} B(x)} (\pi_1(z), \pi_2(z)) \; \mathrm{true}}
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 ) ) ≡ C [ c / a , c / b , refl A ( c ) / p ] t true \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_{C[c/a, c/b, \mathrm{refl}_A(c)/p]} t \; \mathrm{true}}
See also
Last revised on December 16, 2022 at 16:17:52.
See the history of this page for a list of all contributions to it.