Showing changes from revision #3 to #4:
Added | Removed | Changed
The -large Dedekind cut structure real numbers for a universe is defined as the type of all pairs of subtypes of the rational numbers which have a -Dedekind cut structure:
The -Dedekind cut structure real numbers for a $\sigma$-frame is defined as the type of all pairs of open subtypes of the rational numbers which have a -Dedekind cut structure:
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Auke B. Booij, Extensional constructive real analysis via locators, (abs:1805.06781)
Last revised on June 10, 2022 at 14:36:25. See the history of this page for a list of all contributions to it.