There is a lot of interesting stuff to be said about equality in logic, higher category theory, and the foundations of mathematics, but it hasn't all been said here yet.

Different kinds of equality

Here is a list of distinctions between different notions of equality, in different contexts, where possibly all the following pairs of notions are, in turn, “the same”, just expressed in terms of different terminologies:

the difference between axiomatic and defined equality;
the difference between identity and equality,
the difference between intensional and extensional equality,
the difference between equality judgements, equality propositions, and equality types
the difference between equality and isomorphism,
the difference between equality and equivalence,
the possibility of operations that might not preserve equality.

Notions of equality in type theory

In a formal language such as type theory, one distinguishes various different notions of equality or equivalence of the terms of the language.

In type theory, there are broadly three different notions of equality which could be distinguished: judgmental equality, propositional equality, and typal equality. Judgmental equality is defined as a basic judgment in type theory. Propositional equality is defined as a proposition in any two-layered type theory with a layer of types and a layer of propositions. Typal equality is defined as a type in type theory.

Judgmental equality

The first notion of equality is judgmental equality, where we simply judge two elements to be equal to each other. Judgmental equality is expressed in type theory by a separate judgment: in addition to typing judgments Γ⊢(t:A)\Gamma \vdash (t:A), we have equality judgments Γ⊢(t=t′):A\Gamma \vdash (t = t'): A. The rules for manipulating such judgments then include reflexivity, symmetry, transitivity, making judgmental equality into a judgmental equivalence relation.

However, not all type theories have judgmental equality; most first-order theories use propositional equality in place of judgmental equality, and objective type theories use typal equality in place of judgmental equality.

Propositional 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 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:A⊢x= AypropΓ⊢AtypeΓ,x:A⊢x= 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:A,x= Aytrue⊢P(x,y)propΓ,x:A⊢P(x,x)trueΓ,x:A,y:A,x= Aytrue⊢P(x,y)true\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A, y:A, x =_A y \; \mathrm{true} \vdash P(x, y) \; \mathrm{prop} \quad \Gamma, x:A \vdash P(x, x) \; \mathrm{true}}{\Gamma, x:A, y:A, x =_A y \; \mathrm{true} \vdash P(x, y) \; \mathrm{true}}

Propositional equality satisfies the principle of substitution and the identity of indiscernibles:

Γ⊢AtypeΓ,x:A⊢P(x)propΓ,x:A,y:A⊢(x= Ay)⇒(P(x)⇔P(y))true\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash P(x) \; \mathrm{prop}}{\Gamma, x:A, y:A \vdash (x =_A y) \implies (P(x) \iff P(y)) \; \mathrm{true}}

In addition, one could have propositional equality between the types themselves, with formation and introduction rules

Γ⊢AtypeΓ⊢BtypeΓ⊢A=BpropΓ⊢AtypeΓ⊢A=Atrue\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A = B \; \mathrm{prop}} \qquad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash A = A \; \mathrm{true}}

Notable examples of propositional equality include the equality in all flavors of set theory, such as ZFC or ETCS.

The presence of propositional equality is part of the axiomatization of first-order theories, although this is usually swept under the rug by including propositional equality by default in all first-order theories. (It has to be made more explicit in a structural set theory such as SEAR, where there is no propositional equality on sets themselves, only on elements of a particular set.) By contrast, in a first order theory without propositional equality, propositional equality is an equivalence relation which has to be put onto a type or preset.

Typal equality

However, not all type theories are first order logic over type theory, nor are they even two-layered type theories. In type theories with only one layer for types, equality is not a relation. Instead, we have what are called typal equality, as equality of both terms and types are represented by types. Typal equality of terms is also called the equality type, identity type, path type, or identification type, and the terms of typal equality are called equalities, identities, identifications, paths. Notable examples of typal equality of terms include the identity type in Martin-Löf type theory and higher observational type theory, and the cubical path type in cubical type theory. Typal equality of types is also called equivalence of types, are written as A≃BA \simeq B for types AA and BB and are definable in all type theories with typal equality of terms, function types, dependent product types, and dependent sum types.

Type theories with only typal equality are called objective type theories. In type theories with both typal equality and either judgmental equality or propositional equality, one could distinguish between intensional type theories and extensional type theories: extensional type theories are type theories with an equality reflection rule, where one could derive judgmental or propositional equality of terms from typal equality of terms:

Γ⊢p:a= AbΓ⊢a≡b:AΓ⊢p:a= AbΓ⊢a≡ Abtrue\frac{\Gamma \vdash p:a =_A b}{\Gamma \vdash a \equiv b:A} \qquad \frac{\Gamma \vdash p:a =_A b}{\Gamma \vdash a \equiv_A b \; \mathrm{true}}

Intensional type theories are then type theories with typal equality and one of either judgmental or propositional equality without an equality reflection rule. Note that this notion of extensionality is different from the axiom of extensionality or function extensionality.

Comparison of equalities

This table gives the six different notions of equality found in type theory.

Judgment	of types	of terms
Judgmental equality	Γ⊢A=Btype\Gamma \vdash A = B \; \mathrm{type}	Γ⊢a=b:A\Gamma \vdash a = b:A
Propositional equality	Γ⊢A=Btrue\Gamma \vdash A = B \; \mathrm{true}	Γ⊢a= Abtrue\Gamma \vdash a =_A b \; \mathrm{true}
Typal equality	Γ⊢P:A≃B\Gamma \vdash P:A \simeq B	Γ⊢p:a= Ab\Gamma \vdash p:a =_A b

Structural rules of equalities

Reflexivity

The reflexivity of equality is given by the following judgmental, propositional, and typal rules respectively:

Reflexivity of judgmental equality

Γ⊢AtypeΓ⊢A=Atype\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash A = A \; \mathrm{type}}

Γ⊢AtypeΓ⊢a:AΓ⊢a=a:A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A}{\Gamma \vdash a = a:A}

Reflexivity of propositional equality

Γ⊢AtypeΓ⊢A=Atrue\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash A = A \; \mathrm{true}}
Γ⊢AtypeΓ⊢a:AΓ⊢a= Aatrue\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A}{\Gamma \vdash a =_A a \; \mathrm{true}}
Reflexitivity of typal equality (i.e. identity function and identity path)

Γ⊢AtypeΓ⊢id A:A≃A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash id_{A}:A \simeq A}
Γ⊢AtypeΓ⊢a:AΓ⊢refl A(a):a= Aa\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A}{\Gamma \vdash \mathrm{refl}_{A}(a):a =_A a}

Symmetry

The symmetry of equality is given by the following judgmental, propositional, and typal rules respectively:

Symmetry of judgmental equality

Γ⊢A=BtypeΓ⊢B=Atype\frac{\Gamma \vdash A = B \; \mathrm{type}}{\Gamma \vdash B = A \; \mathrm{type}}
Γ⊢AtypeΓ⊢a=b:AΓ⊢b=a:A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a = b:A}{\Gamma \vdash b = a:A}
Symmetry of propositional equality

Γ⊢AtypeΓ⊢BtypeΓ⊢A=BtrueΓ⊢B=Atrue\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash A = B \; \mathrm{true}}{\Gamma \vdash B = A \; \mathrm{true}}
Γ⊢AtypeΓ⊢a:AΓ⊢b:AΓ⊢a= AbtrueΓ⊢b= Aatrue\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash a =_A b \; \mathrm{true}}{\Gamma \vdash b =_A a \; \mathrm{true}}
Symmetry of typal equality (i.e. inverse function and inverse path)

Γ⊢AtypeΓ⊢BtypeΓ⊢P:A≃BΓ⊢P −1:B≃A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash P:A \simeq B}{\Gamma \vdash P^{-1}:B \simeq A}
Γ⊢AtypeΓ⊢a:AΓ⊢b:AΓ⊢p:a= AbΓ⊢p −1:b= Aa\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b}{\Gamma \vdash p^{-1}:b =_A a}

Transitivity

The transitivity of equality is given by the following judgmental, propositional, and typal rules respectively:

Transitivity of judgmental equality

Γ⊢A=BtypeΓ⊢B=CtypeΓ⊢A=Ctype\frac{\Gamma \vdash A = B \; \mathrm{type} \quad \Gamma \vdash B = C \; \mathrm{type} }{\Gamma \vdash A = C \; \mathrm{type}}
Γ⊢AtypeΓ⊢a=b:Ab=c:AΓ⊢a=c:A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a = b:A \quad b = c:A }{\Gamma \vdash a = c:A}
Transitivity of propositional equality

