# Homotopy Type Theory axiom R-flat > history (changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

## Definition

Axiom

$\mathbb{R}\flat$: For a space $A$, $A$ is discrete if and only if for every universe $\mathcal{U}$ and every locally $\mathcal{U}$-small Dedekind real numbers $\mathbb{R}_\mathcal{U}$, the function $const: A \to (\mathbb{R}_\mathcal{U} \to A)$ is an equivalence.