Homotopy Type Theory Cauchy approximation > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Definition

Let $R$ be a Archimedean ordered integral domain with a dense linear order?dense , and let$R_{+}$strict order , be and the let$R_{+}$ be the semiring? of positive terms in $R$.

Suppose $S$ is a $R_{+}$-premetric space, and let $x:R_{+} \to S$ be a net with index type $R_{+}$. We define the predicate

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

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

Properties

Every $R_{+}$-Cauchy approximation is a Cauchy net indexed by $R_{+}$. This is because $R_{+}$ is a linear order, and thus a meet-pseudosemilattice, with $N:R_{+}$ defined as $N \coloneqq \min(\delta, \eta)$ for $\delta:R_{+}$, $\eta:R_{+}$, and meet operation $\min:R_{+} \times R_{+} \to R_{+}$. $\epsilon:R_{+}$ is defined as $\epsilon \coloneqq \delta + \eta$.

Thus, there is a family of dependent terms

See also

• premetric space
• Cauchy structure
• 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)