Homotopy Type Theory
generalized Cauchy real numbers > history (Rev #3)
Contents
Whenever editing is allowed on the nLab again, this article should be ported over there.
Definition
In set theory
Let be the rational numbers and let
be the set of positive rational numbers. Let be a directed set and
is the set of all Cauchy nets with index set and values in . Let
be the (large) set of all Cauchy nets in in a universe , where is the category of all directed sets in .
Let the relation in the Cartesian product for directed sets and be defined as
The generalized Cauchy real numbers is a set with a function such that
In homotopy type theory
Let be the rational numbers and let
be the positive rational numbers.
The generalized Cauchy real numbers are inductively generated by the following:
-
a function , where
is the type of all Cauchy nets with index type and values in .
-
a dependent family of terms
where and are directed types and the equivalence relation on Cauchy nets is defined as
-
a term
See also
Revision on April 14, 2022 at 01:28:52 by
Anonymous?.
See the history of this page for a list of all contributions to it.