#Contents# * table of contents {:toc} Whenever editing is allowed on the [[nLab:HomePage|nLab]] again, this article should be ported over there. ## Definition ### ### In set theory ### Let $\mathbb{Q}$ be the [[rational numbers]] and let $$\mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\}$$ be the set of positive rational numbers. Let $I$ be a [[directed set]] and $$C(I, \mathbb{Q}) \coloneqq \{x \in \mathbb{Q}^I \vert \forall \epsilon \in \mathbb{Q}_{+}. \exists N \in I. \forall i \in I. \forall j \in I. (i \geq N) \wedge (j \geq N) \wedge (x_i \sim_{\epsilon} x_j)\}$$ is the set of all [[Cauchy net]]s with index set $I$ and values in $\mathbb{Q}$. Let $$CauchyNetsIn(\mathbb{Q}) \coloneqq \bigcup_{I \in Ob(DirectedSet_\mathcal{U})} C(I, \mathbb{Q})$$ be the (large) set of all Cauchy nets in $\mathbb{Q}$ in a [[universe]] $\mathcal{U}$, where $DirectedSet_\mathcal{U}$ is the [[category]] of all directed sets in $\mathcal{U}$. Let the [[relation]] $\equiv_{I, J}$ in the Cartesian product $C(I, \mathbb{Q}) \times C(J, \mathbb{Q})$ for directed sets $I$ and $J$ be defined as $$a \equiv_{I, J} b \coloneqq \forall \epsilon \in \mathbb{Q}_{+}, \exists M \in I. \forall i \in I. \exists N \in J. \forall j \in J. (i \geq M) \wedge (j \geq N) \wedge (\vert a_i - b_j \vert \lt \epsilon)$$ Let a *generalized Cauchy algebra* be defined as a [[set]] $A$ with a function $\iota \in {A}^{CauchyNetsIn(\mathbb{Q})}$ such that $$\forall I \in Ob(DirectedSet_\mathcal{U}). \forall J \in Ob(DirectedSet_\mathcal{U}). \forall a \in C(I, \mathbb{Q}). \forall b \in C(J, \mathbb{Q}). (a \equiv_{I, J} b) \implies (\iota(a) = \iota(b))$$ A *generalized Cauchy algebra homomorphism* is a function $f:B^A$ between Cauchy algebras $A$ and $B$ such that $$\forall a \in C(\mathbb{Q}). f(\iota_A(a)) = \iota_B(a)$$ The *category of generalized Cauchy algebras* is the category $GCAlg$ whose objects $Ob(GCAlg)$ are generalized Cauchy algebras and whose morphisms $Mor(GCAlg)$ are generalized Cauchy algebra homomorphisms. The set of **generalized Cauchy real numbers**, denoted $\mathbb{R}$, is defined as the initial object in the category of Cauchy algebras. ### In homotopy type theory ### Let $\mathbb{Q}$ be the [[rational numbers]] and let $$\mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x$$ be the positive rational numbers. The __generalized Cauchy real numbers__ $\mathbb{R}_\mathcal{U}$ are inductively generated by the following: * a function $\iota: \left(\sum_{I:\mathcal{U}} C(I, \mathbb{Q})\right) \to \mathbb{R}_\mathcal{U}$, where $$C(I, \mathbb{Q}) \coloneqq isDirected(I) \times \sum_{x:I \to \mathbb{Q}} isCauchy(x)$$ is the type of all [[Cauchy net]]s with [[directed type|index type]] $I$ and values in $\mathbb{Q}$. * a dependent family of terms $$a:C(I, \mathbb{Q}), b:C(J, \mathbb{Q}) \vdash eq_{\mathbb{R}_\mathcal{U}}(a, b): isEq_{\mathbb{R}_\mathcal{U}}(a, b) \to (\iota(a) =_{\mathbb{R}_\mathcal{U}} \iota(b))$$ where $I$ and $J$ are directed types and the equivalence relation on Cauchy nets $isEq_{\mathbb{R}_\mathcal{U}}(a, b)$ is defined as $$isEq_{\mathbb{R}_\mathcal{U}}(a, b) \coloneqq \prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{M:I} \prod_{i:I} \Vert \sum_{N:J} \prod_{j:J} (i \geq M) \times (j \geq N) \times (\vert a_i - b_j \vert \lt \epsilon) \Vert \Vert$$ * a term $\tau: isSet(\mathbb{R}_\mathcal{U})$ ## See also ## * [[Cauchy real numbers (disambiguation)]] * [[HoTT book real numbers]] * [[Cauchy real numbers]] * [[premetric space]]