## 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]]. ## See also ## * [[contractibility of Dedekind real numbers]] * [[Dedekind real numbers]] * [[intermediate value theorem]] ## References ## * [[Mike Shulman]], Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 ([arXiv:1509.07584](https://arxiv.org/abs/1509.07584), [doi:10.1017/S0960129517000147](https://doi.org/10.1017/S0960129517000147))