This is a more articulate version of a question I asked a few days ago.
I have made an attempt to "categorify" the theory of metric spaces. Informally, in the spirit of representing a topological space as a category (as in topos theory), I think I have a way to make a 2-category that encodes all the information of a given metric space. I have 3 questions:
1) Does this accomplish what I think it does? Does it accomplish something similar but not exactly what I had in mind? What is it missing?
2) From the point of view of logic, does this constitute an interpretation function, model, or something else? What's missing from a proof that the 2-categories I construct are actually "the same" as the metric spaces I construct them from?
3) Has this been done$^1$ (or has something similar been done), and is it useful/revealing?
On to the actual (hopeful) categorification...
Given a metric space $M = (S, d(-,-))$, we construct a digraph $G=K_S$, labeling the edge that goes from $a$ to $b$ with $d(a,b)$ for $a,b\in S$. We then consider the path category of $G$, the category where $Obj(C) = V(G)$ and $Arr(C)=$ paths between vertices of $G$. We then construct a 2-category structure on the path category of G in the following way:
The 2-category structure will be a preorder, ≤, where
1) $\forall x \in M, d(x,x)=id_x$ is minimal among $\{d(x,a)|a\in M\}$.
2) $\forall x,y \in M, d(x,x) ≥ d(y,y)$. (Also implying $d(x,x) ≤ d(y,y)$.)
(**Notice the similarity between these first two axioms and the metric space axiom $\forall x,y\in M, d(x,y)=0\iff x=y$.)
3)$\forall x,y\in M, d(x,y)≥d(y,x)$. (**This is basically equivalent to symmetry of $d$, since it implies $d(x,y)≤d(y,x)$.)
4)$\forall x,y,z\in M,d(x,z)≤d(y,z)\circ d(x,y)$(**This is hopefully a reformulation of the triangle inequality.)
Obviously this 2-category can't tell you anything about the numerical values of distances between points, but it seems to like it could classify a metric space, at least up to isometry, perhaps with a little revision. I want to say that this captures most of the structure on $[0,\infty)$ that is used to define metric spaces, namely $≤$ and $+$. I acknowledge that I do not know that my ≤ is a total order$^2$, as it is on $[0,\infty)$, and that this issue would either need to be resolved by proof or revision of the axioms.
One issue that was raised on my first attempt at this question is that we still need to understand these metric spaces as topological spaces, i.e. we would need a way to talk about arbitrarily small open balls. My conjecture is that we could reformulate topological statements about a small open ball $B_\epsilon(x)$ as statements about a set $\{y|d(x,y)≤d(x,\epsilon)$ and $\neg [d(x,y)≥d(x,\epsilon)]\}$. I guess my 4th question is: Does this reformulation of the topology of metric spaces seem reasonable?
EDIT(s)/Further thoughts:
$^1$ I know that the canonical categorization of metric spaces is as categories enriched over $([0,\infty],≤)$. Actually, this characterizes Lawvere metric spaces, a more general concept. To me, what I've done feels like a fundamentally different approach, but it's possible that the enriched category approach and my 2-category approach are two ways of saying the same thing.
$^2$Technically, I think I'm actually hoping for ≤ to be a total order on arrows of this category modulo the equivalence $d(a,b) \sim d(c,d) := d(a,b)≤d(c,d)$ and $d(a,b)≥d(c,d)$.
A more substantial point is that the problem of making the 2-category structure into a total order might be easier if we added an inverse arrow for each 1-arrow we have already as the category is currently formulated. $d(x,y)^{-1}$ would be distinct from $d(y,x)$, and the former would be used in conjunction with the given categorical triangle inequality to establish ≤-comparisons between all 1-arrows.