Γ⊢AtypeΓ⊢BtypeΓ⊢CtypeΓ⊢A=BtrueΓ⊢B=CtrueΓ⊢A=Ctrue\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash A = B \; \mathrm{true} \quad \Gamma \vdash B = C \; \mathrm{true}}{\Gamma \vdash A = C \; \mathrm{true}}
Γ⊢AtypeΓ⊢a:AΓ⊢b:AΓ⊢c:AΓ⊢a= AbtrueΓ⊢b= ActrueΓ⊢a= Actrue\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 =_A b \; \mathrm{true} \quad \Gamma \vdash b =_A c \; \mathrm{true}}{\Gamma \vdash a =_A c \; \mathrm{true}}
Transitivity of typal equality (i.e. composition of functions and path concatenation)

Γ⊢AtypeΓ⊢BtypeΓ⊢CtypeΓ⊢P:A≃BΓ⊢Q:B≃CΓ⊢Q∘P:A≃C\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash P:A \simeq B \quad \Gamma \vdash Q:B \simeq C}{\Gamma \vdash Q \circ P:A \simeq C}
Γ⊢AtypeΓ⊢a:AΓ⊢b:AΓ⊢c:AΓ⊢p:a= AbΓ⊢q:b= AcΓ⊢p•q:a= Ac\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash c:A \quad \Gamma \vdash p:a =_A b \quad \Gamma \vdash q:b =_A c}{\Gamma \vdash p \bullet q:a =_A c}

Principle of substituting equals for equals

The principle of substituting equals for equals is given by the following judgmental, propositional, and typal rules respectively:

Substitution of judgmentally equal terms:

Γ⊢AtypeΓ⊢a=b:AΓ,x:A,Δ⊢BtypeΓ,Δ[b/x]⊢B[a/x]=B[b/x]type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a = b : A \quad \Gamma, x:A, \Delta \vdash B \; \mathrm{type}}{\Gamma, \Delta[b/x] \vdash B[a/x] = B[b/x] \; \mathrm{type}}
Γ⊢AtypeΓ⊢a=b:AΓ,x:A,Δ⊢c:BΓ,Δ[b/x]⊢c[a/x]=c[b/x]:B[b/x]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a = b : A \quad \Gamma, x:A, \Delta \vdash c:B}{\Gamma, \Delta[b/x] \vdash c[a/x] = c[b/x]: B[b/x]}
Substitution of propositionally equal terms:

Γ⊢AtypeΓ⊢a:AΓ⊢b:AΓ⊢a= AbtrueΓ,x:A,Δ⊢BtypeΓ,Δ[b/x]⊢B[a/x]=B[b/x]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, \Delta \vdash B \; \mathrm{type}}{\Gamma, \Delta[b/x] \vdash B[a/x] = B[b/x] \; \mathrm{true}}
Γ⊢AtypeΓ⊢a:AΓ⊢b:AΓ⊢a= AbtrueΓ,x:A,Δ⊢c:BΓ,Δ[b/x]⊢c[a/x]= B[b/x]c[b/x]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, \Delta \vdash c:B}{\Gamma, \Delta[b/x] \vdash c[a/x] =_{B[b/x]} c[b/x] \; \mathrm{true}}
Substitution of typally equal terms (i.e. transport and action on identifications):

Γ⊢AtypeΓ⊢a:AΓ⊢b:AΓ⊢p:a= AbΓ,x:A,Δ⊢BtypeΓ,Δ[b/x]⊢tr(x.B,a,b,p):B[a/x]≃B[b/x]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \quad \Gamma, x:A, \Delta \vdash B \; \mathrm{type}}{\Gamma, \Delta[b/x] \vdash \mathrm{tr}(x.B, a, b, p):B[a/x] \simeq B[b/x]}
Γ⊢AtypeΓ⊢a:AΓ⊢b:AΓ⊢p:a= AbΓ,x:A,Δ⊢c:BΓ,Δ[b/x]⊢ap(c,x.B,a,b,p):tr(x.B,a,b,p)(c[a/x])= B[b/x]c[b/x]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \quad \Gamma, x:A, \Delta \vdash c:B}{\Gamma, \Delta[b/x] \vdash \mathrm{ap}(c, x.B, a, b, p):\mathrm{tr}(x.B, a, b, p)(c[a/x]) =_{B[b/x]} c[b/x]}

Variable conversion

The variable conversion rule is given by the following judgmental, propositional, and typal rules respectively:

Judgmental variable conversion rule:

Γ⊢A=BtypeΓ,x:A,Δ⊢𝒥Γ,x:B,Δ⊢𝒥\frac{\Gamma \vdash A = B \; \mathrm{type} \quad \Gamma, x:A, \Delta \vdash \mathcal{J}}{\Gamma, x:B, \Delta \vdash \mathcal{J}}
Propositional variable conversion rule:

