[[!redirects premetric]] #Contents# * table of contents {:toc} Whenever editing is allowed on the [[nLab:HomePage|nLab]] again, this article should be ported over there. ## Definition ## ### In set theory ### Let $\mathbb{Q}$ be the [[rational numbers]] and let $$\mathbb{Q}_{+} \coloneqq \{x \in \mathbb{Q} \vert 0 \lt x\}$$ 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 $$\mathbb{Q}_{+} \coloneqq \sum_{x:\mathbb{Q}} 0 \lt x$$ be the positive rational numbers. A __premetric space__ is a type $S$ with a family of types $$a:S, b:S, \epsilon:\mathbb{Q}_{+} \vdash a \sim_{\epsilon} b \ type$$ called the __premetric__, and a family of dependent terms $$a:S, b:S, \epsilon:\mathbb{Q}_{+} \vdash p(a, b, \epsilon):isProp(a \sim_{\epsilon} b)$$ 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]] * [[continuous function]] ## References ## * Auke B. Booij, Analysis in univalent type theory ([pdf](https://etheses.bham.ac.uk/id/eprint/10411/7/Booij2020PhD.pdf))