Homotopy Type Theory Dedekind cut structure real numbers > history (Rev #2)

Dedekind cut structure real numbers

Large Dedekind cut structure real numbers

The $\mathcal{U}$-large Dedekind cut structure real numbers for a universe $\mathcal{U}$ is defined as the type of all pairs of subtypes of the rational numbers $\mathbb{Q}$ which have a $\mathcal{U}$-Dedekind cut structure:

Sigma-Dedekind cut structure real numbers

The $\Sigma$-Dedekind cut structure real numbers for a $\sigma$-frame $\Sigma$ is defined as the type of all pairs of open subtypes of the rational numbers $\mathbb{Q}$ which have a $\Sigma$-Dedekind cut structure:

See also

• real numbers
• Dedekind cut structure
• Dedekind real numbers
• rational closed intervals
• Dedekind real numbers (disambiguation)

References

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

• Auke B. Booij, Extensional constructive real analysis via locators, (abs:1805.06781)