Maths - Equality of Terms and Types

On these pages we look at both equality between terms and equality between types (and how they are related).

Equality of Sets

To get some intuition lets first look at equality between sets. There are multiple ways to define 'equality' between sets. Here I have divided them into 'internal' or 'external' depending whether they look inside the set.

'Internal Equalities' 'External Equalities'
  • same elements
  • Id
  • Leibniz equality

Explained below

  • isomorphism

Explained below

isomorphism

The traditional way to define equality of sets, in set theory, is to say two sets are equal if they contain the same elements.

Equality of Types in Mathematics

In mathematics the natural way to relate types is often to use a weaker form of equality called isomorphism.

IdA = G•F
F•G = IdB

However, for checking the type consistency above, this is too loose. For example, the types A×B and B×A are isomorphic and they might hold the tuples (a,b) and (b,a) which are not the same without swapping the first and second elements.

isomorphism

Note: that this definition of isomorphism requires another type of 'equality' called Id. So, in the end, the definition of 'external' equality still requires an 'internal' equality but a very simple one.

Extensionality

In logic, extensionality, or extensional equality, refers to principles that judge objects to be equal if they have the same external properties.

Equality of Terms

If we have a simple type, such as Nat, it should be fairly simple to determine equality between numbers. For example the compiler can tell that 1=1 and 1≠2.

However, for these purposes, we are usually working with terms (expressions). So, instead of comparing elements of Nat it is like comparing elements of Expr Nat. This means we have to determine potential equalities like: 2*3=5+1.

To do this both sides of the equation are normalised (evaluated) to give us 6=6 in this example and then the equality is checked.

However these expressions can also contain variables and this is where things start to get more complicated. It is still possible that the compiler can do a certain amount of normalisation but exactly what will normalise will depend on the compiler and there are usually equalities that are true but don't normalise to a definitional equality.

It is not always obvious which expressions will normalise further and which won't. For instance x+0 may normalise to x but 0+x may not normalise any further.

Equality of Functions

Two functions are equal if their values are equal at every argument.This is known as functional extensionality.

Equality of Types

We can move from talking about equality of sets to equality of types. Instead of the concept that two sets are equal if they have the same elements we may be able to use the idea that two types are equal if they have the same constructors.

'Internal Equalities' 'External Equalities'
  • same constructors
  • Id
  • Extentional equality
  • Leibniz equality
  • Definitional and Propositional Equality

Explained below

  • isomorphism

Explained below

  isomorphism

Equality of Properties

Equality is a property, but what about equalities between properties? That is equalities between equalities (higher order equalities). How do we determine these?

in simple cases an equality could be represented by a Boolean value, in which case properties would be equal if they were both true or both false, however here we are using inhabited types to indicate truth and uninhabited types represent unproven. So how do we represent equality between these?

A naive approach might be to define equality of properties like this:

proven proven equal
proven unproven unequal
unproven proven unequal
unproven unproven equal

but that's not really in the spirit of M-L type theory, how do you test if something is unproven?

Here is a proof of Leibniz equality. (using Arend Theorem Prover)

In Arend idp is just reflexitivity (Refl)

