## 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:I \to S$ be a [[net]] with index type $I$. A __$R_{+}$-modulus of Cauchy convergence__ is a function $M: R_{+} \to I$ with a type $$\mu:\prod_{\epsilon:R_{+}} \prod_{i:I} \prod_{j:I} (i \geq M(\epsilon)) \times (j \geq M(\epsilon)) \to (x_i \sim_{\epsilon} x_j)$$ A $R_{+}$-[[Cauchy approximation]] is the composition $M \circ x$ of a net $x$ and a $R_{+}$-modulus of Cauchy convergence $M$. ## See also ## * [[limit of a net]] * [[premetric space]] * [[Cauchy structure]] * [[Cauchy approximation]] * [[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)