# nLab bicategory of relations

## In higher category theory

#### 2-Category theory

2-category theory

# Bicategories of relations

## Idea

A bicategory of relations is a (1,2)-category which behaves like the 2-category of internal relations in a regular category. The notion is due to Carboni and Walters.

## Definition

Note: in this article, the direction of composition is diagrammatic (i.e., “anti-Leibniz”).

A bicategory of relations is a cartesian bicategory which is locally posetal and moreover in which for every object $X$, the diagonal $\Delta :X\to X\otimes X$ and codiagonal $\nabla :X\otimes X\to X$ satisfy the Frobenius condition:

$\nabla \Delta =\left(1\otimes \Delta \right)\left(\nabla \otimes 1\right).$\nabla\Delta = (1\otimes \Delta)(\nabla \otimes 1).

Of course, in the locally posetal case the definition of cartesian bicategory simplifies greatly: it amounts to a symmetric monoidal Pos-enriched category for which every object carries a commutative comonoid structure, for which the structure maps ${\Delta }_{X}:X\to X\otimes X$, ${\epsilon }_{X}:X\to 1$ are left adjoint 1-morphisms, and for which every morphism $R:X\to Y$ is a colax morphism of comonoids in the sense that the following inequalities hold:

$R{\Delta }_{Y}\le {\Delta }_{X\otimes X}\left(R\otimes R\right),\phantom{\rule{2em}{0ex}}R{\epsilon }_{Y}\le {\epsilon }_{X}.$R \Delta_Y \leq \Delta_{X \otimes X} (R \otimes R), \qquad R \varepsilon_Y \leq \varepsilon_X.

We remark that such structure is unique when it exists (being a cartesian bicategory is a property of, as opposed to structure on, a bicategory). The tensor product $\otimes$ behaves like the ordinary product of relations. Note this is not a cartesian product in the sense of the usual universal property; nevertheless, it is customary to write it as a product $×$, and we follow this custom below. It does become a cartesian product if one restricts to the subcategory of left adjoints (called maps), which should be thought of as functional relations.

## Properties

We record a few consequences of this notion.

###### Proposition

(Separability condition) $\Delta \nabla =1$.

###### Proof

In one direction, we have the 2-cell $1\le \Delta \nabla$ which is the unit of the adjunction $\Delta ⊣{\Delta }_{*}=\nabla$. In the other direction, there is an adjunction $\epsilon ⊣{\epsilon }_{*}$ between the counit and its dual, and the unit of this adjunction is a 2-cell $1\le \epsilon {\epsilon }_{*}$, from which we derive

$\Delta \nabla =\Delta {\Delta }_{*}\le \Delta \left(1×\epsilon \right)\left(1×{\epsilon }_{*}\right){\Delta }_{*}=1$\Delta\nabla = \Delta\Delta_* \leq \Delta (1 \times \varepsilon)(1 \times \varepsilon_*)\Delta_* = 1

where the last equation follows from the equation $\Delta \left(1×\epsilon \right)=1$ and its dual $\left(1×{\epsilon }_{*}\right){\Delta }_{*}=1$.

###### Proposition

(Dual Frobenius condition) $\nabla \Delta =\left(\Delta ×1\right)\left(1×\nabla \right)$.

###### Proof

The locally full subcategory whose 1-cells are maps (= left adjoints) has finite products, in particular a symmetry involution $\sigma$ for which

${\Delta }_{X}{\sigma }_{XX}={\Delta }_{X}$\Delta_X \sigma_{X X} = \Delta_X

Additionally, the right adjoint ${\sigma }_{XY*}$ is the inverse ${\sigma }_{XY}^{-1}={\sigma }_{YX}$. Hence the equation above is mated to ${\sigma }_{XX}{\nabla }_{X}={\nabla }_{X}$, and we calculate

