Disambiguation page 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. These include: * [[two-sided Dedekind real numbers]], which is defined using Dedekind cuts, which are defined using the type of all prepositions in a universe. * [[lower Dedekind real numbers]], which is defined using only lower Dedekind cuts. * [[upper Dedekind real numbers]], which is defined using only upper Dedekind cuts. * The following types are defined as above but uses [[Sierpinski space]] instead of the type of all prepositions in a universe to define Dedekind cuts: * [[predicative two-sided Dedekind real numbers]] * [[predicative lower Dedekind real numbers]] * [[predicative upper Dedekind real numbers]] * The following types are defined as above but the Dedekind cuts are structure rather than mere property: * [[two-sided Dedekind cut structure real numbers]] * [[lower Dedekind cut structure real numbers]] * [[upper Dedekind cut structure real numbers]] * [[predicative two-sided Dedekind cut structure real numbers]] * [[predicative lower Dedekind cut structure real numbers]] * [[predicative upper Dedekind cut structure real numbers]] ## See also ## * [[real numbers]] for other types of real numbers ## References ## [[HoTT book]] * Auke B. Booij, Extensional constructive real analysis via locators, ([abs:1805.06781](https://arxiv.org/abs/1805.06781))