Abstract
What does the sign " equals " mean in a computer program ? in a mathematicaltext ? The first precise definition of equality, attributed to Leibniz, says that x and y are equal if and only if they satisfy the same properties : ∀P, P(x) ⇔ P(y). This definition is equivalent to other more recent definitions, in first-order logic or set theory, as well as to the type-theoretic definition introduced by Martin-Löf in 1973. This is presented as a type x = A y of identities (proofs of equality) between x : A and y : A, a constructor which is the axiom of reflexivity, and an eliminator which is the law of replacement between equals.
Martin-Löf equality, or its reformulation as an inductive predicate in Coq, is perfect for reasoning about first-order types such as integers, but poses some difficulties on richer types. In particular, we can't show that two point-to-point equal functions are equal, nor that two identities between x and y are equal. This leads many Coq developments to add as axioms the extensionality of functions and the uniqueness of identities.
A new perspective on equality in type theory is provided by homotopy theory in algebraic topology and its extension to the higher order : the ω-groupoid structure. We can interpret identities as paths and identities between identities as homotopies between paths. Based on this homotopic and categorical inspiration, Voevodsky, Avodey, Coquand and others have, since 2005, developed HomotopyType Theory (HoTT), a variant of type theory in which equality plays a central role. HoTT defines logical propositions as types where all elements are equal to each other, and sets as types where equality is a proposition. HoTT also introduces new tools : propositional truncation, quotient types, higher-order inductive types, which open up new possibilities in both mathematical logic and type programming.
