Homotopy Type Theory Dedekind cut (disambiguation) > history (Rev #3)

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 cut
• Dedekind cut structure

See also

• Dedekind real numbers (disambiguation) 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)

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)