Homotopy Type Theory Eudoxus real numbers > history (Rev #1)

Definition

Let the proposition that an endofunction $f:\mathbb{Z} \to \mathbb{Z}$ over the integers is bounded be defined as follows:

and let the proposition that $f$ is almost linear be defined as follows:

Let the type of almost linear endofunctions over the integers be defined as

The type of Eudoxus real numbers, denoted as $\mathbb{R}$, is a higher inductive type generated by:

• a function $inj: AL(\mathbb{Z}) \to \mathbb{R}$

• a dependent product of functions from propositions to identities:

• A set-truncator
  $$\tau_0: \prod_{a:\mathbb{R}} \prod_{b:\mathbb{R}} isProp(a=b)$$

See also

• integers

• real numbers for other types of real numbers

References

• Rob Arthan, The Eudoxus Real Numbers, (abs:0405454).