Homotopy Type Theory Dedekind real closed intervals > history (Rev #3, changes)

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

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: $\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}$: $\mathbb{R}_\Sigma \coloneqq IntervalCut_\Sigma(\mathbb{Q})$.