Showing changes from revision #2 to #3:
Added | Removed | Changed
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.
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 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 in the same universe rather than a large frame in the next universe in the hierarchy.