### 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

Relof 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 becauseRelis its own dual, whereasSetandCpoare 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 inRel.

(c) Show that disjoint sum is in fact also a categorical product inRel.

(d) Show, using converses, that any categorical product inRelis 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 = gDisjoint 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...?

<< 回到主頁