## Definitions ## The **locally $\mathcal{U}$-small Dedekind real unit interval** for a [[universe]] $\mathcal{U}$ is defined as the type of [[extended Dedekind cut|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})$. ## See also ## * [[Dedekind real numbers]] * [[extended Dedekind cut]]s * [[axiom I-flat]] * [[contractibility of Dedekind real unit interval]]