[[!redirects Cauchy real numbers]] #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]] $\mathbb{Q}$ and let $$\mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\}$$ be the positive rational numbers. Let us define a *modulated Cauchy algebra* to be a [[set]] $A$ with a function $\iota \in A^{C(\mathbb{Q})}$, where $C(\mathbb{Q})$ is the set of [[Cauchy approximation]]s in $\mathbb{Q}$ and $A^{C(\mathbb{Q})}$ is the set of functions with domain $C(\mathbb{Q})$ and codomain $A$, such that $$\forall a \in C(\mathbb{Q}). \forall b \in C(\mathbb{Q}). \left( \forall \epsilon \in \mathbb{Q}_{+}. \vert a_\epsilon - b_\epsilon \vert \lt 4 \epsilon \right) \implies (\iota(a) = \iota(b))$$ A *modulated Cauchy algebra homomorphism* is a function $f:B^A$ between modulated Cauchy algebras $A$ and $B$ such that $$\forall a \in C(\mathbb{Q}). f(\iota_A(a)) = \iota_B(a)$$ The *category of modulated Cauchy algebras* is the category $MCAlg$ whose objects $Ob(MCAlg)$ are modulated Cauchy algebras and whose morphisms $Mor(MCAlg)$ are modulated Cauchy algebra homomorphisms. The set of **modulated Cauchy real numbers**, denoted $\mathbb{R}_C$, is defined as the initial object in the category of modulated 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 __modulated Cauchy real numbers__ $\mathbb{R}_C$ are inductively generated by the following: * a function $\iota: C(\mathbb{Q}) \to \mathbb{R}_C$, where $C(\mathbb{Q})$ is the type of [[Cauchy approximation]]s in $\mathbb{Q}$. * a dependent family of terms $$a:C(\mathbb{Q}), b:C(\mathbb{Q}) \vdash eq_{\mathbb{R}_C}(a, b): \left( \prod_{\epsilon:\mathbb{Q}_{+}} \vert a_\epsilon - b_\epsilon \vert \lt 4 \epsilon \right) \to (\iota(a) =_{\mathbb{R}_C} \iota(b))$$ * a family of dependent terms $$a:\mathbb{R}_C, b:\mathbb{R}_C \vdash \tau(a, b): isProp(a =_{\mathbb{R}_C} b)$$ ### Comment ### The modulated Cauchy real numbers are sometimes defined using [[sequence]]s $x:\mathbb{N} \to \mathbb{Q}$, $y:\mathbb{N} \to \mathbb{Q}$ with [[modulus of Cauchy convergence]] $M:\mathbb{Q}_{+} \to \mathbb{N}$, $N:\mathbb{Q}_{+} \to \mathbb{N}$ respectively. However, the composition of a sequence and a modulus of Cauchy convergence yields a Cauchy approximation, so one could define Cauchy approximations $a:\mathbb{Q}_{+} \to \mathbb{Q}$ as $a \coloneqq x \circ M$ and $b:\mathbb{Q}_{+} \to \mathbb{Q}$ as $b \coloneqq y \circ N$, with $x_{M(\epsilon)} = a_\epsilon$ and $y_{N(\epsilon)} = b_\epsilon$ following from function evaluation. In fact, Cauchy approximations and sequences with a modulus of Cauchy convergence are inter-definable. ## See also ## * [[Cauchy real numbers (disambiguation)]] * [[generalized Cauchy real numbers]] * [[HoTT book real numbers]] * [[quotient set]] ## References ## * Auke B. Booij, Analysis in univalent type theory ([pdf](https://etheses.bham.ac.uk/id/eprint/10411/7/Booij2020PhD.pdf)) * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)