Γ⊢AtypeΓ⊢BtypeΓ⊢A=BtrueΓ,x:A,Δ⊢𝒥Γ,x:B,Δ⊢𝒥\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash A = B \; \mathrm{true} \quad \Gamma, x:A, \Delta \vdash \mathcal{J}}{\Gamma, x:B, \Delta \vdash \mathcal{J}}
Typal variable conversion rule:

Γ⊢AtypeΓ⊢BtypeΓ⊢P:A≃BΓ,x:A,Δ⊢𝒥Γ,y:B,Δ[P −1(y)/x]⊢𝒥[P −1(y)/x]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash P:A \simeq B \quad \Gamma, x:A, \Delta \vdash \mathcal{J}}{\Gamma, y:B, \Delta[P^{-1}(y)/x] \vdash \mathcal{J}[P^{-1}(y)/x]}

𝒥\mathcal{J} is a generic judgment thesis.

Usages of equality

In definitions of types and terms

The three different notions of equality above could be used in definitions of types and terms, as well as in the rules for the single assignment operator ≔\coloneqq. In Martin-Löf type theory and cubical type theory, judgmental equality is used for definitional equality. In ZFC and ETCS, propositional equality is used for definitional equality, and in objective type theories, typal equality is used for definitional equality.

In conversion rules and inductive definitions

The three different notions of equality above could also be used in the conversion rules for the various type formers, such as beta conversion or eta conversion, where the equality is called conversional equality or computational equality. Computational equality is important because it is the equality used in inductive definitions. In Martin-Löf type theory and cubical type theory, judgmental equality is used for computational equality, and in objective type theories, typal equality is used for computational equality.

There are also equalities in type theory which are not internal to the type theory itself, but rather equalities in the metatheory. These include syntactic equality of expressions, as well as alpha-equivalence and definitional equality of syntactical expressions. When using de Bruijn indices, alpha-equivalence is the same as syntactic equality, but when using variables, alpha-equivalence is different from syntactic equality: rather alpha-equivalence is equality up to the renaming of bound variables. All type theories, like MLTT, cubical type theory, ZFC, and ETCS, have syntactic equality, alpha-equivalence, and definitional equality of syntactical expressions, including the type theories which lack judgmental equality like objective type theories.

Equality in constructive and classical mathematics

Constructive mathematics is mathematics in which the law of excluded middle does not necessarily hold for propositions, subsingletons, or h-propositions. Classical mathematics is mathematics in which the law of excluded middle does hold for propositions, subsingletons, or h-propositions. Here, we take equality to mean either typal or propositional equality, so that equality is a relation or a type family on a type or set.

In classical mathematics, equality of sets is a stable equivalence relation, and denial inequality of sets is a tight apartness relation. However, in constructive mathematics, equality cannot be proven to be stable for all sets, and denial inequality cannot be proven to be a tight apartness relation for all sets. Instead, one could distinguish between 4 different notions of equality and inequality:

tight apartness relations . However, not all sets have tight apartness relations. The sets which do are calledinequality spaces?.
equality, which is an equivalence relation ; set withinequality spaces?tight apartness relations have stable equality.
denial inequality, which can only be proven to be a weakly tight irreflexive symmetric relation. However, all statements in classical mathematics involving only denial inequalities hold in constructive mathematics, by the double negation translation and the property that for any proposition PP, ¬¬¬P\neg \neg \neg P if and only if ¬P\neg P.
the double negation of equality, which can only be proven to be a stable reflexive symmetric relation. However, all statements in classical mathematics involving only equality hold in constructive mathematics with the equality replaced by its double negation, by the double negation translation.

The sets in which equality and inequality behaves as it does in classical mathematics are the sets with decidable equality.

As a result, in constructive mathematics, sometimes one takes sets withinequality spaces?tight apartness relations instead of general sets to be the foundational primitive concept. In classical mathematics, this is unnecessary, because every set is has an ainequality space?tight apartness relation.

Internal equality in set theory

Relations and equality could be internalized in any set theory: the internal equality in set theory is the smallest internal reflexive relation on SS, and it is in fact an internal equivalence relation; it is the only internal equivalence relation on SS that is also a partial order (although that fact is somewhat circular). This relation is often called the identity relation on SS, either because ‘identity’ can mean ‘equality’ or because it is the identity for composition of relations.

In the category of reflexive relations on SS, the equality relation on SS is an initial reflexive relation; when the equality relation is a type family instead of a family of propositions, then the equality relation is the initial type generated by reflexivity or the first law of thought.

