decidable equality


Equality and Equivalence


Decidable and stable equality


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.



In fact, these examples come close to to exhausting the sets than can be proven to have decidable equality in intuitionistic logic; by BauerSwan18 there is a topos (the function realizability topos, which moreover satisfies countable choice, Markov's principle, and other axioms) in which all sets with decidable equality are countable (admit a surjection from a decidable subset of \mathbb{N}). More precisely, although the statement “all sets with decidable equality are countable” is not true in? that topos, every global object with decidable equality in that topos is countable.


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 constructively 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).