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