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]]s 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 the type of all propositions in a universe, so that the real number types form a (large) [[frame]] (in the next [[universe]] in the hierarchy): * [[two-sided Dedekind real number]] * [[lower Dedekind real number]] * [[upper Dedekind real number]] * [[two-sided extended Dedekind real number]] * [[lower extended Dedekind real number]] * [[upper extended Dedekind real number]] * [[two-sided Dedekind cut structure real number]] * [[lower Dedekind cut structure real number]] * [[upper Dedekind cut structure real number]] * [[two-sided extended Dedekind cut structure real number]] * [[lower extended Dedekind cut structure real number]] * [[upper extended Dedekind cut structure real number]] The following real number types are defined as above but uses [[Sierpinski space]] instead of the type of all prepositions in a universe to define Dedekind cuts, so that the real number types form a [[sigma-frame|$\sigma$-frame]] in the same universe rather than a large frame in the next universe in the hierarchy. * [[two-sided sigma-Dedekind real number]] * [[lower sigma-Dedekind real number]] * [[upper sigma-Dedekind real number]] * [[two-sided extended sigma-Dedekind real number]] * [[lower extended sigma-Dedekind real number]] * [[upper extended sigma-Dedekind real number]] * [[two-sided sigma-Dedekind cut structure real number]] * [[lower sigma-Dedekind cut structure real number]] * [[upper sigma-Dedekind cut structure real number]] * [[two-sided extended sigma-Dedekind cut structure real number]] * [[lower extended sigma-Dedekind cut structure real number]] * [[upper extended sigma-Dedekind cut structure real number]] ## 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))