Homotopy Type Theory
Dedekind real unit interval > history (Rev #2, changes)
Showing changes from revision #1 to #2:
Added | Removed | Changed
Definitions
Large Dedekind real unit interval
The locally -small Dedekind real unit interval for a universe is defined as the type of extended $\mathcal{U}$-Dedekind cuts on the open unit interval of the rational numbers in a universe: .
The -large Dedekind real numbers for a universe is defined as the type of extended $\mathcal{U}$-Dedekind cuts on the open unit interval of the rational numbers in a universe: .
Sigma-Dedekind real unit interval
The -Dedekind real numbers for a $\sigma$-frame is defined as the type of extended $\Sigma$-Dedekind cuts on the open unit interval of the rational numbers : .
See also
Revision on June 10, 2022 at 17:14:25 by
Anonymous?.
See the history of this page for a list of all contributions to it.