Homotopy Type Theory Dedekind real numbers > history (changes)

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

Definitions

< Dedekind real number

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 function i:𝕀 𝒰 𝒰i:\mathbb{I}_\mathcal{U} \to \mathbb{R}_\mathcal{U} from the locally 𝒰\mathcal{U}-small Dedekind real unit interval 𝕀 𝒰\mathbb{I}_\mathcal{U} to 𝒰\mathbb{R}_\mathcal{U} such that i(0)=0i(0) = 0 and i(1)=1i(1) = 1.

See also

Last revised on June 14, 2022 at 20:21:57. See the history of this page for a list of all contributions to it.