Discreteness

Definition

Discreteness in constructive mathematics refers to decidable equality. It is the property that any two elements of a type can be computationally distinguished or identified in finite time.

Formal Statement

A type $A$ is discrete if: ${\Pi }_{(x,y:A)}((x=y)\uplus \neg (x=y))$

Properties

1. Strictness: This is a much stronger condition than merely being a set.
2. Hedberg’s Theorem: If a type has decidable equality, it is necessarily a set (an hSet). $\text{Discrete}(A)\to \text{isSet}(A)$
3. Examples:
   • $\mathbb{N}$, $\mathbb{Z}$, and finite types are discrete.
   • $\mathbb{R}$ (Real Numbers) is not discrete. We cannot decide if a computed real number equals $0$ in finite time.

References

• hedberg1998-coherence
• kraus2013-hedberg