## Definition ## Let the proposition that an endofunction $f:\mathbb{Z} \to \mathbb{Z}$ over the [[integers]] is *bounded* be defined as follows: $$isBounded(f) \coloneqq \left\Vert \sum_{C:\mathbb{Z}} \prod_{m:\mathbb{Z}} \vert f(m) \vert \lt C \ \right\Vert$$ and let the proposition that $f$ is *almost linear* be defined as follows: $$isAlmostLinear(f) \coloneqq \left\Vert \sum_{C:\mathbb{Z}} \prod_{m:\mathbb{Z}} \prod_{n:\mathbb{Z}} \vert f(m + n) - f(m) - f(n) \vert \lt C \ \right\Vert$$ Let the type of almost linear endofunctions over the integers be defined as $$AL(\mathbb{Z}) \coloneqq \sum_{f:\mathbb{Z} \to \mathbb{Z}} isAlmostLinear(f)$$ 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: $$ \eta : \prod_{f:AL(\mathbb{Z})} \prod_{g:AL(\mathbb{Z})} isBounded(f - g) \to (inj(f) = inj(g))$$ * 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](http://arxiv.org/abs/math/0405454)).