nLab propositional equality

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Equality and Equivalence

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

Typed first-order logic

In any two-layer type theory with a layer of types and a layer of propositions, or equivalently a first order logic over type theory or a first-order theory, every type AA has a binary relation according to which two elements xx and yy of AA are related if and only if they are equal; in this case we write x= Ayx =_A y. Since relations are propositions in the context of a term variable judgment in the type layer, this is called propositional equality. The formation and introduction rules for propositional equality is as follows

ΓAtypeΓ,x:A,y:Ax= AypropΓAtypeΓ,x:Ax= Axtrue\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A, y:A \vdash x =_A y \; \mathrm{prop}} \quad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A \vdash x =_A x \; \mathrm{true}}

Then we have the elimination rules for propositional equality:

ΓAtypeΓ,x:A,y:AP(x,y)propΓ(x:A.P(x,x))(x:A.y:A.x= AyP(x,y))true\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A, y:A \vdash P(x, y) \; \mathrm{prop}}{\Gamma \vdash \left(\forall x:A.P(x, x)\right) \implies \left(\forall x:A.\forall y:A.x =_A y \implies P(x, y)\right) \; \mathrm{true}}

Untyped first-order logic

Something similar occurs in untyped first-order logic, where the domain of discourse has a binary relation according to which two elements xx and yy are related if and only if they are equal; in this case we write x=yx = y. Since relations are propositions in the context of a term variable judgment in the type layer, this is similarly called propositional equality. The formation and introduction rules for propositional equality is as follows

ΓxΓyΓx=ypropΓxΓx=xtrue\frac{\Gamma \vdash x \quad \Gamma \vdash y}{\Gamma \vdash x = y \; \mathrm{prop}} \quad \frac{\Gamma \vdash x}{\Gamma \vdash x = x \; \mathrm{true}}

Then we have the elimination rules for propositional equality:

Γ,x,yP(x,y)propΓ(x.P(x,x))(x.y.x=yP(x,y))true\frac{\Gamma, x, y \vdash P(x, y) \; \mathrm{prop}}{\Gamma \vdash \left(\forall x.P(x, x)\right) \implies \left(\forall x.\forall y.x = y \implies P(x, y)\right) \; \mathrm{true}}

Properties

Propositional equality is an equivalence relation

The introduction rule of propositional equality says that propositional equality is reflexive.

We can show that heterogeneous equality is symmetric, that for all x:Ax:A and y:Ay:A such that x= Ayx =_A y, we have y= Axy =_A x. By the introduction rule, we have that for all x:Ax:A, we have that x= Axx =_A x, and because all propositions imply themselves, we have that x= Axx =_A x implies x= Axx =_A x. Thus, by the elimination rules for heterogeneous equality, for all x:Ax:A and y:Ay:A such that x= Ayx =_A y, we have y= Axy =_A x.

We can also show that heterogeneous equality is transitive, that for all x:Ax:A, y:Ay:A, and z:Az:A such that x= Ayx =_A y, y= Azy =_A z implies that x= Azx =_A z. By the introduction rule, we have that for all x:Ax:A and a:B(x)a:B(x), we have that x= Axx =_A x, and because all propositions imply themselves, we have that x= Azx =_A z implies y= Azy =_A z, and because true propositions imply true propositions, we have that x= Axx =_A x implies that x= Azx =_A z implies x= Azx =_A z. Thus, by the elimination rules for heterogeneous equality, for all x:Ax:A, y:Ay:A, and z:Az:A such that x= Ayx =_A y, y= Azy =_A z implies that x= Azx =_A z.

Thus, heterogeneous equality is an equivalence relation.

Functions are extensional

For all function f:ABf:A \to B and elements x:Ax:A and y:Ay:A such that x= Ayx =_A y, f(x)= Bf(y)f(x) =_{B} f(y):

f:AB.x:A.y:A.x= Ayf(x)= Bf(y)\forall f:A \to B.\forall x:A.\forall y:A.x =_A y \implies f(x) =_{B} f(y)

This is because for all functions f:ABf:A \to B, by the introduction rule for propositional equality, for all elements x:Ax:A, f(x)= Bf(x)f(x) =_{B} f(x), and the elimination rule for propositional equality states that if for all elements x:Ax:A, f(x)= Bf(x)f(x) =_{B} f(x), then for all elements x:Ax:A and y:Ay:A such that x= Ayx =_A y, f(x)= Bf(y)f(x) =_{B} f(y).

Function extensionality

The extensionality principle for function types (function extensionality) states that for all functions f:ABf:A \to B and g:ABg:A \to B, f= ABgf =_{A \to B} g if and only if for all a:Aa:A and b:Ab:A such that a= Aba =_A b, f(a)= Bg(b)f(a) =_{B} g(b)

f:AB.g:AB.f= ABga:A.b:A.a= Ab(f(a)= Bg(b))\forall f:A \to B.\forall g:A \to B.f =_{A \to B} g \iff \forall a:A. \forall b:A.a =_A b \implies (f(a) =_{B} g(b))

Relation to heterogeneous propositional equality

Given elements x:Ax:A and y:Ay:A such that x= Ayx =_A y and a:B(x)a:B(x) and b:B(y)b:B(y), heterogeneous propositional equality is given by the relation a= ̲.B x= Ayba =_{\underline{ }.B}^{x =_A y} b. Given elements x:Ax:A, and for all a:B(x)a:B(x) and b:B(x)b:B(x), a= ̲.B x= Axba =_{\underline{ }.B}^{x =_A x} b if and only if a= B(x)ba =_{B(x)} b

a:B(x).b:B(x).a= ̲.B x= Axba= B(x)b\forall a:B(x).\forall b:B(x). a =_{\underline{ }.B}^{x =_A x} b \iff a =_{B(x)} b

This is because by the introduction rules of propositional equality and heterogeneous propositional equality, we have that for all a:B(x)a:B(x), a= B(x)aa =_{B(x)} a and a= ̲.B x= Axaa =_{\underline{ }.B}^{x =_A x} a, and since true propositions imply true propositions, we have a= B(x)aa =_{B(x)} a implies a= ̲.B x= Axaa =_{\underline{ }.B}^{x =_A x} a and a= ̲.B x= Axaa =_{\underline{ }.B}^{x =_A x} a implies a= B(x)aa =_{B(x)} a. By the elimination rules for propositional equality, for all a:B(x)a:B(x) and b:B(x)b:B(x), we have a= B(x)ba =_{B(x)} b implies a= ̲.B x= Axba =_{\underline{ }.B}^{x =_A x} b, and by the elimination rules for heterogeneous propositional equality, we have a= ̲.B x= Axba =_{\underline{ }.B}^{x =_A x} b implies a= B(x)ba =_{B(x)} b. Thus, a= ̲.B x= Axba =_{\underline{ }.B}^{x =_A x} b if and only if a= B(x)ba =_{B(x)} b.

Transport and the principle of substitution

The analogue of identity functions on a type AA, a function f:AAf:A \to A such that x= Af(x)x =_A f(x) for all elements x:Ax:A, is the notion of transport functions between a family of types B(x)B(x) indexed by elements x:Ax:A.

Given elements x:Ax:A and y:Ay:A such that x= Ayx =_A y, a transport function is a function f:B(x)B(y)f:B(x) \to B(y) such that for all a:B(x)a:B(x), a= ̲.B x= Ayf(a)a =_{\underline{ }.B}^{x =_A y} f(a)

a:B(x).a= ̲.B x= Ayf(a)\forall a:B(x).a =_{\underline{ }.B}^{x =_A y} f(a)

These transport functions, if they exist, are unique up to equality. Suppose we have a second function g:B(x)B(y)g:B(x) \to B(y) such that x= Ayx =_A y implies that for all a:B(x)a:B(x), a= ̲.B x= Ayg(a)a =_{\underline{ }.B}^{x =_A y} g(a). Then by symmetry and transitivity of heterogeneous equality, we have f(a)= ̲.B y= Ayg(a)f(a) =_{\underline{ }.B}^{y =_A y} g(a), which is logically equivalent to f(a)= B(y)g(a)f(a) =_{B(y)} g(a). Then by function extensionality, we have f= B(x)B(y)gf =_{B(x) \to B(y)} g, which implies that transport functions, if they exist, are unique up to equality.

Suppose that for all elements x:Ax:A and y:Ay:A such that x= Ayx =_A y, there exists a transport function tr ̲.B x= Ay:B(x)B(y)\mathrm{tr}_{\underline{ }.B}^{x =_A y}:B(x) \to B(y). Then for all a:B(x)a:B(x) and b:B(y)b:B(y), a= ̲.B x= Ayba =_{\underline{ }.B}^{x =_A y} b if and only if tr ̲.B x= Ay(a)= B(y)b\mathrm{tr}_{\underline{ }.B}^{x =_A y}(a) =_{B(y)} b

a:B(x).b:B(y).a= ̲.B x= Aybtr ̲.B x= Ay(a)= B(y)b\forall a:B(x).\forall b:B(y). a =_{\underline{ }.B}^{x =_A y} b \iff \mathrm{tr}_{\underline{ }.B}^{x =_A y}(a) =_{B(y)} b

