#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 $S$ be a [[premetric space]]. A __Cauchy approximation__ is a function $x \in S^{\mathbb{Q}_{+}}$, where $S^{\mathbb{Q}_{+}}$ is the set of functions with domain $\mathbb{Q}_{+}$ and codomain $S$, such that $$\forall \delta \in \mathbb{Q}_{+}.\forall \eta \in \mathbb{Q}_{+}.x(\delta) \sim_{\delta + \eta} x(\eta)$$ The set of all Cauchy approximations is defined as $$C(S) \coloneqq \{x \in S^{\mathbb{Q}_{+}} \vert \forall \delta \in \mathbb{Q}_{+}.\forall \eta \in \mathbb{Q}_{+}.x(\delta) \sim_{\delta + \eta} x(\eta)\}$$ ### 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. Let $S$ be a [[premetric space]]. We define the predicate $$isCauchyApproximation(x) \coloneqq \prod_{\delta:\mathbb{Q}_{+}} \prod_{\eta:\mathbb{Q}_{+}} x_\delta \sim_{\delta + \eta} x_\eta$$ $x$ is a __Cauchy approximation__ if $$x:\mathbb{Q}_{+} \to S \vdash c(x): isCauchyApproximation(x)$$ The type of Cauchy approximations in $S$ is defined as $$C(S) \coloneqq \sum_{x:\mathbb{Q}_{+} \to S} isCauchyApproximation(x)$$ ## Properties ## Every Cauchy approximation is a [[Cauchy net]] indexed by $\mathbb{Q}_{+}$. This is because $\mathbb{Q}_{+}$ is a strictly ordered type, and thus a directed type and a strictly codirected type, with $N:\mathbb{Q}_{+}$ defined as $N \coloneqq \delta \otimes \eta$ for $\delta:\mathbb{Q}_{+}$ and $\eta:\mathbb{Q}_{+}$. $\epsilon:\mathbb{Q}_{+}$ is defined as $\epsilon \coloneqq \delta + \eta$. Thus, there is a family of dependent terms $$x:\mathbb{Q}_{+} \to S \vdash n(x): isCauchyApproximation(x) \to isCauchyNet(x)$$ A Cauchy approximation is the composition $x \circ M$ of a net $x$ and an [[modulus of Cauchy convergence]] $M$. ## See also ## * [[premetric space]] * [[Cauchy structure]] * [[modulus of Cauchy convergence]] * [[Cauchy real numbers]] * [[HoTT book real numbers]] ## 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)