Homotopy Type Theory
Dedekind real closed intervals > history (Rev #2, changes)
Showing changes from revision #1 to #2:
Added | Removed | Changed
Definitions
Large rational Dedekind real closed intervals
The -large rational Dedekind realclosed intervals for a universe is defined as the type of -interval cuts on the rational numbers in a universe: .
Sigma-rational Sigma-Dedekind real closed intervals
The -rational -Dedekind realclosed intervals for a $\sigma$-frame is defined as the type of -interval cuts on the rational numbers : .
See also
Revision on April 22, 2022 at 21:37:10 by
Anonymous?.
See the history of this page for a list of all contributions to it.