## Definition ## Let $A$ be a [[abelian group]] with a point $1:A$, a [[strict order]] $\lt$, a term $\zeta: 0 \lt 1$ and a family of dependent terms $$a:A, b:A \vdash \alpha(a, b):(0 \lt a) \times (0 \lt b) \to (0 \lt a + b)$$ Let $A_{+} \coloneqq \sum_{a:A} (0 \lt a)$ be the [[positive cone]] of $A$. Let $S$ be a $A_{+}$-[[premetric space]]. We define the predicate $$isCauchyApproximation(x) \coloneqq \prod_{\delta:A_{+}} \prod_{\eta:A_{+}} x_\delta \sim_{\delta \oplus \eta} x_\eta$$ $x$ is a __$A_{+}$-Cauchy approximation__ if $$x:A_{+} \to S \vdash c(x): isCauchyApproximation(x)$$ The type of $A_{+}$-Cauchy approximations in $S$ is defined as $$C(S, A_{+}) \coloneqq \sum_{x:A_{+} \to S} isCauchyApproximation(x)$$ ## Properties ## Every $A_{+}$-Cauchy approximation is a [[Cauchy net]] indexed by $A_{+}$. This is because $A_{+}$ is a strictly ordered type, and thus a directed type and a strictly codirected type, with $N:A_{+}$ defined as $N \coloneqq \delta \otimes \eta$ for $\delta:A_{+}$ and $\eta:A_{+}$. $\epsilon:R_{+}$ is defined as $\epsilon + \delta \oplus \eta$. Thus, there is a family of dependent terms $$x:A_{+} \to S \vdash n(x): isCauchyApproximation(x) \to isCauchyNet(x)$$ A $A_{+}$-Cauchy approximation is the composition $x \circ M$ of a net $x$ and a $A_{+}$-[[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)