$\begin{array}{ccc}{\nabla }_{X}{\Delta }_{X}& =& {\sigma }_{XX}{\nabla }_{X}{\Delta }_{X}{\sigma }_{XX}\\ & =& {\sigma }_{XX}\left(1×{\Delta }_{X}\right)\left({\nabla }_{X}×1\right){\sigma }_{XX}\\ & =& \left({\Delta }_{X}×{1}_{X}\right){\sigma }_{X×X,X}{\sigma }_{X×X,X}\left({1}_{X}×{\nabla }_{X}\right)\\ & =& \left({\Delta }_{X}×{1}_{X}\right)\left({\sigma }_{XX}×1\right)\left(1×{\sigma }_{XX}\right)\left(1×{\nabla }_{X}\right)\\ & =& \left({\Delta }_{X}×{1}_{X}\right)\left({1}_{X}×{\nabla }_{X}\right)\end{array}$\array{ \nabla_X \Delta_X & = & \sigma_{X X}\nabla_X \Delta_X \sigma_{X X} \\ & = & \sigma_{X X} (1 \times \Delta_X)(\nabla_X \times 1) \sigma_{X X} \\ & = & (\Delta_X \times 1_X) \sigma_{X \times X, X} \sigma_{X \times X, X} (1_X \times \nabla_X) \\ & = & (\Delta_X \times 1_X) (\sigma_{X X} \times 1) (1 \times \sigma_{X X}) (1 \times \nabla_X) \\ & = & (\Delta_X \times 1_X)(1_X \times \nabla_X) }

which gives the dual equation.

###### Theorem

In a bicategory of relations, each object is dual to itself, making the bicategory a compact closed bicategory.

###### Proof

Both the unit and counit of the desired adjunction $X⊣X$ are given by equality predicates:

${\eta }_{X}=\left(1\stackrel{{\epsilon }_{*}}{\to }X\stackrel{\Delta }{\to }X×X\right)\phantom{\rule{2em}{0ex}}{\theta }_{X}=\left(X×X\stackrel{\nabla }{\to }X\stackrel{\epsilon }{\to }1\right)$\eta_X = (1 \stackrel{\varepsilon_*}{\to} X \stackrel{\Delta}{\to} X \times X) \qquad \theta_X = (X \times X \stackrel{\nabla}{\to} X \stackrel{\varepsilon}{\to} 1)

One of the triangular equations follows from the commutative diagram

$\begin{array}{ccccc}X& \stackrel{1×{\epsilon }_{*}}{\to }& X×X& \stackrel{1×\Delta }{\to }& X×X×X\\ & {}_{1}↘& ↓\nabla & & ↓\nabla ×1\\ & & X& \stackrel{\Delta }{\to }& X×X\\ & & & {}_{1}↘& ↓\epsilon ×1\\ & & & & X\end{array}$\array{ X & \stackrel{1 \times \varepsilon_*}{\to} & X \times X & \stackrel{1 \times \Delta}{\to} & X \times X \times X \\ & {}_1\searrow & \downarrow \mathrlap{\nabla} & & \downarrow \mathrlap{\nabla \times 1} \\ & & X & \overset{\Delta}{\to} & X \times X \\ & & & {}_{1}\searrow & \downarrow \mathrlap{\varepsilon \times 1} \\ & & & & X }

where the square expresses a Frobenius equation. The other triangular equation uses the dual Frobenius equation.

The compact closure allows us to define the opposite of a relation $R:X\to Y$ as the 1-morphism mate:

${R}^{\mathrm{op}}=\left(Y\stackrel{{1}_{Y}×{\eta }_{X}}{\to }Y×X×X\stackrel{{1}_{Y}×R×{1}_{X}}{\to }Y×Y×X\stackrel{{\theta }_{Y}×{1}_{X}}{\to }X\right)$R^{op} = (Y \stackrel{1_Y \times \eta_X}{\to} Y \times X \times X \stackrel{1_Y \times R \times 1_X}{\to} Y \times Y \times X \stackrel{\theta_Y \times 1_X}{\to} X)

In this way, a bicategory of relations becomes a †-compact $\mathrm{Pos}$-enriched category.

Recall (again) that a map in the bicategory of relations is the same as a 1-cell that has a right adjoint.

###### Proposition

