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

Definition

Let $T$ be a directed type, let $S$ be a $T$ -premetric space, and let $x:I \to S$ be a net with index type $I$ . A $T$ -modulus of Cauchy convergence is a function $M: T \to I$ with a type

\mu:\prod_{\epsilon:T} \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 $T$ -modulus of Cauchy convergence $M$ is also a net.

References

Auke B. Booij, Analysis in univalent type theory (pdf)
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

Revision on March 12, 2022 at 08:30:11 by Anonymous?. See the history of this page for a list of all contributions to it.

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

Definition

See also

References