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$\mathrm{<span><del\; class="diffmod">\; i</del><ins\; class="diffmod">\; 𝒰</ins></span>}:{𝕀}_{𝒰}\to {ℝ}_{𝒰}$ i:\mathbb{I}_\mathcal{U} \mathcal{U} \to \mathbb{R}_\mathcal{U} -small from the locally$\mathcal{U}$-small Dedekind real unit interval to${\mathrm{<span><del\; class="diffmod">\; ℝ</del><ins\; class="diffmod">\; 𝕀</ins></span>}}_{𝒰}$ \mathbb{R}_\mathcal{U} \mathbb{I}_\mathcal{U} such to that$i{ℝ}_{𝒰}(0)=0$ i(0) \mathbb{R}_\mathcal{U} = 0 and such that$i(\mathrm{<span><del\; class="diffmod">\; 1</del><ins\; class="diffmod">\; 0</ins></span>})=\mathrm{<span><del\; class="diffmod">\; 1</del><ins\; class="diffmod">\; 0</ins></span>}$ i(1) i(0) = 1 0 and $i(1) = 1$.

See also

• Dedekind real unit interval
• real numbers
• axiom R-flat
• contractibility of Dedekind real numbers