Homotopy Type Theory Dedekind real closed intervals > history (changes)

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

<Dedekind cut

Definitions

Large Dedekind real closed intervals

The 𝒰\mathcal{U}-large Dedekind real closed intervals for a universe 𝒰\mathcal{U} is defined as the type of 𝒰\mathcal{U}-interval cuts on the rational numbers \mathbb{Q} in a universe: 𝒰IntervalCut 𝒰()\mathbb{R}_\mathcal{U} \coloneqq IntervalCut_\mathcal{U}(\mathbb{Q}).

Sigma-Dedekind real closed intervals

The Σ\Sigma-Dedekind real closed intervals for a $\sigma$-frame Σ\Sigma is defined as the type of Σ\Sigma-interval cuts on the rational numbers \mathbb{Q}: ΣIntervalCut Σ()\mathbb{R}_\Sigma \coloneqq IntervalCut_\Sigma(\mathbb{Q}).

See also

Last revised on June 10, 2022 at 15:05:23. See the history of this page for a list of all contributions to it.