Homotopy Type Theory Cauchy approximation > history (Rev #6)

Definition

Let $T$ be a directed type and codirected type where the directed type operation $\oplus$ is associative, and let $S$ be a $T$-premetric space. We define the predicate

$x$ is a $T$-Cauchy approximation if

The type of $T$-Cauchy approximations in $S$ is defined as

Properties

Every $T$-Cauchy approximation is a Cauchy net indexed by $T$. This is because $T$ is a codirected type, with $N:T$ defined as $N \coloneqq \delta \otimes \eta$ for $\delta:T$ and $\eta:T$. $\epsilon:R_{+}$ is defined as $\epsilon \coloneqq \delta \oplus \eta$.

Thus, there is a family of dependent terms

A $T$-Cauchy approximation is the composition $x \circ M$ of a net $x$ and a $T$-modulus of Cauchy convergence $M$.

See also

• premetric space
• Cauchy structure
• modulus of Cauchy convergence
• Cauchy real numbers
• 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)