Homotopy Type Theory modulus of Cauchy convergence > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | ~~Removed~~ | ~~Chan~~ged

Definition

Let $T R$ T R be a dense integral subdomain of the ~~directed~~ rational ~~type~~ numbers , ~~let~~ $S ℚ$ S \mathbb{Q} be and a let $T R_{+}$ T R_{+} - be the positive terms of $R$ . Let $S$ be a $R_{+}$ -premetric space, and let $x:I \to S$ be a net with index type $I$ . A $T R_{+}$ T R_{+}-modulus of Cauchy convergence is a function $M : T R_{+} \to I$ M: T R_{+} \to I with a type

μ : \prod_{ϵ : T R_{+}} \prod_{i : I} \prod_{j : I} (i \geq M (ϵ)) \times (j \geq M (ϵ)) \to (x_{i} \sim_{ϵ} x_{j})

~~\mu:\prod_{\epsilon:T}~~ \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)

The composition $x \circ M$ of a net $x$ and a $T R_{+}$ T R_{+}-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 31, 2022 at 02:36:08 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 #3, changes)

Definition

See also

References