Richman Premetric Space

A Richman Premetric Space is an alternative definition of a Metric Space that is more suitable in Constructive Mathematics. Explicitly, a Richman premetric space consists of:

• A set $X$
• A ternary relation $D:X\to X\to\mathbb{Q}_{0\leq}\to\Omega$
• For all $x,y:X$, $D(x,y,0)\leftrightarrow x=y$. In other words, $D(-,=,0)$ is an Identity System.
• For all $x,y:X$, there merely exists some $q$ such that $D(x,y,q)$
• For all $x,y:X$, and $q\leq r$, $D(x,y,q)\to D(x,y,r)$
• For all $x,y,z:X$, if $D(x,y,q)$ and $D(y,z,r)$, then $D(x,z,q+r)$ More concisely, $D$ satisfies the Triangle inequality with respect to $+$.

Generalizations

A Richman Premetric space is a sort of Locally Graded Category; in particular, one graded by a Min Tropical Semiring.