Contents

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

 Definition

In set theory

Let $\mathbb{Q}$ be the rational numbers and let

be the set of positive rational numbers.

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

In homotopy type theory

Let $\mathbb{Q}$ be the rational numbers and let

be the positive rational numbers.

A premetric space is a type $S$ with a family of types

called the premetric, and a family of dependent terms

representing that the premetric is a predicate.

Examples

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

See also

• Cauchy structure

• Cauchy net

• limit of a net

• pointwise continuous function

• uniformly continuous function

References

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