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

Definition

Let $A$ be a dense Archimedean ordered abelian group with a point $1:A$ and a term $\zeta: 0 \lt 1$. Let $A_{+} \coloneqq \sum_{a:A} (0 \lt a)$ be the positive cone? of $A$.

Let $S$ be a $A_{+}$-premetric space. We define the predicate

$x$ is a $A_{+}$-Cauchy approximation if

The type of $A_{+}$-Cauchy approximations in $S$ is defined as

Properties

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

Thus, there is a family of dependent terms

A $A_{+}$-Cauchy approximation is the composition $x \circ M$ of a net $x$ and a $A_{+}$-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)