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

Dedekind real numbers

The Dedekind real numbers for a universe $\mathcal{U}$ is defined as the type of Dedekind cuts on the rational numbers $\mathbb{Q}$ in a universe:

$\mathbb{R}_\mathcal{U} \coloneqq DedekindCut_\mathcal{U}(\mathbb{Q})$

See also

• real numbers
• Dedekind cuts
• Dedekind real numbers (disambiguation)