Showing changes from revision #6 to #7:
Added | Removed | Changed
Disambiguation page <Dedekind real numbers
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:
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.