nLab
decidable equality

Context

Equality and Equivalence

Foundations

Decidable and stable equality

Definitions

In constructive mathematics, a set XX has decidable equality if any two elements of XX are either equal or not equal. Equivalently, XX has decidable equality if its equality relation is a decidable subset of X×XX \times X. Sometimes one says that such a set XX is discrete, although of course this term has many meanings. Of course, in classical mathematics, every set has decidable equality. But the concept generalises in topos theory to the notion of decidable object.

More generally, XX has stable equality if any two elements of XX are equal if (hence iff) they are not not equal. Every set with decidable equality must also have stable equality, but not conversely.

Applications

Working with decidable subsets of sets with decidable equality makes constructive mathematics very much like classical mathematics. This is why constructivism has few consequences for basic combinatorics and algebra (although it does have important consequences for more advanced topics in those fields). In analysis, in contrast, constructivism matters right away, because the set of real numbers may not have decidable equality. (However, the set of located real numbers does have stable equality.)

In type theory

In type-theoretic foundations, the notion of decidable equality is slightly different depending on whether “or” is interpreted using propositions as types or propositions as some types. That is, decidable equality for AA could be either of the two types

Decidable1(A) x,y:A(x=y)+¬(x=y) Decidable2(A) x,y:A[(x=y)+¬(x=y)] \begin{aligned} Decidable1(A) &\coloneqq \prod_{x,y\colon A} (x=y) + \neg (x=y)\\ Decidable2(A) &\coloneqq \prod_{x,y\colon A} [(x=y) + \neg (x=y)] \end{aligned}

where [][-] denotes a bracket type. Since every type maps to its bracket, Decidable1(A)Decidable1(A) implies Decidable2(A)Decidable2(A).

On the other hand, if Decidable2(A)Decidable2(A) holds and AA is an h-set, i.e. it satisfies uniqueness of identity proofs, then (x=y)(x=y) and ¬(x=y)\neg (x=y) represent disjoint subobjects of A×AA\times A. Thus (x=y)+¬(x=y)(x=y) + \neg (x=y) is already a subobject of A×AA\times A, so it is equivalent to its bracket, and Decidable1(A)Decidable1(A) also holds.

The converse of this is also true: if Decidable1(A)Decidable1(A) holds, then not only does Decidable2(A)Decidable2(A) also hold, but in fact AA is an h-set. This was first proven by Michael Hedberg; a proof can be found at h-set and in the references below. This fact is useful in homotopy type theory to show that many familiar types, such as the natural numbers, are h-sets.

For non-h-sets, the difference between Decidable1Decidable1 and Decidable2Decidable2 can be dramatic. For instance, if we model homotopy type theory in a Boolean (,1)(\infty,1)-topos (such as Gpd\infty Gpd constructed classically), then every type satisfies Decidable2Decidable2 (which is what it means for the logic to be boolean), but only the h-sets satisfy Decidable1Decidable1 (in accordance with Hedberg's theorem).

References

  • Michael Hedberg, A coherence theorem for Martin-Löf’s type theory, J. Functional Programming, 1998

  • Nicolai Kraus, A direct proof of Hedberg’s theorem, blog post

Revised on September 18, 2012 21:40:19 by Urs Schreiber (82.169.65.155)