Skip to main content
Post Made Community Wiki
Source Link
Mike Shulman
  • 66.8k
  • 7
  • 162
  • 368

Regarding question 3, one can make an argument that actually the fundamental object is "Set together with Rel". The bijective-on-objects inclusion of Set into Rel is a categorical structure that can be expressed as an F-category, a proarrow equipment, or a double category. All of these are slightly different ways of talking about a (2-)category that has two classes of morphisms.

It turns out that in the particular case of Set+Rel, either class of morphisms can be recovered from the other. The relations are the jointly monic spans of functions, while the functions are the relations with right adjoints. The same fact holds in much greater generality: from any regular category (whose morphisms are "function-like") we can construct a unitary tabular allegory (whose morphisms are "relation-like"), and conversely. The two are really just the same structure expressed in different ways. Sometimes it's more convenient to use the functions; sometimes it's more convenient to use the relations; and sometimes we want both encapsulated in a single structure.

The importance of this sort of two-kinds-of-morphism structure becomes more pronounced as you go up in categorical dimension. For instance, the analogous thing for categories is the inclusion of Cat (whose morphisms are functors) into Prof (whose morphisms are profunctors). In this case, Prof can be constructed from Cat, but with rather more difficulty than Rel is constructed from Set, while Cat cannot be recovered 2-categorically from Prof (e.g. Morita-equivalent categories are equivalent in Prof, but not in Cat). On the other hand, profunctors seem an essential ingredient for doing "formal category theory", e.g. in the formulation of weighted limits and colimits, so it's valuable to keep both kinds of morphism around.