Homotopy Type Theory Dedekind real unit interval > history (Rev #2)

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})$ .

Homotopy Type Theory Dedekind real unit interval > history (Rev #2)

Definitions

See also