## Definition ### Let $R$ be a dense integral subdomain of the [[rational numbers]] $\mathbb{Q}$ and let $R_{+}$ be the positive terms of $R$. Let us define The __Cauchy real numbers__ $\mathbb{R}_C$ are inductively generated by the following: * a function $inj: C(R, R_{+}) \to \mathbb{R}_C$, where $C(R, R_{+})$ is the type of $R_{+}$-indexed [[net]]s in $R$ that are $R_{+}$-[[Cauchy approximation]]s. * a dependent family of terms $$a:C(R, R_{+}), b:C(R, R_{+}) \vdash eq_{\mathbb{R}_C}(a, b): \left( \prod_{\epsilon:R_{+}} a_\epsilon \sim_{\epsilon} b \right) \to (inj(a) =_{\mathbb{R}_C} inj(b))$$ where the $R_{+}$-[[premetric]] for $\epsilon:R_{+}$ is defined as $$a \sim_{\epsilon} b \coloneqq \vert a_\epsilon - b_\epsilon \vert \lt 4 \epsilon$$ * a family of dependent terms $$a:\mathbb{R}_C, b:\mathbb{R}_C \vdash \tau(a, b): isProp(a =_{\mathbb{R}_C} b)$$ The Cauchy real numbers are sometimes defined using [[sequence]]s $x:\mathbb{N} \to R$, $y:\mathbb{N} \to R$ with [[modulus of Cauchy convergence]] $M:R_{+} \to \mathbb{N}$, $N:R_{+} \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:R_{+} \to R$ as $a \coloneqq x \circ M$ and $b:R_{+} \to R$ 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)]] * [[HoTT book real numbers]] * [[premetric space]] ## 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)