## Definition ## Let $T$ be a [[directed type]] and [[codirected type]] where the directed type operation $\oplus$ is associative, and let $S$ be a $T$-[[premetric space]]. We define the predicate $$isCauchyApproximation(x) \coloneqq \prod_{\delta:T} \prod_{\eta:T} x_\delta \sim_{\delta \oplus \eta} x_\eta$$ $x$ is a __$T$-Cauchy approximation__ if $$x:T \to S \vdash c(x): isCauchyApproximation(x)$$ The type of $T$-Cauchy approximations in $S$ is defined as $$C(S, T) \coloneqq \sum_{x:T \to S} isCauchyApproximation(x)$$ ## Properties ## Every $T$-Cauchy approximation is a [[Cauchy net]] indexed by $T$. This is because $T$ is a codirected type, with $N:T$ defined as $N \coloneqq \delta \otimes \eta$ for $\delta:T$ and $\eta:T$. $\epsilon:R_{+}$ is defined as $\epsilon \coloneqq \delta \oplus \eta$. Thus, there is a family of dependent terms $$x:T \to S \vdash n(x): isCauchyApproximation(x) \to isCauchyNet(x)$$ A $T$-Cauchy approximation is the composition $x \circ M$ of a net $x$ and a $T$-[[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)