Showing changes from revision #8 to #9:
Added | Removed | Changed
The locally -small Dedekind real numbers for a universe is defined as the Archimedean ordered integral domain with a strictly monotonic function? from the locally -small Dedekind real unit interval to such that and .
The locally -small Dedekind real numbers for a universe is defined as the Archimedean ordered integral domain with a strictly monotonic function? from the locally -small Dedekind real unit interval to such that and .
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Auke B. Booij, Extensional constructive real analysis via locators, (abs:1805.06781)