Relations with "for each" composition and its properties (coming from profunctors with end composition)

Question

$\newcommand{\sq}{\mathbin{\square}}$The usual composition $S\diamond R$ of two relations $R\colon A⇸B$ and $S\colon B⇸C$ is defined as follows:

• For each $(a,c)\in A\times C$, we declare $a\sim_{S\diamond R}c$ if there exists $b\in B$ such that $a\sim_{R}b$ and $b\sim_{S}c$.

Now, consider the relation $S\sq R$ defined as follows:

• For each $(a,c)\in A\times C$, we declare $a\sim_{S\sq R}c$ if for each $b\in B$, we have $a\sim_{R}b$ and $b\sim_{S}c$.

Intuitively, the composition $\sq$ is quite weird, although its categorical origin is at least natural: categorically, $\diamond$ is a 0-categorical analogue of the coend composition of profunctors, where we view relations as morphisms $R\colon A\times B\to\{\mathtt{true},\mathtt{false}\}$ and then have $$(S\diamond R)^{c}_{a}=\int^{b\in B}S^{c}_{b}\times R^{b}_{a},$$ whereas we have $$(S\sq R)^{c}_{a}=\int_{b\in B}S^{c}_{b}\times R^{b}_{a},$$ where:

• The product $\times$ on $\{\mathtt{true},\mathtt{false}\}:=\{\mathtt{t},\mathtt{f}\}$ is given by logical conjunction;
• The coend $\int^{b\in B}$ is given by $\vee_{b\in B}$, the join in the poset $\{\mathtt{t},\mathtt{f}\}$ equipped with logical implication $\implies$.
• The end $\int_{b\in B}$ is given by $\wedge_{b\in B}$, the meet in $(\{\mathtt{t},\mathtt{f}\},\mathord{\implies})$.

---

1. Has $\sq$ found any natural use in practice?
2. What kinds of nice properties does the 2-category $\mathsf{Rel}^{\sq}$ given by sets, relations and inclusions with the composition $\sq$ has?

For instance, while $\mathsf{Rel}^{\diamond}$ has right Kan lifts and right Kan extensions, $\mathsf{Rel}^{\sq}$ has left ones. Other properties would include whether $\mathsf{Rel}^{\sq}$ is co/complete (1- or 2-categorically), what the adjunctions in $\mathsf{Rel}^{\sq}$ are, etc.

3. Are there any references which study $\sq$ or $\mathsf{Rel}^{\sq}$?
4. (This is slightly outside of the scope of the question, but I'm also interested in profunctors with end composition (and the properties $\mathsf{Prof}$ enjoys with such a composition). I'm sure these have been considered before, and likely the results for those are adaptable to $\mathsf{Rel}^{\sq}$)

Answer 1

Your operation $\square$ defined with $\forall$ and $\land$ is associative, because both $a(R\square(S\square T))d$ and $a((R\square S)\square T)d$ expand to $$ (\forall b_1.\ a R b_1)\land(\forall b_2 c_1.\ b_2 S c_1)\land(\forall c_2.\ c_2 T d). $$ However, it does not define a category unless you restrict to relations between singletons. This is because the unit laws give $$ \forall a_1 a_2 b_1 b_2.\quad a_2 R b_1 \iff a_1 R b_1 \iff a_1 R b_2 $$ for any relation $R$.

A "category" without identities can be turned into a genuine category by taking its idempotents as objects (Karoubi construction), but in this case the idempotents are "constant" relations in the above sense, so there is no improvement.

The only useful ways of forming this composition use $\exists$ with $\land$ or $\forall$ with $\lor$.

I'll leave it to you to adapt this to type-theoretic products and sums or to (co)ends, together with (co)products.

Answer 2

If you define the universal composition with respect to the disjunction, rather than the conjunction, then you do get another category structure as Paul mentioned.

In this case, the identities are different for each category structure. In particular, the identity on a set with respect to the universal composition is the set of all antidiagonal pairs. This shouldn't be surprising if you think about it, because both structures are demorgan duals to each other.

In fact, these two category structures interact laxly according to the Frobenius equations making Rel a linear bicategory. This observation is made on page 6 of Cockett, Kolowski and Seeley. I think this is pretty strong evidence why it is natural to define the one category structure as the De Morgan dual of the other!

The two categorical structures of relations have been secretly used in first order logic for a while, albeit before the advent of category theory. I would recommend reading the article of Bonchi et al. for a good exposition on this side of things, as well as some cool novel work using string diagrams.

Regarding your second point, I must point out that relations are not the same as Bool-enriched profunctors. They are almost the same, but the difference is that in Bool-enriched profunctors, for every enriched category there is an opposite category that need not be the same.

However, generalizing the situation in Rel, it is known that relations valued in a Girard quantale has the structure of a linear bicategory. And it isn't hard to imagine that Girard quantale-enriched profunctors would also have the structure of linear bicategories.