Homotopy Type Theory
HoTT book real numbers > history (Rev #12, changes)
Showing changes from revision #11 to #12:
Added | Removed | Changed
Contents
Whenever editing is allowed on the nLab again, this article should be ported over there.
Definition
In set theory
The Let set ofHoTT book real numbers be anArchimedean ordered field is and the let initial object in thecategory of Cauchy structures and Cauchy structure homomorphisms.
be the positive elements in . is sequentially Cauchy complete if every Cauchy sequence in converges:
The set of HoTT book real numbers is the initial sequentially Cauchy complete? Archimedean ordered field.
The set of HoTT book real numbers is the initial object in the category of Cauchy structures and Cauchy structure homomorphisms.
In homotopy type theory
The HoTT book real numbers are a homotopy initial Cauchy structure, i.e. a Cauchy structure such that for every other Cauchy structure , the type of Cauchy structure homomorphisms with domain and codomain is contractible.
As a higher inductive-inductive type
Let be the rational numbers and let
be the positive rational numbers. The HoTT book real numbers are inductively generated by the following:
-
a function
-
a function , where is the type of Cauchy approximations in .
-
a dependent family of terms
and the premetric type family is simultaneously inductively generated by the following:
-
a dependent family of terms
-
a dependent family of terms
-
a dependent family of terms
-
a dependent family of terms
-
a dependent family of terms
See also
References
Revision on April 14, 2022 at 19:32:23 by
Anonymous?.
See the history of this page for a list of all contributions to it.