nLab heterogeneous equality

Redirected from "propositional heterogeneous equality".

Context

Equality and Equivalence

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Contents

Idea

A form of equality which allows for elements of families of types to be compared for equality.

Definition

Typal heterogeneous equality

In the type theory literature, there are different kinds of types which are called heterogeneous equality types:

Propositional heterogeneous equality

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 called propositional equality, 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. Similarly, every type family B(x)B(x) indexed by x:Ax:A has a family of binary relations, according to which, given two elements xx and yy of AA where x= Ayx =_A y, and two elements aa of B(x)B(x) and bb of B(y)B(y), aa and bb are related if and only if they are equal across the equality x= Ayx =_A y. Since relations are propositions in the context of a term variable judgment in the type layer, this is called propositional heterogeneous equality or heterogeneous propositional equality. The formation and introduction rules for propositional heterogeneous equality is as follows

ΓAtypeΓ,x:AB(x)typeΓ,x:A,y:A,x= Aytrue,a:B(x),b:B(y)a= ̲.B x= AybpropΓAtypeΓ,x:AB(x)typeΓ,x:A,a:B(x)a= ̲.B x= Axatrue\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, x:A, y:A, x =_A y \; \mathrm{true}, a:B(x), b:B(y) \vdash a =_{\underline{ }.B}^{x =_A y} b \; \mathrm{prop}} \quad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma, x:A, a:B(x) \vdash a =_{\underline{ }.B}^{x =_A x} a \; \mathrm{true}}

Then we have the elimination rules for propositional heterogeneous equality:

ΓAtypeΓ,x:AB(x)type Γ,x:A,y:A,x= Aytrue,a:B(x),b:B(y),a= ̲.B x= AybtrueP(a,b,x,y)prop Γ,x:A,a:B(x),P(x,x,a,a)trueΓ,x:A,y:A,x= Aytrue,a:B(x),b:B(y),a= ̲.B x= AybtrueP(a,b,x,y)true\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma, x:A, y:A, x =_A y \; \mathrm{true}, a:B(x), b:B(y), a =_{\underline{ }.B}^{x =_A y} b \; \mathrm{true} \vdash P(a, b, x, y) \; \mathrm{prop} \\ \Gamma, x:A, a:B(x), \vdash P(x, x, a, a) \; \mathrm{true} \end{array} }{\Gamma, x:A, y:A, x =_A y \; \mathrm{true}, a:B(x), b:B(y), a =_{\underline{ }.B}^{x =_A y} b \; \mathrm{true} \vdash P(a, b, x, y) \; \mathrm{true}}

Properties

Heterogeneous equalities are equivalence relations

The introduction rule of heterogeneous equality says that heterogeneous 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, and for all a:B(x)a:B(x) and b:B(y)b:B(y) such that a= ̲.B x= Ayba =_{\underline{ }.B}^{x =_A y} b, we have b= ̲.B y= Axab =_{\underline{ }.B}^{y =_A x} a. Non-heterogeneous equality is symmetric, which means that for all x:Ax:A and y:Ay:A such that x= Ayx =_A y, y= Axy =_A x. By the introduction rule, we have that for all x:Ax:A and a:B(x)a:B(x), we have that a= ̲.B x= Axaa =_{\underline{ }.B}^{x =_A x} a, and because all propositions imply themselves, we have that a= ̲.B x= Axaa =_{\underline{ }.B}^{x =_A x} a implies a= ̲.B x= Axaa =_{\underline{ }.B}^{x =_A x} a. Thus, by the elimination rules for heterogeneous equality, for all x:Ax:A and y:Ay:A such that x= Ayx =_A y, and for all a:B(x)a:B(x) and b:B(y)b:B(y) such that a= ̲.B x= Ayba =_{\underline{ }.B}^{x =_A y} b, we have b= ̲.B y= Axab =_{\underline{ }.B}^{y =_A x} a.

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 and y= Azy =_A z, and for all a:B(x)a:B(x), b:B(y)b:B(y), and c:B(z)c:B(z) such that a= ̲.B x= Ayba =_{\underline{ }.B}^{x =_A y} b, b= ̲.B y= Aycb =_{\underline{ }.B}^{y =_A y} c implies a= ̲.B x= Azca =_{\underline{ }.B}^{x =_A z} c. Non-heterogeneous equality is transitive, that for all x:Ax:A, y:Ay:A, and z:Az:A such that x= Ayx =_A y and y= Azy =_A z, 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 a= ̲.B x= Axaa =_{\underline{ }.B}^{x =_A x} a, and because all propositions imply themselves, we have that a= ̲.B x= Azca =_{\underline{ }.B}^{x =_A z} c implies a= ̲.B x= Azca =_{\underline{ }.B}^{x =_A z} c, and because true propositions imply true propositions, we have that a= ̲.B x= Axaa =_{\underline{ }.B}^{x =_A x} a implies that a= ̲.B x= Azca =_{\underline{ }.B}^{x =_A z} c implies a= ̲.B x= Azca =_{\underline{ }.B}^{x =_A z} c. Thus, by the elimination rules for heterogeneous equality, or all x:Ax:A, y:Ay:A, and z:Az:A such that x= Ayx =_A y and y= Azy =_A z, and for all a:B(x)a:B(x), b:B(y)b:B(y), and c:B(z)c:B(z) such that a= ̲.B x= Ayba =_{\underline{ }.B}^{x =_A y} b, b= ̲.B y= Aycb =_{\underline{ }.B}^{y =_A y} c implies a= ̲.B x= Azca =_{\underline{ }.B}^{x =_A z} c.

Thus, heterogeneous equality is an equivalence relation.

Dependent functions are extensional

For all dependent function f: x:AB(x)f:\prod_{x:A} B(x) and elements x:Ax:A and y:Ay:A such that x= Ayx =_A y, f(x)= ̲.B x= Ayf(y)f(x) =_{\underline{ }.B}^{x =_A y} f(y):

f: x:AB(x).x:A.y:A.x= Ayf(x)= ̲.B x= Ayf(y)\forall f:\prod_{x:A} B(x).\forall x:A.\forall y:A.x =_A y \implies f(x) =_{\underline{ }.B}^{x =_A y} f(y)

This is because for all dependent function f: x:AB(x)f:\prod_{x:A} B(x), by the introduction rule for heterogeneous equality, for all elements x:Ax:A, f(x)= ̲.B x= Axf(x)f(x) =_{\underline{ }.B}^{x =_A x} f(x), and the elimination rule for heterogeneous equality states that if for all elements x:Ax:A, f(x)= ̲.B x= Axf(x)f(x) =_{\underline{ }.B}^{x =_A x} f(x), then for all elements x:Ax:A and y:Ay:A such that x= Ayx =_A y, f(x)= ̲.B x= Ayf(y)f(x) =_{\underline{ }.B}^{x =_A y} f(y).

Dependent function extensionality

The extensionality principle for dependent product types (dependent function extensionality) states that for all dependent functions f: x:AB(x)f:\prod_{x:A} B(x) and g: x:AB(x)g:\prod_{x:A} B(x), f= x:AB(x)gf =_{\prod_{x:A} B(x)} g if and only if for all a:Aa:A and b:Ab:A such that a= Aba =_A b, f(a)= ̲.B a= Abg(b)f(a) =_{\underline{ }.B}^{a =_A b} g(b)

f: x:AB(x).g: x:AB(x).f= x:AB(x)ga:A.b:A.a= Ab(f(a)= ̲.B a= Abg(b))\forall f:\prod_{x:A} B(x).\forall g:\prod_{x:A} B(x).f =_{\prod_{x:A} B(x)} g \iff \forall a:A. \forall b:A.a =_A b \implies (f(a) =_{\underline{ }.B}^{a =_A b} g(b))

Relation to non-heterogeneous propositional equality

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 functions

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.

Last revised on November 13, 2023 at 18:10:56. See the history of this page for a list of all contributions to it.