Disambiguation page
There are many different terms which are called Dedekind cuts in the literature.
The following are defined using a $\sigma$-frame, such as the type of propositions in a universe or Sierpinski space:
Dedekind real numbers (disambiguation) 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)