Homotopy Type Theory
Cauchy structure > 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
Let be a dense integral subdomain of the rational numbers and let be the positive terms of .
In set theory
An ACauchy structure-Cauchy structure is a premetric space -premetric space with a function and a function such that
-
a function
-
a function , where is the type of -Cauchy approximations in
-
dependent families of terms
For two Cauchy structures and , a Cauchy structure homomorphism is a function such that
For two -Cauchy structures and , a -Cauchy structure homomorphism consists of
-
a function
-
a dependent family of functions
-
a dependent family of types
-
a dependent family of types
-
a dependent family of types
In homotopy type theory
Let be a dense integral subdomain of the rational numbers and let be the positive terms of .
An -Cauchy structure is a -premetric space with
-
a function
-
a function , where is the type of -Cauchy approximations in
-
dependent families of terms
For two -Cauchy structures and , a -Cauchy structure homomorphism consists of
-
a function
-
a dependent family of functions
-
a dependent family of types
-
a dependent family of types
-
a dependent family of types
See also
References
- Auke B. Booij, Analysis in univalent type theory (pdf)
Revision on April 13, 2022 at 22:00:44 by
Anonymous?.
See the history of this page for a list of all contributions to it.