## Definitions ## ### Axiomatic definiton ## The Dedekind real numbers is a [[Dedekind complete Archimedean ordered field]]. ### 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 cut]]s 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$-frame]] $\Sigma$ is defined as the type of $\Sigma$-[[Dedekind cut]]s on the [[rational numbers]] $\mathbb{Q}$: $\mathbb{R}_\Sigma \coloneqq DedekindCut_\Sigma(\mathbb{Q})$. ## See also ## * [[real numbers]] * [[Dedekind cut]]s * [[Dedekind cut structure real numbers]] * [[Dedekind real numbers (disambiguation)]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013) * Auke B. Booij, Extensional constructive real analysis via locators, ([abs:1805.06781](https://arxiv.org/abs/1805.06781))