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

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

## Definitions

### Large Dedekind real unit interval

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

The $\mathcal{U}$-large Dedekind real numbers 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})$.

### Sigma-Dedekind real unit interval

The $\Sigma$-Dedekind real numbers for a $\sigma$-frame $\Sigma$ is defined as the type of extended $\Sigma$-Dedekind cuts on the open unit interval of the rational numbers $(0, 1)_\mathbb{Q}$: $\mathbb{I}_\Sigma \coloneqq ExtendedDedekindCut_\Sigma((0, 1)_\mathbb{Q})$.