As a subset of S×SS \times S, the equality relation is often called the diagonal and written Δ S\Delta_S or similarly. As an abstract set, this subset is isomorphic to SS itself, so one also sees the diagonal as a map, the diagonal function S→Δ SS×SS \overset{\Delta_S}\to S \times S, which maps xx to (x,x)(x,x); note that x=xx = x. This is in Set; analogous diagonal morphisms exist in any cartesian monoidal category.

−\phantom{-}symbol−\phantom{-}	−\phantom{-}in logic−\phantom{-}
A\phantom{A}∈\in	A\phantom{A}element relation
A\phantom{A}:\,:	A\phantom{A}typing relation
A\phantom{A}==	A\phantom{A}equality
A\phantom{A}⊢\vdashA\phantom{A}	A\phantom{A}entailment / sequentA\phantom{A}
A\phantom{A}⊤\topA\phantom{A}	A\phantom{A}true / topA\phantom{A}
A\phantom{A}⊥\botA\phantom{A}	A\phantom{A}false / bottomA\phantom{A}
A\phantom{A}⇒\Rightarrow	A\phantom{A}implication
A\phantom{A}⇔\Leftrightarrow	A\phantom{A}logical equivalence
A\phantom{A}¬\not	A\phantom{A}negation
A\phantom{A}≠\neq	A\phantom{A}negation of equality / apartnessA\phantom{A}
A\phantom{A}∉\notin	A\phantom{A}negation of element relation A\phantom{A}
A\phantom{A}¬¬\not \not	A\phantom{A}negation of negationA\phantom{A}
A\phantom{A}∃\exists	A\phantom{A}existential quantificationA\phantom{A}
A\phantom{A}∀\forall	A\phantom{A}universal quantificationA\phantom{A}
A\phantom{A}∧\wedge	A\phantom{A}logical conjunction
A\phantom{A}∨\vee	A\phantom{A}logical disjunction

symbol	in type theory (propositions as types)
A\phantom{A}→\to	A\phantom{A}function type (implication)
A\phantom{A}×\times	A\phantom{A}product type (conjunction)
A\phantom{A}++	A\phantom{A}sum type (disjunction)
A\phantom{A}00	A\phantom{A}empty type (false)
A\phantom{A}11	A\phantom{A}unit type (true)
A\phantom{A}==	A\phantom{A}identity type (equality)
A\phantom{A}≃\simeq	A\phantom{A}equivalence of types (logical equivalence)
A\phantom{A}∑\sum	A\phantom{A}dependent sum type (existential quantifier)
A\phantom{A}∏\prod	A\phantom{A}dependent product type (universal quantifier)

symbol	in linear logic
A\phantom{A}⊸\multimapA\phantom{A}	A\phantom{A}linear implicationA\phantom{A}
A\phantom{A}⊗\otimesA\phantom{A}	A\phantom{A}multiplicative conjunctionA\phantom{A}
A\phantom{A}⊕\oplusA\phantom{A}	A\phantom{A}additive disjunctionA\phantom{A}
A\phantom{A}&\&A\phantom{A}	A\phantom{A}additive conjunctionA\phantom{A}
A\phantom{A}⅋\invampA\phantom{A}	A\phantom{A}multiplicative disjunctionA\phantom{A}
A\phantom{A}!\;!A\phantom{A}	A\phantom{A}exponential conjunctionA\phantom{A}
A\phantom{A}?\;?A\phantom{A}	A\phantom{A}exponential disjunctionA\phantom{A}

References

Georg Hegel, Science of Logic, 1812

equality is the subject of volume 1, book 2 “Die Lehre vom Wesen” (The doctrine of essence). As discussed at Science of Logic, one can roughly identify in Hegel’s text there the notion of intensional identity and of the reflector term in identity types.

Texts on type theory typically deal with the subtleties of the notion of equality. For instance

Per Martin-Löf, Intuitionistic type theory, Lecture notes (1980)

Besides

Kurt Gödel, Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica (1958), pp. 280–287,

which might be the first paper to mention intensional equality (and the fact that it should be decidable), there is

Nicolaas de Bruijn, Automath,

where de Bruijn makes a distinction between definitional equality and “book” equality.

Kevin Buzzard, Grothendieck’s use of equality (arXiv:2405.10387)

Last revised on January 17, 2025 at 17:05:44. See the history of this page for a list of all contributions to it.

equality (changes) in nLab

Context

Equality and Equivalence

Foundations

The basis of it all

Set theory

Foundational axioms

Removing axioms

Contents

Idea