## Definitions ## ### Locally $\mathcal{U}$-small Dedekind real numbers ### The **locally $\mathcal{U}$-small Dedekind real numbers** for a [[universe]] $\mathcal{U}$ is defined as the [[Archimedean ordered integral domain]] $\mathbb{R}_\mathcal{U}$ with a [[strictly monotonic function]] $i:\mathbb{I}_\mathcal{U} \to \mathbb{R}_\mathcal{U}$ from the locally $\mathcal{U}$-small [[Dedekind real unit interval]] to $\mathbb{R}_\mathcal{U}$ such that $i(0) = 0$ and $i(1) = 1$. ## See also ## * [[real numbers]] * [[Dedekind cut]]s * [[Dedekind cut structure real numbers]] * [[Dedekind real closed intervals]] * [[Dedekind real numbers (disambiguation)]] * [[axiom R-flat]] * [[contractibility of Dedekind real numbers]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013) * Auke B. Booij, Extensional constructive real analysis via locators, ([abs:1805.06781](https://arxiv.org/abs/1805.06781))