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

Showing changes from revision #4 to #5: Added | Removed | Changed

Disambiguation page

There are many different types which are called Dedekind real numbers in the literature. All of them involve the use of Dedekind cuts in a dense integral subdomain of the rational numbers in their definition, and they differ based upon which definitions of a Dedekind cut are used.

The following real number types are defined using a $\sigma$-frame, such as the type of propositions in a universe or Sierpinski space:

• Dedekind real numbers
• Dedekind cut structure real numbers
• rational closed intervals, where the Dedekind real numbers are the located rational closed intervals, and the Dedekind cut structure real numbers are the rational closed intervals with a locator.

See also

• real numbers for other types of real numbers

References

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

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

• Mark Bridger, Real Analysis: A Constructive Approach Through Interval Arithmetic, Pure and Applied Undergraduate Texts 38, American Mathematical Society, 2019.