Showing changes from revision #3 to #4:
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 cut cuts 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 $\sigma$-frame , (in such as the next type of propositions in a universe or universe Sierpinski space : in the hierarchy):
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.
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Auke B. Booij, Extensional constructive real analysis via locators, (abs:1805.06781)