## Dedekind cut structure real numbers ## ### Large Dedekind cut structure real numbers ### The **$\mathcal{U}$-large Dedekind cut structure real numbers** for a [[universe]] $\mathcal{U}$ is defined as the type of all pairs of subtypes of the [[rational numbers]] $\mathbb{Q}$ which have a $\mathcal{U}$-[[Dedekind cut structure]]: $$\mathbb{R}_\mathcal{U} \coloneqq \sum_{(L, R):Sub_\mathcal{U}(\mathbb{Q}) \times Sub_\mathcal{U}(\mathbb{Q})} \left[DedekindCutStructure_\mathcal{U}(L, R)\right]$$ ### Sigma-Dedekind cut structure real numbers ### The **$\Sigma$-Dedekind cut structure real numbers** for a [[sigma-frame|$\sigma$-frame]] $\Sigma$ is defined as the type of all pairs of open subtypes of the [[rational numbers]] $\mathbb{Q}$ which have a $\Sigma$-[[Dedekind cut structure]]: $$\mathbb{R}_\Sigma \coloneqq \sum_{(L, R):(\mathbb{Q} \to \Sigma) \times (\mathbb{Q} \to \Sigma)} \left[DedekindCutStructure_\Sigma(L, R)\right]$$ ## See also ## * [[real numbers]] * [[Dedekind cut structure]] * [[Dedekind real numbers]] * [[Dedekind real closed intervals]] * [[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))