Let the set of almost linear endofunctions over the integers be defined as
Let us define a Eudoxus algebra as a set 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: