[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Defining the metric on an open interval. Given rational numbers $a:\mathbb{Q}$ and $b:\mathbb{Q}$, we define the open interval $$(a, b) \coloneqq \sum_{c:\mathbb{Q}} (a \lt c) \times (c \lt b)$$ The metric $d_{(a, b)}$ is defined by $$d_{(a, b)}(c, d) =_\mathbb{Q} {| \pi_1(c) - \pi_1(d)|}$$ \begin{definition} A **rational pseudometric space** is a type $X$ with a function $d_X:X \times X \to \mathbb{Q}_{\geq 0}$, which comes with witnesses for symmetry, the triangle identity, and the identity-to-zero-distance condition: $$\mathrm{sym}(x, y):d_X(x, y) =_\mathbb{Q} d_X(y, x)$$ $$\mathrm{triangle}(x, y, z):d_X(x, z) \leq d_X(x, y) + d_X(y, z)$$ $$\mathrm{ptineq}(x):d_X(x, x) =_\mathbb{Q} 0$$ \end{definition} \begin{definition} A rational pseudometric space is a **rational metric space** if the axiom $$\mathrm{idtozerodis}(x, y):(x =_X y) \to (d_X(x, y) =_\mathbb{Q} 0)$$ inductively defined by $$\mathrm{idtozerodis}(x, x, \mathrm{refl}_X(x)) \coloneqq \mathrm{ptineq}(x)$$ is an equivalence of types. \end{definition} category: redirected to nlab