Showing changes from revision #2 to #3:
Added | Removed | Changed
Definition
Let be a dense integral subdomain of the rational numbers and let be the positive terms of . The HoTT book real numbers are a homotopy initial -Cauchy structure, i.e. an -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 a dense integral subdomain of the rational numbers and let be the positive terms of . The HoTT book real numbers are inductively generated by the following:
a function
a function , where is the type of -indexed nets in that are -Cauchy - approximations.Cauchy approximations.
a dependent family of terms
and the -premetric type family is simultaneously inductively generated by the following: