Let the set of almost linear endofunctions over the integers be defined as
The Let set us of define aEudoxus real numbersEudoxus algebra is as aset with a function such that
An Eudoxus algebra homomorphism between two Eudoxus algebras and is a function such that
The category of Eudoxus algebras is the category whose objects are Eudoxus algebras and whose morphisms are Eudoxus algebra homomorphisms. The set of Eudoxus real numbers, denoted , is defined as the initial object in the category of Eudoxus algebras.
In homotopy type theory
Let the proposition that an endofunction over the integers is bounded be defined as follows:
and let the proposition that 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 , is a higher inductive type generated by:
a function
a dependent product of functions from propositions to identities: