Homotopy Type Theory Dedekind real unit interval > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | ~~Removed~~ | ~~Chan~~ged

~~Definitions~~

~~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)_\mathbb{Q}$~~ ~~in a universe:~~ ~~$\mathbb{I}_\mathcal{U} \coloneqq ExtendedDedekindCut_\mathcal{U}((0, 1)_\mathbb{Q})$~~ .

~~See also~~

Dedekind real numbers

extended Dedekind cuts

axiom I-flat?

contractibility of Dedekind real unit interval?

Revision on June 14, 2022 at 20:22:55 by Anonymous?. See the history of this page for a list of all contributions to it.