Homotopy Type Theory premetric space > history (Rev #3, changes)

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

 Definition

Let $R$ be a Archimedean ordered integral domain with a dense linear order?, and let $R_{+}$ be the semiring? of positive terms in $R$. A $R_{+}$-premetric space is a type $R_{+}S$ R_{+} S with a family of types

called the $R_{+}$-premetric, and a family of dependent terms

representing that the $R_{+}$ -premetric for is a$a:A$predicate, $b:A$, $\epsilon:R_{+}$ is a proposition.

Examples

• A $\mathbb{Q}_{+}$-premetric$\mathbb{Q}_{+}$ -premetric on$\mathbb{R}_H$ is used to define the HoTT book real numbers.

See also

• Cauchy structure

• Cauchy net

References

• Auke B. Booij, Analysis in univalent type theory (pdf)