## Definitions ## 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 ## * [[Dedekind real unit interval]] * [[real numbers]] * [[axiom R-flat]] * [[contractibility of Dedekind real numbers]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)