Homotopy Type Theory Dedekind real numbers > history (Rev #5)

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 cuts on the rational numbers \mathbb{Q} in a universe: 𝒰DedekindCut 𝒰()\mathbb{R}_\mathcal{U} \coloneqq DedekindCut_\mathcal{U}(\mathbb{Q}).

Sigma-Dedekind real numbers

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

See also

References

Revision on April 22, 2022 at 21:38:13 by Anonymous?. See the history of this page for a list of all contributions to it.