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.