Homotopy Type Theory premetric space > history (Rev #2)

 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_{+}$ with a family of types

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

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

Examples

• A $\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)