Showing changes from revision #1 to #2:
Added | Removed | Changed
Disambiguation page
There are many different terms which are called Dedekind cuts in the literature.
The following terms are defined using the type of all propositions in a universe, so that the type of Dedekind cuts form a (large) frame (in the next universe in the hierarchy):
The following terms 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 type of Dedekind cuts form a $\sigma$-frame in the same universe rather than a large frame in the next universe in the hierarchy.
Dedekind real numbers for the types of real numbers that use Dedekind cuts.
Auke B. Booij, Extensional constructive real analysis via locators, (abs:1805.06781)
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)