Showing changes from revision #4 to #5:
Added | Removed | Changed
The Dedekind real numbers is a Dedekind complete Archimedean ordered field.
The -large Dedekind real numbers for a universe is defined as the type of -Dedekind cuts on the rational numbers in a universe: .
The -Dedekind real numbers for a $\sigma$-frame is defined as the type of -Dedekind cuts on the rational numbers : .
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Auke B. Booij, Extensional constructive real analysis via locators, (abs:1805.06781)