Contents

Whenever editing is allowed on the nLab again, this article should be ported over there.

 Definition

In set theory

A premetric space is a set $S$ with a ternary relation $\sim$ on the Cartesian product $\mathbb{Q}_{+} \times S \times S$, where

is the set of positive rational numbers.

In homotopy type theory

Let $R$ be a dense integral subdomain of the rational numbers $\mathbb{Q}$ and let $R_{+}$ be the positive terms of $R$.

A $R_{+}$-premetric space is a type $S$ with a family of types

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

representing that the $R_{+}$-premetric is a predicate.

Examples

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

See also

• Cauchy structure

• Cauchy net

• limit of a net

• continuous function

References

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