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
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.