Homotopy Type Theory Dedekind real numbers > history (Rev #10, changes)

Showing changes from revision #9 to #10: Added | Removed | Changed

Definitions

The locally $\mathcal{U}$-small Dedekind real numbers for a universe $\mathcal{U}$ is defined as the Archimedean ordered integral domain $\mathbb{R}_\mathcal{U}$ with a strictly monotonic functionstrictly monotonic function?$i:\mathbb{I}_\mathcal{U} \to \mathbb{R}_\mathcal{U}$ from the locally i:\mathbb{I}_\mathcal{U} \mathcal{U} \to \mathbb{R}_\mathcal{U} -small from the locally$\mathcal{U}$-small Dedekind real unit interval to \mathbb{R}_\mathcal{U} \mathbb{I}_\mathcal{U} such to that i(0) \mathbb{R}_\mathcal{U} = 0 and such that i(1) i(0) = 1 0 and $i(1) = 1$.