[[!redirects premetric]] ## 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 $$a:A, b:A, \epsilon:R_{+} \vdash a \sim_{\epsilon} b \ type$$ called the __$R_{+}$-premetric__, and a family of dependent terms $$a:A, b:A, \epsilon:R_{+} \vdash p(a, b, \epsilon):isProp(a \sim_{\epsilon} b)$$ 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](https://etheses.bham.ac.uk/id/eprint/10411/7/Booij2020PhD.pdf))