## Definition ## Let $R$ be a [[Archimedean ordered integral domain]] with a [[dense]] [[strict order]], and let $R_{+}$ be the [[semiring]] of positive terms in $R$. Suppose $S$ is a $R_{+}$-[[premetric space]], and let $x:R_{+} \to S$ be a [[net]] with index type $R_{+}$. We define the predicate $$isCauchyApproximation(x) \coloneqq \Vert \prod_{\delta:R_{+}} \prod_{\eta:R_{+}} x_\delta \sim_{\delta + \eta} x_\epsilon \Vert$$ $x$ is a __$R_{+}$-Cauchy approximation__ if $$x:R_{+} \to S \vdash c(x): isCauchyApproximation(x)$$ The type of $R_{+}$-Cauchy approximations in $S$ is defined as $$C(S, R_{+}) \coloneqq \sum_{x:R_{+} \to S} isCauchyApproximation(x)$$ ## Properties ## Every $R_{+}$-Cauchy approximation is a [[Cauchy net]] indexed by $R_{+}$. This is because $R_{+}$ is a [[linear order]], and thus a meet-pseudosemilattice, with $N:R_{+}$ defined as $N \coloneqq \min(\delta, \eta)$ for $\delta:R_{+}$, $\eta:R_{+}$, and meet operation $\min:R_{+} \times R_{+} \to R_{+}$. $\epsilon:R_{+}$ is defined as $\epsilon \coloneqq \delta + \eta$. Thus, there is a family of dependent terms $$x:R_{+} \to S \vdash n(x): isCauchyApproximation(x) \to isCauchyNet(x)$$ A $R_{+}$-Cauchy approximation is the composition $M \circ x$ of a net $x$ and a $R_{+}$-[[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)