Equality

Equality

We can distinguish different strengths of equality:

• intensional equality: it equates programs which evaluate the same by beta-reduction (and iota, delta, zeta, fix, cofix, ...); it generally generates a confluent rewriting system (w/o critical pairs)
• eta-equality: it equates programs which observationally behave the same; it is decidable in the finite types (e.g. on boolean, on finite products), but it is undecidable in the infinite cases (e.g., on natural numbers, on streams, ...); actually, the undecidability of eta-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; it is unclear whether we can canonically associate to higher-inductive types an eta-equality but it would suspectingly be undecidable for most of them (starting with the circle)
• extensional equality (also called observational equality) coincides with eta-equality on positive types (such as sums, products, Boolean, ...) but not in the case of functions or types:
  • in the case of functions, it is pointwise equality and it is equivalent to eta for functions + the ξ-rule which says that x ⊢ t = u implies ⊢ λx.t = λx.u
  • in the case of types, equality is equivalence (in the HoTT sense).

A few properties of an equality:

• an equality is strict if any two proofs of equality are necessarily themselves equal (see UIP or axiom K)
• 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).

The structure of equality proofs gives rise to:

• "homotopic" equality, also called weak equality in the context of category theory: it is an equality which supports a rich algebraic structure of equality of equality proofs, and of equality of proofs of equality proofs, 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 definitional equality, which consists in defining the "meaning" of non-constructor operators, as in β-reduction which can be thought as "defining" application as the operation which replaces the parameter of a function by its actual argument (λa.t)u → t[a:=u], or as in ɩ-reduction which can be thought as "defining" case analysis as the operation that actually selects a branch match true with true => t | false => u end → t and match false with true => t | false => u end → u, or as in δ-reduction which reduces a constant to its definition; definitional equality plays then the rôle of a computational equality, both rich enough and minimal enough to ensure that any closed expression can be canonically reduced to a weak-head normal form; definitional equality is thus generated by congruent-reflexive-symmetric-transitive closure from a reduction relation which is typically written → or ▹ in papers
    • it can also extend definitional 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 Agda extended with rewriting rules, ...)

• 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, to make things more confused, it is written t ≣ u in Agda!

In another direction, we can make a difference between:

• an 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
• cubical equality (also called path equality in the context of cubical type theory, also called sometimes equality over in a categorical context) is an equality between objects in types which are themselves provably equal
• heterogeneous equality (aka John Major equality) was an equality useful in type theory to compare objects in non judgementally equal types; in practice, the types are often nevertheless provably equal (as e.g. in vec (n+m) = vec (m+n)) and it has the drawback that it has to be strict (i.e. it requires UIP); so, in my opinion, John Major equality is nowadays advantageously replaced by cubical equality, which is also an heterogeneous equality.