# Homotopy Type Theory Dedekind real numbers > history (Rev #9, changes)

Showing changes from revision #8 to #9: Added | Removed | Changed

## 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$.

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$.

## References

Revision on June 10, 2022 at 11:41:04 by Anonymous?. See the history of this page for a list of all contributions to it.