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.
Other attempted axiomatizations of the same idea “something that acts like the category of relations in a regular category” include:
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.