Homotopy Type Theory modulus of Cauchy convergence > history (Rev #1)

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

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)

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)