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]] ## 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))