Homotopy Type Theory Dedekind real unit interval > history (changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Definitions

< unit interval

The

locally 𝒰\mathcal{U}-small Dedekind real unit interval for a universe 𝒰\mathcal{U} is defined as the type of extended $\mathcal{U}$-Dedekind cuts on the open unit interval of the rational numbers (0,1) (0, 1)_\mathbb{Q} in a universe: 𝕀 𝒰ExtendedDedekindCut 𝒰((0,1) )\mathbb{I}_\mathcal{U} \coloneqq ExtendedDedekindCut_\mathcal{U}((0, 1)_\mathbb{Q}).

See also

Last revised on June 14, 2022 at 16:22:55. See the history of this page for a list of all contributions to it.