If $f:X\to Y$ is a map, then $f$ is a strict morphism of comonoids.

###### Proof

If $g$ is the right adjoint of $f$, we have ${\Delta }_{X}g\le \left(g×g\right){\Delta }_{Y}$ since $g$, like any morphism, is a lax comonoid morphism. But this 2-cell is mated to a 2-cell $\left(f×f\right){\Delta }_{X}\to {\Delta }_{Y}f$, inverse to the 2-cell ${\Delta }_{Y}f\to \left(f×f\right){\Delta }_{X}$ that comes for free. So $f$ preserves comultiplication strictly. A similar argument shows $f$ preserves the counit strictly.

###### Proposition

If $f:X\to Y$ is a map, then ${f}^{\mathrm{op}}:Y\to X$ equals the right adjoint ${f}_{*}$.

###### Proof

The proof is much more perspicuous if we use string diagrams. But the key steps are given in two strings of equalities and inequalities. The first gives a counit for $f⊣{f}^{\mathrm{op}}$, and the second gives a unit. We have

$\begin{array}{ccc}f{f}^{\mathrm{op}}& \stackrel{0}{=}& f\circ \left({\epsilon }_{Y}×1\right)\left({\nabla }_{Y}×1\right)\left(1×f×1\right)\left(1×{\Delta }_{X}\right)\left(1×{\epsilon }_{X}{}_{*}\right)\\ & \stackrel{1}{=}& \left({\epsilon }_{Y}×1\right)\left({\nabla }_{Y}×1\right)\left(1×f×f\right)\left(1×{\Delta }_{X}\right)\left(1×{\epsilon }_{X}{}_{*}\right)\\ & \stackrel{2}{=}& \left({\epsilon }_{Y}×1\right)\left({\nabla }_{Y}×1\right)\left(1×{\Delta }_{Y}\right)\left(1×f\right)\left(1×{\epsilon }_{X}{}_{*}\right)\\ & \stackrel{3}{\le }& \left({\epsilon }_{Y}×1\right)\left({\nabla }_{Y}×1\right)\left(1×{\Delta }_{Y}\right)\left(1×{\epsilon }_{Y}{}_{*}\right)\\ & \stackrel{4}{=}& \left({\epsilon }_{Y}×1\right){\Delta }_{Y}{\nabla }_{Y}\left(1×{\epsilon }_{Y}{}_{*}\right)\\ & \stackrel{5}{=}& {1}_{Y}\end{array}$\array{ f f^{op} & \stackrel{0}{=} & f \circ (\varepsilon_Y \times 1)(\nabla_Y\times 1)(1 \times f \times 1)(1 \times \Delta_X)(1 \times \varepsilon_X_\ast) \\ & \stackrel{1}{=} & (\varepsilon_Y \times 1)(\nabla_Y \times 1)(1 \times f \times f)(1 \times \Delta_X)(1 \times \varepsilon_X_\ast) \\ & \stackrel{2}{=} & (\varepsilon_Y \times 1)(\nabla_Y \times 1)(1 \times \Delta_Y)(1 \times f)(1 \times \varepsilon_X_\ast)\\ & \stackrel{3}{\leq} & (\varepsilon_Y \times 1)(\nabla_Y \times 1)(1 \times \Delta_Y)(1 \times \varepsilon_Y_\ast) \\ & \stackrel{4}{=} & (\varepsilon_Y \times 1)\Delta_Y \nabla_Y(1 \times \varepsilon_Y_\ast) \\ & \stackrel{5}{=} & 1_Y }

where (0) uses the definition of ${f}^{\mathrm{op}}$, (1) uses properties of monoidal categories, (2) uses the fact that $f$ strictly preserves comultiplication, (3) is mated to the fact that $f$ laxly preserves the counit, (4) is a Frobenius condition, and (5) uses comonoid and dual monoid laws. We can also “almost” run the same calculation backwards to get the unit:

