[[!redirects premetric]] ## Definition ## Given a type $T$, a __$T$-premetric space__ is a type $S$ with a family of types $$a:S, b:S, \epsilon:T \vdash a \sim_{\epsilon} b \ type$$ called the __$T$-premetric__, and a family of dependent terms $$a:S, b:S, \epsilon:T \vdash p(a, b, \epsilon):isProp(a \sim_{\epsilon} b)$$ representing that the $T$-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]] ## References ## * Auke B. Booij, Analysis in univalent type theory ([pdf](https://etheses.bham.ac.uk/id/eprint/10411/7/Booij2020PhD.pdf))