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

See also

References

Revision on June 10, 2022 at 13:17:35 by Anonymous?. See the history of this page for a list of all contributions to it.