[[!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 bounded open interval $$(a, b) \coloneqq \sum_{c:\mathbb{Q}} (a \lt c) \times (c \lt b)$$ Similarly we define the half unbounded open intervals $$(a, \infty) \coloneqq \sum_{c:\mathbb{Q}} (a \lt c)$$ $$(\infty, b) \coloneqq \sum_{c:\mathbb{Q}} (c \lt b)$$ The metrics $d_{(a, b)}$, $d_{(a, \infty)}$, $d_{(\infty, b)}$ is defined in the same way by $$d_{(a, b)}(c, d) =_\mathbb{Q} {| \pi_1(c) - \pi_1(d)|}$$ $$d_{(a, \infty)}(c, d) =_\mathbb{Q} {| \pi_1(c) - \pi_1(d)|}$$ $$d_{(\infty, 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 point inequality 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 function $$\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} These definitions allows us to show that [[rational functions]] on the rational numbers on each disconnected open interval of the domain. category: redirected to nlab