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

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.

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

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:

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

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.

• Definitional equality is sometimes known as judgemental equality.
• Propositional equality is indicated by the presence of an inhabited identity type (id).

Equality of Types and Terms

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

• terms
• types
• type families (types that depend on terms)
• and so on for higher orders,

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

t:AA=B t:B

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

• Integer is not identical to Boolean.
• Integer is identical to Integer.

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:
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]

C : T -> Type

f : x:T -> y:T -> (x=y) -> C(x) -> C(y) 

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.

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:

• Judgemental equality
• External equality

See this page for more information.

Propositional Equality

Propositional equality may also be known as:

• Equality type
• Identity type
• Internal equality
• Liebniz equality (well Liebniz equality is defined differently but we can convert between propositional equality and Liebniz equality so in this context they amount to the same thing, more information about this on this page)

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 AB then A=B can be constructed.

Embed definitional equality into propositional equality.

ab : A a=aa=b refl a = b

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

Identity (Propositional Equality) Constructor

see ncatlab

x = x : Type

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 (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 : (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).

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

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

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:

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 equality (ETT) equates things if they are constructed in the same way - If they normalise to the same value.
• Intentional equality (ITT) equates things that behave the same - If every property of x is equal to the property of y (satisfy the same predicates) then x=y.

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:Ax≡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:ARefl : 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:Ax≡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:ARefl : 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.

||| Equality is a congruence.
cong : {f : t -> u} -> (a = b) -> f a = f b
cong Refl = Refl

||| 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

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.

Rewrite in Idris

See Idris documentation.

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

equ: x=y

rewrite equ in prop

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

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: 1 2

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:

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

((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

Where:

• P is a property given by a family of types (type universe) for every pair of terms that are equal. We need to choose a suitable property depending on what we need to prove about identity types.

Why is the elimination rule so complicated for identity types?

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

Given:

• A function P which forms a type which depends on two terms of T and a constructor for the proposition a=b.
• A function from a term 'a' to an element of P (gives each terms equality to itself)

we get:

• An term of P for every pair of terms.

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	A:Type Γ, x:A, y:AIdA(x,y) : Type
term introduction rule reflexitvity Id is only inhabited if both elements of the pair are the same.	ΓA:Type Γ , a:Arefl(a) : IdA(a,a)
term eliminator
computation rule
Local completeness rule

Implemetations of Identity Type

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

(** [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 Γx:A,y:A,A:Type ΓIdA(x,y):Type type introduction Γx:A Γreflx:IdA(x,x):Type
examples	beta-reduction ΓT ΓT = T' Γt:T Γt=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 (aA). 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.

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

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.
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).
2-groupoids

sequent calculus notation:

• Γ- Γ is context.
• Type - is a universe of types (which may be an term in a higher order tower of universes).
• A:Type - A is a type in the universe of types
• A(x):Type - a family of types indexed by term x.
• Id_A(x,y):Type - Martin-Löf's identity type - collects the ways that x,y are identified.
• p:Id_A(x,y) - terms of Id give a reason why x and y are the same.
• refl:Id_A(x,x) - reflexivity proof, every term is equal to itself .

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 Id_A(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): ΓA:Type Γ,x:A,y:AIdA(x,y):Type from Warren: ΓA:Type Γx,y :A Id formation ΓIdA(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): ΓA:Type Γ,x:Ar(x):IdA(x,x):Type from Warren: ΓA:Type Id Introduction ΓrA(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)C(x,y,p):Type   Γ,x:A,C(x,x,r(x)):Type Γ,x:A,y:A,p:IdA(x,y)J(t; x,y,p):C(x,y,p) from Warren: Γ,x:A,y:A, z:IdA(x,y)B(x,y,z):Type Γ,u:A,b(u):B(u,u,rA(u)) Γp:IdA(a,a') ΓJA,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)C(x,y,p):Type   Γ,x:A,C(x,x,r(x)):Type Γ,x:AJ(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]

Computer Code

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

    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)

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:

• Idris
• Coq

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 ΓP:IdA(M,N) ΓM=N : A UIP ΓP:IdA(M,N) ΓP=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:

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:

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
Sum A B	eliminator removes information uses energy

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.

EuclideanSpace

home

This Page

This page is part of a set of pages about type theory, these pages start here.

Related Subjects

On this site:

• For more information about Univalence Axiom see page here.
• For more information about Propositional, First Order and Higher Order Logic see page here.
• More information about setoid and groupoid structures.
• For information about how equality proofs are implemented in the Idris language see this page.
• Equality in category theory.

Other Sites

• http://strictlypositive.org/obseqnow.pdf

Type Equality in Idris

Handbook of Mathematics - This is a really useful reference book where you can find formulas, definitions and descriptions of a wide range of mathematics. The book is very nicely bound with a flexible plastic cover.

Inverse Functions

Equality

In Set Theory More on page here.		Two sets are equal if they contain the same elements (Principle of Extensionality). If the set has structure then that would also have to be equal in some way.
In Category Theory More on page here.		Often when comparing types we need some loser way of considering that two types are essentially the same. Isomorphism is frequently the most appropriate type of equality. This is defined using a category theory way, that is, by external morphisms.
In Type Theory More on page here.	vec(x)=vec(x+0)	In M-L type theory the Identity type is often used. If things are equal in this way they can be interchanged when used in computer programs.
In Type Theory More on page here.		In Homotopy Type Theory (HoTT) there is a different way to get isomorphism from equality. That is to allow types to be equal in many ways.

Curry-Howard Correspondence

There is a relationship between computer programs and mathematical proofs, this is known as the Curry-Howard correspondence.

A type in λ-calculus has the same mathematical structure as a proposition in intuitionistic logic.

A constructor for that type corresponds to a proof of the proposition. The following table has some specific types with their corresponding propositions:

For more information about the Curry-Howard correspondence see the page here.