Homotopy Type Theory Dedekind real unit interval > history (Rev #2, changes)

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

Definitions

Large Dedekind real unit interval

The locally 𝒰\mathcal{U}-small Dedekind real unit interval for a universe 𝒰\mathcal{U} is defined as the type of extended $\mathcal{U}$-Dedekind cuts on the open unit interval of the rational numbers (0,1) (0, 1)_\mathbb{Q} in a universe: 𝕀 𝒰ExtendedDedekindCut 𝒰((0,1) )\mathbb{I}_\mathcal{U} \coloneqq ExtendedDedekindCut_\mathcal{U}((0, 1)_\mathbb{Q}).

The 𝒰\mathcal{U}-large Dedekind real numbers for a universe 𝒰\mathcal{U} is defined as the type of extended $\mathcal{U}$-Dedekind cuts on the open unit interval of the rational numbers (0,1) (0, 1)_\mathbb{Q} in a universe: 𝕀 𝒰ExtendedDedekindCut 𝒰((0,1) )\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 is defined as the type of extended $\Sigma$-Dedekind cuts on the open unit interval of the rational numbers (0,1) (0, 1)_\mathbb{Q}: 𝕀 ΣExtendedDedekindCut Σ((0,1) )\mathbb{I}_\Sigma \coloneqq ExtendedDedekindCut_\Sigma((0, 1)_\mathbb{Q}).

See also

Revision on June 10, 2022 at 17:14:25 by Anonymous?. See the history of this page for a list of all contributions to it.