idp : a = a
\func Leibniz {A : \Type} {a a' : A}
  (f : \Pi (P : A -> \Type) ->
       \Sigma (P a -> P a') (P a' -> P a)) : a = a'
  => (f (\lam x => a = x)).1 idp

An approach is to say the property of a is equal to the property of a' if P a implies P a' and P a' implies P a.

Definitional and Propositional Equality

Here we are looking at the relationship between two types of equality: definitional equality and propositional equality.

In Nat consider 'n', '0+n' and 'n+0' they are equal terms in some way.

In Idris 'n' and '0+n' are definitionally equal because they automatically normalise to the same. Definitionally equality is sometimes denoted with a 3-bar equals sign (≡) or just by using the same symbol.

But 'n+0' is propositionally (but not definitionally) equal to n. It is denoted with a normal equals sign (=) and shown as an arrow between nodes.

computational path

Equality of Types and Terms

Because we are working in dependant type theory we need to be able to determine the equality of:

This leads to a complex structure, for these equalities, which can be represented by a setoid (see page here) or groupoid (see page here).

One of the main differences between set theory and type theory is that terms (elements in set theory terminology) only exist within the type they are defined in.

So, if we have an term x:A and we need to express it like this x:B we need to know that A and B are effectively the same type, close enough that it makes no difference. This is an identity (Id).

Equality of Types

A and B can only contain the same term if they are the same type:

equality conversion rule

 
right adjointt:Aright adjointA=B
right adjointt:B

For discrete types, it is easy to know if they are identical, for instance:

The interesting cases are for dependent types. How do we determine if members of a type family are identical?

Here C(A) is a type family that depends on A:

  type family

If x and y are propositionally equal then C(x) is identical enough to C(y) to be treated as the same type.

[ref Homotopy Type theory: Univalent Foundations - Section 1.12 Identity Types]

 
So if we have a type family C and a function f like this:  
C : T -> Type

f : x:T -> y:T -> (x=y) -> C(x) -> C(y) 
Then C(x) will be identical to C(y) and can be exchanged and treated the same in a program.  
f(x,x,refl) = Id 

At first it looks like the function f is partial in that, we could put any values for x and y, but it is only valid when x=y. However, for programs like Idris, x=y will be checked at compile time and so cannot be run unless x=y (a proof exists that x=y).

Type Checking in Computer Programs

At compile time the compiler will need to check that types are consistent and what is expected.

In the case of dependent types equality of types will depend on equality of terms. For example, if we are adding two vectors we require the lengths to be the same, so we need to be able to prove the equality of the lengths even if they are variables.

Theories

There are different type theories, with different uses, depending on the way properties are preserved under different definitions of equalities.
 

ETT

Extensional Type Theory

ITT

Intentional Type Theory

HoTT

Homotopy Type Theory

Equality Used Exact equality (after normalisation) Leibniz equality Equivalence
  see page here see page here see page here

In M-L extensional type theory two types are the same only if they are defined in exactly the same way. This becomes very important for dependent types, for example, vectors can only be added if they have the same length, however (Vect n) and (Vect (n+0)) would be treated as different types in extensional type theory. This means that extensional type theory limits the calculations and checks that can be done.

In M-L intentional type theory two types are the same if they are defined in the same way or if there is a proof that they are equal. However, in intentional type theory, proofs are not canonical for instance to construct a proof we may have to make expressions more complicated before we can simplify them. So there is not a general algorithm for constructing proofs and each proof required may have to be supplied by a human coder.

In homotopy type theory proofs are canonical (canonicity) and therfore automatic but to get this benefit other things get more complicated (conservation of complexity?). In homotopy type theory structures are built constructively rather than having constraints in the form of equations instead we have rules. The intuition for this type theory comes from homotopy.

Definitional Equality

may also be known as:

See this page for more information.

Propositional Equality

Propositional equality may also be known as:

See this page for more information.

There is another type of equality which here is denoted by the usual two-bar equals sign '='.

A=B is a proposition which may, or may not, be true. To prove it is true we need to construct an instance of it. The constructor for such a proof is called 'refl'.

This quality of being equal to itself is called reflexitivity (refl). See equivalence.

Definitional equality can be embedded into propositional equality because if A=B then A=B can be constructed.

Embed definitional equality into propositional equality.  
right adjointa=b : A
right adjointa=a=a=b
right adjointrefl a = b

More about propositional equality and definitionaly equality (with Idris examples) on page here.

Identity (Propositional Equality) Constructor

see ncatlab

If we have an identity type

 
x = x : Type

then we can construct it with a simple constructor with no parameters

 
Refl : x = x

That is, if x=x is inhabited by Refl that constitutes a proof that x=x.

However this hides a lot of complexity, if we use the same symbol on both sides of the equation - what does that mean? We might say that the meaning comes from the deconstuctor but how is this all implemented?

In some ways we could think of rewrite as like a second constructor for an equality type. So it behaves a bit like an inductivly defined type where Refl can construct a definitional equality on its own but requires the help of rewrites to identity as inductive type

Identity (Propositional Equality) Deconstructor/Eliminator

There are also two possible deconstructors/eliminators known as J and K.

(K does not apply to some flavors of type theory)

In the same way that, in Leibniz equality, equal terms have equal properties we can now consider properties of equalities.

j deconstructor

The first part 'P' is a dependent type. We could think of it as property which is true for every pair of terms which are equal:

(P : (a,b:t) -> (a=b) -> Type)

The next part shows that an element of each of these types (Refl) can be constructed and are therefore 'true':

((a:t) -> P a a Refl)

The result say that every property that is true for identical things also is true of a thing with itself.

((a,b:t) -> (p:a=b) -> P a b p)

J : (P : (a,b:t) -> (a=b) -> Type) ->
    ((a:t) -> P a a Refl) ->
    ((a,b:t) -> (p:a=b) -> P a b p)
J P h a a Refl = h a

When all properties of a type are the same this is also known as Leibniz equality (see page here) however P is a property of two equal terms.

Axiom J allows the possibility of many equality constructors Refl (although the single name and the pattern matching rules in Idris would prevent that).

Examples Rational Numbers

Wiki Each number has numerator p and a non-zero denominator q. So P could be defined like this:

 P : (a,b:t) -> (a=b) -> Type
 P a b Refl = (ap*bq = aq*bp)

So ((a:t) -> P a a Refl)

If we want to specifically prevent the possibility of multiple Refl constructors then axiom K applies:

Axiom K

K : (P : (a:t) -> (a=a) -> Type)

((a:t) -> P a Refl)

((a:t) -> (p:a=a) -> P a p)

K : (P : (a:t) -> (a=a) -> Type) ->
    ((a:t) -> P a Refl) ->
    ((a:t) -> (p:a=a) -> P a p)
K P h a Refl = h a

K: ΠA:TypeΠx:AΠP: x=x -> Type(P (Refl) -> Πh:x=xP(h))

Asserts that each term of each identity type x=x (of equivalences of a term x:A) is propositionally equal to the canonical reflexivity equality proof Refl:x=x.

Unary predicate by diagonalization of binary predicate J

Cantor's diagonal argument

Another consequence of this is the higher order identity types:

x=p=qy   [or in the other notation: IdIdA(p,q)(x,y)]

are always inhabited. This is known as 'uniqueness of identity proofs (UIP).

Extensional and Intentional Type Theory

This is where extensional and intentional type theory start to diverge.

 

Extensional type theory has some nice properties when using for computing but undecidable type checking.

Intentional type theory allows programs that may be non-terminating.

Extensional Type Theory (ETT)

Allows provable equations to impact directly on type checking without the need for explicit substitutions.

If x and y are definitionally equal then they are propositionaly equal.  
A:Type, x:A, y:Aright adjointx≡y
Refl : x = y

equality reflection rule

In ETT only, if x and y are propositionaly equal then they are definitionally equal.

That is, the two types of equality are interchangeable.

 
A:Type, x:A, y:Aright adjointRefl : x = y
x≡y

Undecidable type checking

Program always has normal form

ncatlab - Extensional type theory denotes the flavor of type theory in which identity types must be propositions (of h-level 1). In other words, they are determined by their extensions — the collection of pairs of points which are equal.

Intentional Type Theory (ITT)

Keeps definitional equality and propositional equality more separate.

As with ETT, If x and y are definitionally equal then they are propositionaly equal.  
A:Type, x:A, y:Aright adjointx≡y
Refl : x = y

But the inverse is not true, if x and y are propositionaly equal then they are not necessarily definitionally equal.

However, we may be able to turn propositional equality into definitional equality by using a sequence of rewrite/substitution/induction rules.

However there is not a general algorithmic way to do this.

 
A:Type, x:A, y:Aright adjointRefl : x = y
s (x≡y)

where:

  • s takes the place of Refl and is a sequence of rewrite/substitution/induction rules.

So we may need to provide these proofs by adding code to the program.

This allows definitional equality to remain decidable.

But this reduces the power of the propositional equality.

Requires an explicit operation, transporting values between types which are merely provably, but perhaps not definitionally, equal.

Leibniz Equality and Indiscerniblity of Identicals

More about Leibniz equality on page here.

Leibniz equality says that if two terms have the same properties, for all properties, then they are equal.

When programming we might represent properties as a function from a term to a type.

 

||| Equality is a congruence.
cong : {f : t -> u} -> (a = b) -> f a = f b
cong Refl = Refl
Idris code from Github
So if we have a property: Prop : A -> Type
and if we have a proof that x=y where x and y are both of type A: Refl : x=y
and we have a proof that Prop x is true: Refl: Prop x
then Prop y is true: Refl: Prop y
For example, in Idris, replace or rewrite (which has a nicer syntax)
||| Perform substitution in a term according to some equality.
replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
replace Refl prf = prf
Idris code from Github
In this context Leibniz equality is the same as propositional equality.

Rewrites

In order to construct an identity type, such as n=n+0, we need proof that n does equal n+0. In a programming environment we do that by rewriting n=n+0 to n=n and then constructing using Refl. computational path

Rewrite in Idris

See Idris documentation.

prop: Nat -> Type
prop x = (x=2)

equ: x=y

rewrite equ in prop
 

This does the following:

  • Start with an equation x=y and a property prop : x -> Type
  • Search for x in prop
  • Replaces all occurrences of x with y in prop.
Here is a proof in Idris for n=n+0 using the 'rewrite' keyword.  
plusReducesR : n = plus n 0
plusReducesR {n = Z} = Refl
plusReducesR {n = (S k)} = let rec = plus_commutes_Z {n=k} in
                                  rewrite rec in Refl

There is more information about how to write proofs in Idris on the page here.

Rewrite in AGDA

See AGDA documentation.

In AGDA we seem to be able to put the rewrite on the LHS of a function definition where the 'rewrite' keyword translates to a 'with' construction.

plusC : (a b : Nat) -> P (a + b) -> P (b + a)
plusC a b t with   a + b  | plus-commute a b
plusC a b t    | .(b + a) | refl = t
  This proves that some property of a+b is also true of b+a.

 

Formation, Introduction and Elimination of Identity Type Families

Identity Type Families model propositional equality.

Formation: A type exists for every pair of terms in base type

Introduction: The above types are only inhabited if the terms are propositionally equal.

refl: introduces terms.

J: eliminates terms.

see these sites:

equality theory

The elimination rule 'J' for propositional equality can be explaind by thinking of the propositional equality as Leibniz equality as discussed on the page here.

Equality Type Constructor

The equality type only has one constructor which is Refl (short for reflexive).

If we have an equation, such as 1+1=2, this can be constructed using Refl only if the left and right of the equation is the same. We think of this constructor as proof of that the equation is true.

If we have an identity with a variable, such as (x:Nat) -> x = x + 0, then we need to be able to generate a Refl for every value of x. For information about how to do this see the page here.

Equality Type eliminator

This goes in the opposite direction, that is, start with an equality type and take it apart somehow. The equality type eliminator, traditionally called J has two parameters:

A function P which generates a type family. This gives a type for every pair of elements.

(P : (a,b:t) -> (a≡b) -> Type)
A proof of equality for equal elements.
((a:t) -> P a a Refl)

From these parameters we can then generate the following function:

((a,b:t) -> (p:a≡b) -> P a b p)

Elimination Rule (J)

Here is the constructor and eliminator for

Constructor Eliminator
Refl
equality deconstructor

Where:

Why is the elimination rule so complicated for identity types?

Simpler Case of Eliminator for a Group

Sometimes it helps to look at a simpler structure first to get some intuition.

In the case of a finite group the constructors are the permutations representing the generators. By combining these generators we get other permutations.

So the constructor is a set of permutations however, the same group may be generated by different sets of permutations.

So what would be the eliminator? The eliminator should not have to choose and one set of permutations when other sets would be just as good.

In the case of a groupoid the elimination rule (J) determines the induction/recursion principles. J says:

Given:

we get:

Path Induction

The idea of path induction is to prove that a property holds for all identifications between terms in some A it suffices to show that the property holds for all trivial self-identities refl.

 

Propositional Equality - Identity Type

ref

 

Identity Type

formation rule

Id exists for every pair of terms in A

right adjointA:Type
Γ, x:A, y:Aright adjointIdA(x,y) : Type

term introduction rule

reflexitvity

Id is only inhabited if both elements of the
pair are the same.

Γright adjointA:Type
Γ , a:Aright adjointrefl(a) : IdA(a,a)
term eliminator  
computation rule  

Local completeness rule

 

Implemetations of Identity Type

Idris

from : Idris-dev/libs/prelude/Prelude/Basics.idr

||| Identity function.
id : a -> a
id x = x

COQ

from : coq/theories/Init/Datatypes.v

(** [identity A a] is the family of
    datatypes on [A] whose sole non-empty
    member is the singleton datatype [identity A a a] whose
    sole inhabitant is denoted [identity_refl A a] *)

#[universes(template)]
Inductive identity (A:Type) (a:A) : A -> Type :=
  identity_refl : identity a a.
Hint Resolve identity_refl: core.

Arguments identity_ind [A] a P f y i.
Arguments identity_rec [A] a P f y i.
Arguments identity_rect [A] a P f y i.

Register identity as core.identity.type.
Register identity_refl as core.identity.refl.
Register identity_ind as core.identity.ind.

(** Identity type *)

Definition ID := forall A:Type, A -> A.
Definition id : ID := fun A x => x.

Definition IDProp := forall A:Prop, A -> A.
Definition idProp : IDProp := fun A x => x.

Definitional Equality vs. Propositional Equality

Type theory without dependant types is computable in that we can easily type check code. Dependent types allow much more powerful compile-time checking but now we cant be certain that we can type check at compile-time. To understand this dilemma we need to spilt type equality into definitional and propositional equality.

ref: http://www.cs.nott.ac.uk/~psznk/docs/karlsruhe.pdf

 

Definitional Equality

(Judgements)

Propositional Equality
  decidable equality equality needing a proof
for program:

static (syntax)

This is the equality the type checker uses, it is equality that can be decided statically, at compile time.

dynamic (semantics)

we may need to run program to determine equality at runtime.

for Curry-Howard  

true if ID type can be inhabited (constructed). There is an Id type for every two elements IdA(x,y) but it is only inhabited if they are the same IdA(x,x).

type formation Γright adjointx:A,y:A,A:Type
Γright adjointIdA(x,y):Type
type introduction Γright adjointx:A
Γright adjointreflx:IdA(x,x):Type
examples
  • beta-reduction
  • Γright adjointT
  • Γright adjointT = T'
  • Γright adjointt:T
  • Γright adjointt=t':T

eta equality is included in some proof checkers Agda and Epigram but not Coq.

What you use when stating a proposition (x = x + 0) to be proved.
     

In set theory (and in logic based on set theory) many propositions are about whether something is an element of a given set (a∈A). In type theory a term does not exist outside the type therefore, whether a term is part of a type (a:A), is definitional not propositional.

  Set Theory Type Theory
Definitional Equality

a∈A

membership of a set may be either defined or be a proposition

a:A
Propositional Equality Id

Propositional Equality

For every pair of terms there is an identity type. If these two terms are equal the type can be constructed by Rafl definitional equality

The equalities that are supported, or otherwise, by an evidence (a composition of rewrites). - Queiroz, Oliveira.

Set

The first way to construct terms of IdA(x,y) is to use refl.

refl : Π(a:A), Id(a,a)

This gives a set without additional structure (discrete homotopy).

There is a type for every pair of points but only loops are ocupied.

groupoid 0

1-groupoids

In addition to refl, for any given type family A(x,y,p) indexed by terms x,y:X and p:Id(x,y) and any given function

f : Π(x:X), A(x,x,refl(x)),

we have a function

J(A,f) : Π(x,y:X), Π(p:Id(x,y)), A(x,y,p)

with J(A,f)(x,x,refl(x)) stipulated to be f(x).

groupoid 1

2-groupoids

 

 

sequent calculus notation:

Propositional Equality in Computer Languages

Propositional equality is used in proof assistants but a general language - Idris allows propositional equalities to be declared (see here), allowing theorems about programs to be stated and proved. Equality is built in, but conceptually has the following definition:

data (=) : a -> b -> Type where
    Refl : x = x

Equalities can be proposed between any values of any types, but the only way to construct a proof of equality is if values actually are equal. For example:

fiveIsFive : 5 = 5
fiveIsFive = Refl

 

twoPlusTwo : 2 + 2 = 4
twoPlusTwo = Refl 

Id - Identity type

see site here for a good overview

We can interpret equalities between 2 terms 'a' and 'b' as being a computational path between the two terms, that is sequences of rewrites and substitutions that turn 'a' into 'b'.

The collection of all these terms is the identity type Id(a,b).

Ways to constuct terms of IdA(x,y)

refl : Π(x:X), Id(x,x),

In addition to refl, for any given type family A(x,y,p) indexed by terms x,y:X and p:Id(x,y) and any given function

f : Π(x:X), A(x,x,refl(x)),

we have a function

J(A,f) : Π(x,y:X), Π(p:Id(x,y)), A(x,y,p)

with J(A,f)(x,x,refl(x)) stipulated to be f(x).

Then, in summary, the identity type is given by the data Id,refl,J. With this, the exact nature of the type Id(x,y) is fairly under-specified. It is consistent that it is always a subsingleton in the sense that K(X) holds, where

K(X) := Π(x,y:X), Π(p,q:Id(x,y)), Id(p,q).

Using Introduction and Elimination Rules (see ncatlab)

type formation

For every pair of terms of A we introduce a type IdA which is inhabited when the terms are equal.

from ncatlab (hypothetical form):
Γright adjointA:Type
Γ,x:A,y:Aright adjointIdA(x,y):Type

from Warren:

Γright adjointA:Type Γright adjointx,y :A Id formation
Γright adjointIdA(x,y):Type

term introduction

reflexivity

Without univalence, refl is the only given way to construct terms of the identity type.

the univalence axiom provides a means of constructing terms other than refl(x), at least for some types, and hence the univalence axiom implies that some types are not sets. (Then they will instead be 1-groupoids, or 2-groupoids, ∞-groupoids.

A term is alway equal to itself, this is given by the reflexivity operator (refl or r(a)) like this:
a:A
r(a):IdA(a,a)

Or more formally:

from ncatlab (hypothetical form):

Γright adjointA:Type
Γ,x:Aright adjointr(x):IdA(x,x):Type

from Warren:

Γright adjointA:Type Id Introduction
Γright adjointrA(a):IdA(x,x)

rA(a) is the reflexitivity term for 'a'

term elimination
  • for any x,y:A and any reason p:IdA(x,y) why they are the same, we have a type C(x,y,p), and
  • if x and y are actually identical and p:IdA(x,x) is the reflexivity proof r(x), then we have a specified term t:C(x,x,r(x))),

then we can construct a canonically defined term J(t;x,y,p):C(x,y,p) for any x, y, and p:Id A(x,y), by “transporting” the term t along the proof of equality p.

from ncatlab:
Γ,x:A,y:A, p:IdA(x,y)right adjointC(x,y,p):Type   Γ,x:A,right adjointC(x,x,r(x)):Type
Γ,x:A,y:A,p:IdA(x,y)right adjointJ(t; x,y,p):C(x,y,p)

from Warren:

Γ,x:A,y:A, z:IdA(x,y)right adjointB(x,y,z):Type

Γ,u:A,right adjointb(u):B(u,u,rA(u))

Γright adjointp:IdA(a,a')

Γright adjointJA,B([u:A] b(u), a, a',p):B(a,a',p)

J is the elimination term

B is type representing identity

variable 'u' gets bound, indicated by square brackets.

computation rule

β-reduction
We can substitute along a reflexitivity proof without changing it.
Γ,x:A,y:A, p:IdA(x,y)right adjointC(x,y,p):Type   Γ,x:A,right adjointC(x,x,r(x)):Type
Γ,x:Aright adjointJ(t; x,x,r(x)) = t

Where:

  • = is definitional equality
coherence or "Beck-Chevalley" rules    

Reflexitivity does not fully define equality, for example ≥is reflexive but is not the same as =. The eliminator 'J' is the 'least reflexive relation' that is, only types on the diagonal are inhabited, this is its universal property (extreemal clause).

If the types which are not on the diagonal are not inhabited we can say anything about them, so we need a function going in the other direction (the eliminator).

J=Q[M/a]

 

Definitional Equality

(Judgmental Equality)

Propositional Equality

(Identity Equality)

 

The equality used when making a definition:

f(x) = x

The equality you use when stating a proposition to be proved:

x = x + 0

  For instance the symbols “2” and “s(s(0))” (meaning the successor of the successor of 0) are definitionally/intensionally equal terms (of type the natural numbers): the first is merely an abbreviation for the second  
written x ≡ y

x =A y

short for- x : A = y : A

 
  • Equal iff they have same normal form
  • Types are decidable
  • Equal if ID(a1,a2) is inhabited
  • Types are not decidable for natural numbers or greater complexity.
 

it 'controls type-checking'.

if a:A, and A≡B , then a:B.

if only p:A=B, then instead of a:B we have

Suppose that P is a type family over A and that

p:x =A y.

Then there is a function p*: P(x)->P(y).

  inferred automatically by the type checker a type with corresponding term formers
 

The propositional equality type, containing proofs of equality between x and y . Here x and y must have the same type A , and if we have A : Typei , then we also have x ≡ y : Typei.

 
introduction rule

reflexivity

refl : { A : Typei } -> ( x : A ) -> x ≡ x

 
equality eliminator

traditionally called J

J : { A : Typei } ->

( P : ( x y : A ) -> x ≡ y -> Typej ) ->

(for allx . P x x ( refl x )) ->

for all{ x y } . ( eq : x ≡ y ) ->P x y eq

 
computation rule    
     

Computer Code

To try to understand the equality eliminator 'J' here is some code:

Idris Code

From Philip Dorrell s github repository where a postulated '~~' identity type is equivalent in what it implies to the built in Idris '=' identity type.

No constructor given. We would expect refl_ to be the implementation of ~~ but instead it is another undefined function.

    infix 40 ~~
     
    postulate (~~) : t -> t -> Type
     
    postulate refl_ : (a:t) -> a ~~ a
     
    postulate J : (P : (a,b:t) -> (a~~b) -> Type) ->
        ((a:t) -> P a a (refl_ a)) ->
        ((a,b:t) -> (p:a~~b) -> P a b p)

Agda Code

from Univalence From Scratch by Martin Escardo

J : {𝓤 𝓥 : Universe} {X : 𝓤 ̇}
  -> (A : (x y : X) -> Id x y -> 𝓥 ̇)
  -> ((x : X) -> A x x (refl x))
  -> (x y : X) (p : Id x y) -> A x y p
J A f x .x (refl .x) = f x

For more information Idris and proof assistants see these pages:

Extensional Equality vs. Intentional Equality

 

Intentional Equality

Extensional Equality

Equality

Intentional equality equates things if they are constructed in the same way.

Extensional equality equates things that behave the same.

example

a+b not equal to b+a
because they are not definitionally equal.

 
type theory ITT ETT
properties Program always has normal form. Allows programs that may be non-terminating.
   
Id-Refl Γright adjointP:IdA(M,N)
Γright adjointM=N : A
UIP Γright adjointP:IdA(M,N)
Γright adjointP=refl(M) : A

only proof of Id is refl

The first form of extensional type theory (ETT) assumes types form a 'homotopy set' that is each type is a distinct point (see Oregon Programming Languages Summer School 2012 type theory part 5). HoTT takes this futher by allowing higher layers, types can be equal in multiple ways which gives a groupoid structure.

Examples

Example 1

Start with 2 types, Int and Bool, this allows us to generate other types: example 1
example 1 So, for instance, is Int ×Bool = Bool×Int ? Conventionally no because (3,true) ≠ (true,3) but Int ×Bool is isomorphic to Bool×Int. In HoTT we can express this isomorphism as representing equality in potenially many ways:

Example 2

Constructor contains proofs they are equal: example 2
example 2  

Information content of Terms

This may not be a formal part of type theory but informally we often think about concepts like η-reduction (tells us how to simplify a term that involves a constructor applied to an eliminator) in terms of not introducing new information.

Type Infomation Content of Term  
Unit 0 bits  
Product A B Add together information in A and B information product
Sum A B

eliminator removes information

uses energy

information sum

Category Theory - Ends and Dinatural Transformations

Bartosz Milewski

Equality in category theory.

Equality of Dependent Types

So how do we define equality of dependent types?

On this page we look at some of the issues involving varous type of 'equalities' of types.

dependant type equality

metadata block
see also:

On this site:

Other Sites

Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.

 

Terminology and Notation

Specific to this page here:

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.