$\begin{array}{ccc}{1}_{X}& \stackrel{0}{=}& \left({\epsilon }_{X}×1\right){\Delta }_{X}{\nabla }_{X}\left(1×{\epsilon }_{X}{}_{*}\right)\\ & \stackrel{1}{=}& \left({\epsilon }_{X}×1\right)\left({\nabla }_{X}×1\right)\left(1×{\Delta }_{X}\right)\left(1×{\epsilon }_{X}{}_{*}\right)\\ & \stackrel{2}{=}& \left({\epsilon }_{Y}×1\right)\left(f×1\right)\left({\nabla }_{X}×1\right)\left(1×{\Delta }_{X}\right)\left(1×{\epsilon }_{X}{}_{*}\right)\\ & \stackrel{3}{\le }& \left({\epsilon }_{Y}×1\right)\left({\nabla }_{Y}×1\right)\left(f×f×1\right)\left(1×{\Delta }_{X}\right)\left(1×{\epsilon }_{X}{}_{*}\right)\\ & \stackrel{4}{=}& \left({\epsilon }_{Y}×1\right)\left({\nabla }_{Y}×1\right)\left(1×f×1\right)\left(1×{\Delta }_{X}\right)\left(1×{\epsilon }_{X}{}_{*}\right)\circ f\\ & \stackrel{5}{=}& {f}^{\mathrm{op}}f\end{array}$\array{ 1_X & \stackrel{0}{=} & (\varepsilon_X \times 1)\Delta_X \nabla_X(1 \times \varepsilon_X_\ast) \\ & \stackrel{1}{=} & (\varepsilon_X \times 1)(\nabla_X \times 1)(1 \times \Delta_X)(1 \times \varepsilon_X_\ast) \\ & \stackrel{2}{=} & (\varepsilon_Y \times 1)(f \times 1)(\nabla_X\times 1)(1 \times \Delta_X)(1 \times \varepsilon_X_\ast) \\ & \stackrel{3}{\leq} & (\varepsilon_Y \times 1)(\nabla_Y \times 1)(f \times f \times 1)(1 \times \Delta_X)(1 \times \varepsilon_X_\ast) \\ & \stackrel{4}{=} & (\varepsilon_Y \times 1)(\nabla_Y \times 1)(1 \times f \times 1)(1 \times \Delta_X)(1 \times \varepsilon_X_\ast) \circ f \\ & \stackrel{5}{=} & f^{op} f }

where (0) uses comonoid and dual monoid laws, (1) uses a Frobenius condition, (2) uses the fact that $f$ preserves the counit, (3) is mated to the fact that $f$ laxly preserves comultiplication, (4) uses properties of monoidal categories, and (5) uses the definition of ${f}^{\mathrm{op}}$.

In fact, what this proof really proves is a converse of the earlier proposition:

###### Proposition

If $f$ is a strict comonoid morphism, then $f$ has a right adjoint: $f⊣{f}^{\mathrm{op}}$.

###### Proposition

If $f,g:X\to Y$ are maps and $f\le g$, then $f=g$. Thus, the locally full subcategory whose morphisms are maps is locally discrete (the hom-posets are discrete).

###### Proof

A 2-cell inequality $\alpha :f\le g$ is mated to a inequality ${\alpha }_{*}:{g}_{*}\le {f}_{*}$. On the other hand, whiskering ${1}_{Y}×\alpha ×{1}_{X}$ with ${1}_{Y}×{\eta }_{X}$ and ${\theta }_{Y}×{1}_{X}$, as in the construction of opposites above, gives ${\alpha }^{\mathrm{op}}:{f}^{\mathrm{op}}\le {g}^{\mathrm{op}}$. Since ${f}^{\mathrm{op}}={f}_{*}$ and ${g}^{\mathrm{op}}={g}_{*}$, we obtain ${f}^{\mathrm{op}}={g}^{\mathrm{op}}$, and because ${f}^{\mathrm{op}\mathrm{op}}=f$, we obtain $f=g$.

## The Beck-Chevalley condition