In particular, this means that we have tr ̲.B y= Ax(b)= B(x)a\mathrm{tr}_{\underline{ }.B}^{y =_A x}(b) =_{B(x)} a, and by the fact that functions preserve equality, tr ̲.B y= Ax(tr ̲.B x= Ay(a))= B(x)tr ̲.B y= Ax(b)\mathrm{tr}_{\underline{ }.B}^{y =_A x}(\mathrm{tr}_{\underline{ }.B}^{x =_A y}(a)) =_{B(x)} \mathrm{tr}_{\underline{ }.B}^{y =_A x}(b), which by transitivity of propositional equality implies that tr ̲.B y= Ax(tr ̲.B x= Ay(a))= B(x)a\mathrm{tr}_{\underline{ }.B}^{y =_A x}(\mathrm{tr}_{\underline{ }.B}^{x =_A y}(a)) =_{B(x)} a. Similarly, we have tr ̲.B x= Ay(tr ̲.B y= Ax(b))= B(y)tr ̲.B x= Ay(a)\mathrm{tr}_{\underline{ }.B}^{x =_A y}(\mathrm{tr}_{\underline{ }.B}^{y =_A x}(b)) =_{B(y)} \mathrm{tr}_{\underline{ }.B}^{x =_A y}(a), which by transitivity of propositional equality implies that tr ̲.B x= Ay(tr ̲.B y= Ax(b))= B(y)b\mathrm{tr}_{\underline{ }.B}^{x =_A y}(\mathrm{tr}_{\underline{ }.B}^{y =_A x}(b)) =_{B(y)} b. Thus, the transport functions tr ̲.B x= Ay:B(x)B(y)\mathrm{tr}_{\underline{ }.B}^{x =_A y}:B(x) \to B(y) and tr ̲.B y= Ax:B(y)B(x)\mathrm{tr}_{\underline{ }.B}^{y =_A x}:B(y) \to B(x) are inverse functions of each other, and thus both transport functions are bijections, and could be written as tr ̲.B x= Ay:B(x)B(y)\mathrm{tr}_{\underline{ }.B}^{x =_A y}:B(x) \cong B(y) and tr ̲.B y= Ax:B(y)B(x)\mathrm{tr}_{\underline{ }.B}^{y =_A x}:B(y) \cong B(x) respectively.

Thus, provided that transport functions exist, we have the following derivable rules for the principle of substitution of propositionally equal terms:

ΓAtypeΓa:AΓb:AΓa= AbtrueΓ,x:AB(x)typeΓtr ̲.B a= Ab:B(a)B(b)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a : A \quad \Gamma \vdash b : A \quad \Gamma \vdash a =_A b \; \mathrm{true} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{tr}_{\underline{ }.B}^{a =_A b}:B(a) \to B(b)}
ΓAtypeΓa:AΓb:AΓa= AbtrueΓ,x:Ac(x):B(x)Γtr ̲.B a= Ab(c(a))= B(b)c(b)true\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a : A \quad \Gamma \vdash b : A \quad \Gamma \vdash a =_A b \; \mathrm{true} \quad \Gamma, x:A \vdash c(x):B(x)}{\Gamma \vdash \mathrm{tr}_{\underline{ }.B}^{a =_A b}(c(a)) =_{B(b)} c(b) \; \mathrm{true}}

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:Ab(x):B(x)Γa:AΓλ(x:A).b(x)(a)= B(a)b(a)true\frac{\Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash \lambda(x:A).b(x)(a) =_{B(a)} b(a) \; \mathrm{true}}
  • Uniqueness rules for dependent product types:
Γf: x:AB(x)Γf= x:AB(x)λ(x).f(x)true\frac{\Gamma \vdash f:\prod_{x:A} B(x)}{\Gamma \vdash f =_{\prod_{x:A} B(x)} \lambda(x).f(x) \; \mathrm{true}}
  • Computation rules for negative dependent sum types:
Γ,x:Ab(x):B(x)Γa:AΓπ 1(a,b)= AatrueΓ,x:Ab:BΓa:AΓπ 2(a,b)= B(π 1(a,b))btrue\frac{\Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash \pi_1(a, b) =_A a \; \mathrm{true}} \qquad \frac{\Gamma, x:A \vdash b:B \quad \Gamma \vdash a:A}{\Gamma \vdash \pi_2(a, b) =_{B(\pi_1(a, b))} b \; \mathrm{true}}
  • Uniqueness rules for negative dependent sum types:
Γz: x:AB(x)Γz= x:AB(x)(π 1(z),π 2(z))true\frac{\Gamma \vdash z:\sum_{x:A} B(x)}{\Gamma \vdash z =_{\sum_{x:A} B(x)} (\pi_1(z), \pi_2(z)) \; \mathrm{true}}
  • Computation rules for identity types:
Γ,a:A,b:A,p:a= AbCtypeΓt: x:AC(x,x,refl A(x))Γc:AΓJ(t,c,c,refl(c))= C(c,c,refl A(c))t(c)true\frac{\Gamma, a:A, b:A, p:a =_A b \vdash C \; \mathrm{type} \quad \Gamma \vdash t:\prod_{x:A} C(x, x, \mathrm{refl}_A(x)) \quad \Gamma \vdash c:A}{\Gamma \vdash J(t, c, c, \mathrm{refl}(c)) =_{C(c, c, \mathrm{refl}_A(c))} t(c) \; \mathrm{true}}

 See also

Last revised on January 15, 2024 at 15:45:23. See the history of this page for a list of all contributions to it.