# Homotopy Type Theory Dedekind real unit interval > history (changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

## Definitions

The

locally $\mathcal{U}$-small Dedekind real unit interval for a universe $\mathcal{U}$ is defined as the type of extended $\mathcal{U}$-Dedekind cuts on the open unit interval of the rational numbers $(0, 1)_\mathbb{Q}$ in a universe: $\mathbb{I}_\mathcal{U} \coloneqq ExtendedDedekindCut_\mathcal{U}((0, 1)_\mathbb{Q})$.