Equality

Equality

We can distinguish different strengths of equality:

• Syntactic equality: it is the finest notion of equality corresponding to the identity of representation of terms in their abstract syntax.

  Note that historically, terms using different names for binders, e.g. fun x => x and fun y => y, were not considered syntactically equal but only α-equal, where α-equality is the notion of equality that equates terms up to the names used in binders. Nowadays, a distinction is made between abstract syntax, where binders are canonically represented (e.g. using de Bruijn indices) and concrete syntax, where names are used as a notation for human readability, and only for human readability.

• Intensional equality: it equates programs which evaluate the same by β-reduction (and ɩ, δ, 𝛇, fix, cofix, ...); it is generated by the congruent-reflexive-symmetric-transitive closure of a confluent rewriting system (w/o critical pairs).

  It is also called definitional equality [Tait98] as it can be seen as defining the "meaning" of the elimination rule of the type (see Martin-Löf's meaning explanation). For instance, the β-reduction (λa.t)u → t[a:=u] can be thought as "defining" application while ɩ-reduction, e.g. match true with true => t | false => u end → t and match false with true => t | false => u end → u in the case of Booleans, can be thought as "defining" case analysis. On its side, δ-reduction reduces a constant to its definition, and 𝛇-reduction defining the meaning of a let. Finally, fix and cofix can be seen as defining the meaning of a recursion and corecursion. Intensional equality is a computational equality, it ensures that any closed expression can be canonically reduced to a weak-head normal form.

  The reduction generating intensional equality is typically written → or ▹ in papers.

• η-equality tells how types are canonically inhabited and its formulation depends on the polarity of the type.

  In negative types (such as the type of dependent functions, the type of tuples, and coinductive types), it ensures a canonical form to the inhabitants of the type. E.g. η for functions says that any function t is equal to a function of the form fun x => ..., namely the function fun x => t x. Also, η for pairs says that any inhabitant t of a product type takes the syntactic form of a pair (..., ...), namely the pair (fst t, snd t).

  In positive types (such as Boolean, natural numbers, disjunction, and more generally all inductive types), it ensures a canonical form to the contexts in which an inhabitant of the type is used. E.g., η for Booleans says that any computation E[t] made of a context E filled with a Boolean t is canonically equal to a computation if t then E[true] else E[false] that first starts to analyze the form of the Boolean.

  The congruent-reflexive-symmetric-transitive of η implies that terms in negative types are equal if they are equal observationally. E.g., in the case of tuples, it says that t is equal to u iff (fst t, snd t) is equal to (fst u, snd u) that is iff fst t is equal to fst u and snd t is equal to snd u. In the case of functions, it says that f is equal to g iff fun x => f x is equal to fun x => g x, that is iff f x is equal to g x in a context extended with x.

  In positive types, it says that two terms E[t] and E'[t] depending on a common subterm t are equal when match t with ... C x1...xn => E[C x1...xn] ... end and match t with ... C x1...xn => E'[C x1...xn] ... end are equal, that is when E[C x1...xn] is equal to E'[C x1...xn] for all possible forms C x1...xn taken by a case analysis on t.

  In the context of type theory, η is decidable in finite record types and conjectured decidable on booleans, but it is undecidable in infinite types (e.g., on natural numbers, on streams, ...), because it would require unfolding recursion arbitrarily often; actually, the undecidability of η-equality is the very reason why proofs are not machine-inferrable in general, otherwise, any statement would be checkable just by testing that it is true on all inputs.

  The decidability of η for the empty type is undecidable in full generality. Indeed, η-equality for False says that u is equal to match t with end for any proof t of False. Taking its congruent-reflexive-symmetric-transitive implies that u is equal to v whenever a proof t of False is known, which is undecidable. However, we can design an algorithm that decides a subset of η for False that equates any two terms such at least one of the two terms has a subterm proving False (instead of the more demanding expectation of the existence of an arbitrary proof of False).

  Regarding higher inductive types, it is unclear whether we can canonically associate an η-equality but it would suspectingly be undecidable for most of them (starting with the circle).

• Extensional equality (also called observational equality) extends η-equality with specific rules which characterize the maximal congruence in a type that cannot be contradicted:

  • in the case of functions, function extensionality extends η for functions with the ξ-rule which says that x ⊢ t = u implies ⊢ λx.t = λx.u, that is (∀ x, t(x) = u(x)) → λx.t = λx.u,
  • in the case of types, univalence, also called type extensionality, is equivalence of types (the corresponding axiom for propositions, that is for proof-irrelevant types, is traditionally known as Propositional extensionality),
  • in the case of the equality type, the uniqueness of identity proofs (UIP) can also be seen as a form of extensionality.

  Note that the largest equality on types, namely equivalence, is contradictory with the largest equality on equalities, namely UIP, resulting in two radically different incompatible views at observational equality. On the contrary, function extensionality is compatible with both either univalence or UIP.

  Note also that on covariant types (such as sums, products, Boolean, records, ...), η-equality already brings full extensionality, that is the largest possible equality on elements of the type.

A few properties of an equality:

• An equality is strict if any two proofs of equality are necessarily themselves equal (see UIP, which can be seen as stating a form of extensionality of equality).
• An equality is non-strict (or relevant) if there are provably disjoint proofs of equality of the same equality; this is typically the case of equality in the presence of univalence (= extensionality of types), since then, there are two distinct proofs of Bool = Bool (the identity and the negation on Boolean values).

The structure of equality proofs gives rise to:

• "Homotopic" equality, also called weak equality in the context of category theory, or path in the context of geometry: it is an equality which supports a rich algebraic structure of equality of proofs of equality, and of equality of proofs of equality of proofs of equality, etc.; in practice, from a syntactic point of view, we have actually no other choice than to work with a "homotopic" equality, because, in a syntactic view, the reflexivity, or symmetry, or transitivity of equality proofs are terms themselves, and trans p (trans q r) is syntactically different from trans (trans p q) r and we need to write an explicit proof term of the equality of trans p (trans q r) = trans (trans p q) r, and recursively, and there are different provably equal but not syntactically equal proofs of this latter statement. So, what really matters is whether the equality up to equality (and recursively in further nestings of equality) is strict or not, and if strict, whether there is a decidable subset of it that could be managed automatically at the meta-level in a proof assistant.

There are also interactions between the equality of a theory as a proposition and the (meta)equality of the metatheory:

• Judgemental equality, in the context of Martin-Löf's type theory, also called conversion in the context of Pure Type Systems, also called "equality on the nose" in the context of set theory is used to quotient terms and types at the metalevel by a subset of strict equality. It is often written ≣ in theoretical papers (thought sometimes it is also written =). It can be typed or not, decidable or not:

  • in practice, the terminology "judgemental" is generally used when it is typed and when decidability does not care,
  • the terminology "conversion" is generally used when it is untyped and decidable (as in Coq).

  Its extent can also vary:

  • it can coincide with strict equality, as in so-called Extensional Type Theory (as e.g. in NuPrl or Andromeda, but to some extent, this is also an extensional equality which we find in set theory, even if it has no nested dependency and proofs of equality are thus invisible anyway),
  • or it can cover only a decidable subset of strict equality (as is the case for Coq, basic Agda, ...)
    • it is expected to include at least intensional equality,
    • it can also extend intensional equality with observational properties, such as η-reduction, one for each type constructor, which remains decidable as long as the type is finitely described,
  • or it can include a larger decidable subset of strict equality, as in the Calculus of Algebraic Constructions (see also CoqMT or the extension of Agda and Coq with rewriting rules, ...).

  Judgemental equality is sometimes also called definitional equality. This is justified when it has the strength of intensional equality. To some extent, this is also justified when it includes η-equality, in the sense that η-equality is part of the characterization of a connective, as much as β-equality is, even if η-equality is not needed to compute.

  Note that judgemental equality generally includes the ξ-rule and it thus satisfies function extensionality.

• By contrast, equality as a connective is called propositional (and, of course, it includes the judgemental quotient); in Coq, it is written t = u (or t = u :> A) while, be careful on the confusion it can induce, it is written t ≣ u in Agda.

  The term propositional is actually disputable in the general context of type theory, as the proofs of an equality are sometimes relevant, as it is the case in Homotopy Type Theory in the presence of univalence of higher inductive types. Shulman proposed the term typical equality as an alternative to propositional equality to include the case where the inhabitants of the equality connective are informative.

  In Coq, none of function extensionality, type extensionality, and uniqueness of identity proofs hold by default.

In another direction, we can make a difference between:

• Homogeneous equality (also called globular since it corresponds to a globular shape in geometry) which is when the comparison is between objects of the same type.

• Heterogeneous equality (also called cubical since it corresponds to a cubical shape in geometry) which is when the comparison is between objects whose types are themselves provably equal. It is also sometimes called cubical path, or equality over, or fibered equality. If the two types are of the form P a and P a', for P a family of types, together with a proof of a = a', it is also called dependent pair equality.

  If p is a proof of A = B and a and b are of types A and B respectively, it is equivalent to the equality in A of a with the "transport" of b from type B to type A along p (that is the replacement of the type B of b by A thanks to p : A = B), or symmetrically, to the equality in B of b and of a transported from B to A along p.

  If, moreover, the heterogeneous equality of a and a' when both a and a' are in A implies the homogeneous equality of a and a' then, the heterogeneous equality is commonly referred to as John Major equality. The latter property is equivalent to UIP and thus implies a strict equality.

[Tait98] Variable-free formalization of the Curry-Howard Theory of Types

See also ncatlab's equality page.