#Contents# * table of contents {:toc} Whenever editing is allowed on the [[nLab:HomePage|nLab]] again, this article should be ported over there. ## Definition ## ### In set theory ### An endofunction $f:\mathbb{Z}^\mathbb{Z}$ over the [[integers]] is *bounded* if $$\exists C \in \mathbb{Z}. \forall m \in \mathbb{Z}. \vert f(m) \vert \lt C$$ and $f$ is *almost linear* if $$\exists C \in \mathbb{Z}. \forall m \in \mathbb{Z}. \forall n \in \mathbb{Z}. \vert f(m + n) - f(m) - f(n) \vert \lt C$$ Let the set of almost linear endofunctions over the integers be defined as $$AL(\mathbb{Z}) \coloneqq \{f\in \mathbb{Z}^\mathbb{Z} \vert \exists C \in \mathbb{Z}. \forall m \in \mathbb{Z}. \forall n \in \mathbb{Z}. \vert f(m + n) - f(m) - f(n) \vert \lt C \}$$ Let us define a *Eudoxus algebra* as a [[set]] $A$ with a function $\iota \in A^{AL(\mathbb{Z})}$ such that $$\forall f \in AL(\mathbb{Z}). \forall g \in AL(\mathbb{Z}). (\exists C \in \mathbb{Z}. \forall m \in \mathbb{Z}. \vert f(m) - g(m) \vert \lt C) \implies (\iota(f) = \iota(g))$$ An *Eudoxus algebra homomorphism* between two Eudoxus algebras $A$ and $B$ is a function $f \in B^A$ such that $$\forall a \in AL(\mathbb{Z}). f(\iota_A(a)) = \iota_B(a)$$ The *category of Eudoxus algebras* is the category $EudoxusAlg$ whose objects $Ob(EudoxusAlg)$ are Eudoxus algebras and whose morphisms $Mor(EudoxusAlg)$ are Eudoxus algebra homomorphisms. The set of **Eudoxus real numbers**, denoted $\mathbb{R}$, is defined as the initial object in the category of Eudoxus algebras. ### In homotopy type theory ### 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 $\iota: 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 (\iota(f) = \iota(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 * [[quotient set]] ## References ## * Rob Arthan, The Eudoxus Real Numbers, ([abs:0405454](http://arxiv.org/abs/math/0405454)).