|
And, these non-negative real numbers, which are these homs, are “hom objects”, so regarded as objects in “the category with as objects the non-negative real numbers, and as morphisms, the ‘being greater than or equal to’ “ ? Is that right? So, I guess, (\R_{>= 0}, >=, +, 0) is like, a monoidal category with + as the monoidal operation? So like, for x,y,z in the metric space, the well, from hom(x,y) and hom(y,z)
I guess the idea is
there is a designated composition morphism from hom(x,y) monoidalProduct hom(y,z) to hom(x,z) which is specifically, hom(x,y)+hom(y,z) >= hom(x,z) (I said designated, but there is only the one, which is just the fact above.) I.e. d(x,y)+d(y,z) >= d(x,z) (Note: I didn’t manage to “just guess” this. I’ve seen it before, and was thinking it through as part of remembering how the idea worked. I am commenting this to both check my understanding in case I’m wrong, and to (assuming I’m remembering the idea correctly) provide an elaboration on what you said for anyone who might want more detail.) |
This works, but it's not quite what you want in most cases. There's a lot of stuff that requires you to enrich over a closed category, so instead we define `Hom(a,b)` to be `max(b - a, 0)` (which you can very roughly think of as replacing the mere proposition `a < b` with its "witnesses"). See https://www.emis.de/journals/TAC/reprints/articles/1/tr1.pdf for more.