Bicategories of relations $B$ satisfy a Beck-Chevalley condition, as follows. Let $\mathrm{Prod}\left({B}_{0}\right)$ denote the free category with finite products generated by the set of objects of $B$. According to the results at free cartesian category, $\mathrm{Prod}\left({B}_{0}\right)$ is finitely complete.

Since $\mathrm{Map}\left(B\right)$ has finite products, there is a product-preserving functor $\pi :\mathrm{Prod}\left({B}_{0}\right)\to Map\left(B\right)$ which is the identity on objects. Again, according to the results of free cartesian category, we have the following result.

###### Lemma

If a diagram in $\mathrm{Prod}\left({B}_{0}\right)$ is a pullback square, then application of $\pi$ to that diagram is a pullback square in $\mathrm{Map}\left(B\right)$.

Let us call pullback squares of this form in $\mathrm{Map}\left(B\right)$ product-based pullback squares.

###### Proposition

Given a product-based pullback square

$\begin{array}{ccc}W& \stackrel{h}{\to }& X\\ k↓& & ↓f\\ Y& \underset{g}{\to }& Z\end{array}$\array{ W & \stackrel{h}{\to} & X \\ k \downarrow & & \downarrow f \\ Y & \underset{g}{\to} & Z }

in $\mathrm{Map}\left(B\right)$, the Beck-Chevalley condition holds: ${h}_{*}k=f{g}_{*}$.

See Brady-Trimble for further details. The critical case to consider is the pullback square

$\begin{array}{ccc}X& \stackrel{\Delta }{\to }& X×X\\ \Delta ↓& & ↓\Delta ×1\\ X×X& \underset{1×\Delta }{\to }& X×X×X\end{array}$\array{ X & \overset{\Delta}{\to} & X \times X \\ \mathllap{\Delta} \downarrow & & \downarrow \mathrlap{\Delta \times 1} \\ X \times X & \underset{1 \times \Delta}{\to} & X \times X \times X }

where the Beck-Chevalley condition is exactly the Frobenius condition.

One way of interpreting this result is by viewing $B$ as a hyperdoctrine or monoidal fibration over $\mathrm{Prod}\left({B}_{0}\right)$, where the fiber over an object $B$ is the local hom-poset $\mathrm{hom}\left(B,1\right)$. Each $f:A\to B$ in the base induces a pullback functor, by precomposing $R:B\to 1$ with $\pi \left(f\right):A\to B$ in $\mathrm{Map}\left(B\right)$. Existential quantification is interpreted by precomposing with right adjoints $\pi \left(f{\right)}_{*}$. The Beck-Chevalley condition exerts compatibility between quantification and pullback/substitution functors.

## Relation to allegories

Any bicategory of relations is an allegory. Recall that an allegory is a $\mathrm{Pos}$-enriched $†$-category whose local homs are meet-semilattices, satisfying Freyd’s modular law:

$RS\cap T\le \left(R\cap T{S}^{\mathrm{op}}\right)S$R S \cap T \leq (R \cap T S^{op})S

A proof of the modular law is given in the blog post by R.F.C. (“Bob”) Walters referenced below.

In fact, we may prove a little more:

###### Theorem

The notion of bicategory of relations is equivalent to the notion of unitary pretabular allegory.

###### Proof

A bicategory of relations has a unit $1$ in the sense of allegories:

• $1$ is a partial unit: we have ${\epsilon }_{1}={\mathrm{id}}_{1}:1\to 1$, and for any $R:1\to 1$ we have $R=R{\epsilon }_{1}\le {\epsilon }_{1}={\mathrm{id}}_{1}$.

• Any object $X$ is the source of a map ${\epsilon }_{X}:X\to 1$, which being a map is entire. Thus $1$ is a unit.

A bicategory of relations is also pretabular, for the maximal element in $\mathrm{hom}\left(X,Y\right)$ is tabulated as $\left({\pi }_{X}{\right)}_{*}{\pi }_{Y}$, where ${\pi }_{X}$, ${\pi }_{Y}$ are the product projections for $X×Y$.

