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

Showing changes from revision #6 to #7: Added | Removed | Changed

## Definitions

### Axiomatic Locally definiton$\mathcal{U}$-small Dedekind real numbers

The Dedekind real numbers is aDedekind complete Archimedean ordered fieldlocally $\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$.

### Large Dedekind real numbers

The $\mathcal{U}$-large Dedekind real numbers for a universe $\mathcal{U}$ is defined as the type of $\mathcal{U}$-Dedekind cuts on the rational numbers $\mathbb{Q}$ in a universe: $\mathbb{R}_\mathcal{U} \coloneqq DedekindCut_\mathcal{U}(\mathbb{Q})$.

### Sigma-Dedekind real numbers

The $\Sigma$-Dedekind real numbers for a $\sigma$-frame $\Sigma$ is defined as the type of $\Sigma$-Dedekind cuts on the rational numbers $\mathbb{Q}$: $\mathbb{R}_\Sigma \coloneqq DedekindCut_\Sigma(\mathbb{Q})$.