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): * [[two-sided bounded Dedekind cut]] * [[lower bounded Dedekind cut]] * [[upper bounded Dedekind cut]] * [[two-sided unbounded Dedekind cut]] * [[lower unbounded Dedekind cut]] * [[upper unbounded Dedekind cut]] * [[two-sided bounded Dedekind cut structure]] * [[lower bounded Dedekind cut structure]] * [[upper bounded Dedekind cut structure]] * [[two-sided unbounded Dedekind cut structure]] * [[lower unbounded Dedekind cut structure]] * [[upper unbounded Dedekind cut structure]] 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|$\sigma$-frame]] in the same universe rather than a large frame in the next universe in the hierarchy. * [[two-sided bounded sigma-Dedekind cut]] * [[lower bounded sigma-Dedekind cut]] * [[upper bounded sigma-Dedekind cut]] * [[two-sided unbounded sigma-Dedekind cut]] * [[lower unbounded sigma-Dedekind cut]] * [[upper unbounded sigma-Dedekind cut]] * [[two-sided bounded sigma-Dedekind cut structure]] * [[lower bounded sigma-Dedekind cut structure]] * [[upper bounded sigma-Dedekind cut structure]] * [[two-sided unbounded sigma-Dedekind cut structure]] * [[lower unbounded sigma-Dedekind cut structure]] * [[upper unbounded sigma-Dedekind cut structure]] ## See also ## * [[Dedekind real numbers]] for the types of real numbers that use Dedekind cuts. * [[dense strict order]] ## References ## * Auke B. Booij, Extensional constructive real analysis via locators, ([abs:1805.06781](https://arxiv.org/abs/1805.06781)) * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)