In the other direction, suppose $A$ is a unitary pretabular allegory. There is a faithful embedding, which preserves the unit, of $A$ into its coreflexive splitting, which is unitary and tabular, and hence equivalent to $\mathrm{Rel}$ of the regular category $\mathrm{Map}\left(A\right)$. By the proposition below, then, $A$ is a full sub-2-category of a bicategory of relations. Because the product of two Frobenius objects is again Frobenius, it suffices to show that $A$ is closed under products in its coreflexive splitting. The inclusion of $A$ into the latter preserves the unit and the property of being a map, and hence preserves top elements of hom sets, while any allegory functor must preserve tabulations. So the tabulation $\left({\pi }_{X}^{XY},{\pi }_{Y}^{XY}\right)$ of ${\top }_{XY}$ in $A$ is a tabulation of ${\top }_{{1}_{X}{1}_{Y}}$ in the coreflexive splitting, and hence ${1}_{X×Y}\cong {1}_{X}×{1}_{Y}$.

###### Proposition

If $C$ is a regular category, then the bicategory $\mathrm{Rel}C$ of relations in $C$ is a bicategory of relations.

###### Proof

By theorem 1.6 of Carboni–Walters, $A$ is a Cartesian bicategory if:

• $\mathrm{Map}\left(A\right)$ has finite products.

• $A$ has local finite products, and ${\mathrm{id}}_{1}$ is the top element of $A\left(1,1\right)$.

• The tensor product defined as

$R\otimes S=\left(pR{p}_{*}\right)\cap \left(p\prime Sp{\prime }_{*}\right)$R \otimes S = (p R p_*) \cap (p' S p'_*)

is functorial, where $p$ and $p\prime$ are the appropriate product projections.

The first two are obvious, and for the third we may reason in the internal language of $C$. Clearly

$1\otimes 1=\left[x=x\wedge x\prime =x\prime \right]=1$1 \otimes 1 = [x = x \wedge x' = x'] = 1

The formula whose meaning is by $RS\otimes R\prime S\prime$ is

$\left(\exists y.Rxy\wedge Syz\right)\wedge \left(\exists y\prime .R\prime x\prime y\prime \wedge S\prime y\prime z\prime \right)$(\exists y. R x y \wedge S y z) \wedge (\exists y'. R' x' y' \wedge S' y' z')

and we may use Frobenius reciprocity to get

$\begin{array}{rl}& \exists y.\left(Rxy\wedge Syz\wedge {y}^{*}\exists y\prime .R\prime x\prime y\prime \wedge S\prime y\prime z\prime \right)\\ & \equiv \exists y.\left(Rxy\wedge Syz\wedge \exists y\prime .{y}^{*}\left(R\prime x\prime y\prime \wedge S\prime y\prime z\prime \right)\right)\\ & \equiv \exists y,y\prime .Rxy\wedge Syz\wedge R\prime x\prime y\prime \wedge S\prime y\prime z\prime \\ \end{array}$\begin{aligned} & \exists y. (R x y \wedge S y z \wedge y^* \exists y'. R' x' y' \wedge S' y' z') \\ & \equiv \exists y. (R x y \wedge S y z \wedge \exists y'. y^* (R' x' y' \wedge S' y' z')) \\ & \equiv \exists y, y'. R x y \wedge S y z \wedge R' x' y' \wedge S' y' z' \\ \end{aligned}

which is the meaning of $\left(R\otimes R\prime \right)\left(S\otimes S\prime \right)$. Finally, the Frobenius law is

$\left[\exists x\prime .\left({x}_{1},{x}_{2}\right)=\left(x\prime ,x\prime \right)=\left({x}_{3},{x}_{4}\right)\right]=\left[\exists x\prime .\left({x}_{1},x\prime \right)=\left({x}_{3},{x}_{3}\right)\wedge \left({x}_{2},{x}_{2}\right)=\left({x}_{4},x\prime \right)\right]$[\exists x'. (x_1, x_2) = (x', x') = (x_3, x_4)] = [\exists x'. (x_1, x') = (x_3, x_3) \wedge (x_2, x_2) = (x_4, x')]

which follows from transitivity and symmetry of equality.