Disambiguation page There are many different types which are called Dedekind real numbers in the literature. All of them involve the use of [[Dedekind cut (disambiguation)|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|$\sigma$-frame]], such as the type of propositions in a universe or [[Sierpinski space]]: * [[Dedekind real numbers]] * [[Dedekind cut structure real numbers]] * [[Dedekind real closed intervals]], where the Dedekind real numbers are the located Dedekind real closed intervals, and the Dedekind cut structure real numbers are the Dedekind real closed intervals with a [[locator]]. ## See also ## * [[real numbers]] for other types of real numbers ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013) * Auke B. Booij, Extensional constructive real analysis via locators, ([abs:1805.06781](https://arxiv.org/abs/1805.06781)) * Mark Bridger, [Real Analysis: A Constructive Approach Through Interval Arithmetic](https://bookstore.ams.org/amstext-38), Pure and Applied Undergraduate Texts 38, American Mathematical Society, 2019.