Hacker News new | ask | show | jobs
by consilient 1065 days ago
> 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’ “ ?

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.