$\newcommand{\defeq}{\mathrel{\mathop:}=}$

## 2008/04/07

### Coincidence of Products and Coproducts in Rel

I've seen a lot of times that categorical products and coproducts coincide in Rel, and it seems that I should formally work it out at least once. The exercise description below is taken from Bird, Gibbons, and Mu, adapted to the style of AoP:

A straightforward interpretation in Rel of the standard theory of datatypes from Chapter 5 (about functional derivation) is inappropriate: products and coproducts coincide, whereas we intend them to be different constructions. Technically, this is because Rel is its own dual, whereas Set and Cpo are not self-dual.

Categorically speaking, bifunctor ⊗ is a product if arrows f : B ← A and g : C ← A uniquely determine a morphism h : B ⊗ C ← A with outl . h = f and outr . h = g. Dually, bifunctor ⊕ is a coproduct if arrows f : C ← A and g : C ← B uniquely determine a morphism h : C ← A ⊕ B with h . inl = f and h . inr = g.

(a) Show that cartesian product is not a categorical product in Rel.
(b) Show that disjoint sum is a categorical coproduct in Rel.
(c) Show that disjoint sum is in fact also a categorical product in Rel.
(d) Show, using converses, that any categorical product in Rel is necessarily a coproduct, and vice versa.

Cartesian product is not a categorical product since partiality emerges in Rel. For example, taking f = ∅ and g = id, we have

split f g = ∅

and now the cancellation law fails to hold:
outl . split f g = ∅ ≠ id = g

Disjoint sum is, however, still a categorical coproduct, which can be easily verified by the definitions of relation composition and join.

Now we have coproducts in Rel. To show that products and coproducts coincide, we define <f, g> = [fº, gº]º, outl = inlº, outr = inrº and reason:

(The proof actually starts in the middle and goes dually towards the top and the bottom.) The arrow <fº, gº> has type B + C ← A if fº : B ← A and gº : C ← A and is unique since [f, g] is. Therefore a coproduct in Rel is also a product and vice versa. In particular, disjoint sum is both a product and a coproduct. One can easily see that it is converse which makes Rel dual to itself and causes the coincidence.

--
Why am I feeling that the logic is a bit strange...?