Homotopy Type Theory pre-algebra real numbers > history (Rev #3)

Idea

The real numbers as encountered in pre-algebra.

Definition

The pre-algebra real numbers $\mathbb{R}$ is an Archimedean ordered field such that the infinite decimal representation function of the unit interval $\mathcal{I}:[0, 1]_\mathbb{R} \to (\mathbb{N} \to [0, 9]_\mathbb{N})$ is an equivalence.

See also

• real numbers
• limited principle of omniscience