Homotopy Type Theory
Eudoxus real numbers > history (Rev #2, changes)
Showing changes from revision #1 to #2:
Added | Removed | Changed
Contents
Whenever editing is allowed on the nLab again, this article should be ported over there.
Definition
Let the proposition that an endofunction over the integers is bounded be defined as follows:
In set theory
An endofunction over the integers is bounded if
and let the proposition that is almost linear be defined as follows:
and is almost linear if
Let the set of almost linear endofunctions over the integers be defined as
The set of Eudoxus real numbers is a set with a function such that
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 set-truncator
See also
References
Revision on April 13, 2022 at 23:42:51 by
Anonymous?.
See the history of this page for a list of all contributions to it.