#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 positive rational numbers. Let $S$ be a [[premetric space]], and let $x \in S^I$ be a [[net]] with index set $I$. A __modulus of Cauchy convergence__ is a function $M \in I^{\mathbb{Q}_{+}}$ such that $$\forall \epsilon \in \mathbb{Q}_{+}. \forall i \in I. \forall j \in I. (i \geq M(\epsilon)) \wedge (j \geq M(\epsilon)) \implies (x_i \sim_{\epsilon} x_j)$$ The composition $x \circ M$ of a net $x$ and a modulus of Cauchy convergence $M$ is also a [[net]]. ### 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]], and let $x:I \to S$ be a [[net]] with index type $I$. A __modulus of Cauchy convergence__ is a function $M: \mathbb{Q}_{+} \to I$ with a type $$\mu:\prod_{\epsilon:\mathbb{Q}_{+}} \prod_{i:I} \prod_{j:I} (i \geq M(\epsilon)) \times (j \geq M(\epsilon)) \to (x_i \sim_{\epsilon} x_j)$$ The composition $x \circ M$ of a net $x$ and a modulus of Cauchy convergence $M$ is also a [[net]]. ## 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)