A 2-category equipped with proarrows is a 2-category together with a 2-category of “proarrows” which are intended to generalize the arrows of in the same way that profunctors generalize the functors in Cat. Since profunctors are a categorification of relations, it is natural to think of decategorifying such equipments to give a structure on a 1-category that equips it with “relations”. We call this structure a 1-category equipped with relations.
Recall that a 2-category equipped with proarrows (aka “proarrow equipment” or “equipment”) can be defined as a certain sort of double category, with . If, in such a double category, any two squares with the same boundary are equal, we say that it is is a (1,2)-category equipped with proarrows, or a (1,2)-category proarrow equipment. This is equivalent to requiring that the 2-category of proarrows (and hence also the underlying 2-category of arrows) is locally posetal, i.e. a (1,2)-category.
A 1-category equipped with relations is a (1,2)-category equipped with proarrows, regarded as a double category , together with an involution which is (isomorphic to) the identity on objects and (vertical) arrows. Here denotes the horizontal opposite of a double category obtained by reversing the horizontal (pro-)arrows but not the vertical ones. We also call this structure a relation equipment or a 1-category proarrow equipment.
In particular, the definition implies that we have an involution which is the identity on objects and arrows, which for a (1,2)-category means that is actually (equivalent to) a 1-category. Note though that the 2-category of proarrows (which we now call “relations”) is still (like Rel) a (1,2)-category, not necessarily a 1-category.
For example, for any quantale , the sub-2-category of consisting of the symmetric -categories (those where ) is a 1-category equipped with relations. In particular, for , we have the relation equipment of sets, functions, and binary relations.
In general, we can think of a relation equipment as generalizing some of the properties of . For instance, internal relations in any regular category also form a relation equipment.
It is proven in
that a (1,2)-category is a cartesian bicategory precisely when it is a cartesian object in a suitable 2-category of proarrow equipments (where we make a bicategory into an equipment by taking the proarrows to be those of and the arrows to be the “maps” in , i.e. the morphisms having right adjoints). Here is a rough sketch of the argument, using the double-category description of equipments.
Let be a 1-category equipped with relations, which is a cartesian object in the 2-category of relation equipments (that is, it is a cartesian relation equipment). Then is a cartesian bicategory.
That is a cartesian object means, in particular, that it is a pseudomonoid in the 2-category of equipments. By lifting the coherence data from arrows to representable proarrows, it follows that is a monoidal 2-category. Being a cartesian object also gives a cartesian product on objects and proarrows, with diagonals , and lifting these arrows to representable proarrows and gives each object a commutative monoid and comonoid structure. Now for any proarrow , the square
in induces 2-cells, i.e. inequalities, and .
A bicategory of relations is a (1,2)-category which is a cartesian bicategory, and which also satisfies some additional conditions. We can also construct this structure starting from a relation equipment.
Let be a relation equipment satisfying the hypotheses of the previous theorem, and suppose in addition that every proarrow in can be written as for some (vertical) arrows and . (That is, “tabulations” in a certain sense exist.) Then is a bicategory of relations.
We first verify the axiom . Since is the restriction of along on both sides, it suffices to show that
is a cartesian 2-cell in . But if we have any other square
then factoring through means that , and likewise . Composing the given square with the projection
(which comes from being a cartesian object in ), we obtain a square
which factors the given square through the putative cartesian one. The factorization is unique since all 2-cells are unique.
We now verify the Frobenius axiom . Since is associative, we have a square
and therefore a square
and it suffices to show that this is a cartesian 2-cell. So suppose given a square
The fact that and appear twice is equivalent to saying that the left and right boundaries of this square factor through and , respectively. Now by assumption, for some and . Thus our square is equivalent to one
But this is just a 2-cell in the vertical category , which is a 1-category; hence we have and thus . Calling their common value , we thus have a composite square
(since ) which gives us the desired factorization. The other Frobenius axiom is, of course, dual.
If is a relation equipment satisfying the hypotheses of the theorem, then is an allegory.
It is shown here that any bicategory of relations is an allegory.
Other attempted axiomatizations of the same idea “something that acts like the category of relations in a regular category” include: