Let's imagine how a given category is a monad in a bicategory of spans.
Consider the set of all the objects in the category C0
and the set of all the morphisms in the category C1
(they're all muddled together in this set). We have two functions domain : C1 -> C0
and codomain : C1 -> C0
which assign to each morphism its source and target object.
This pair of functions forms a "span" of sets, which is a diagram of this shape:
C_1
╱ ╲
dom cod
╱ ╲
V V
C_0 C_0
Moreover, it forms a span where the sets at both tips are identical: C0
. Abusing notation, I will refer to a span by the set that occurs in the middle, and give it a "type" as an arrow between the sets it has at its tips. Hence the span above will be written: C1 : C0 -/-> C0
(you are left to figure out the actual pair of functions from context).
We can "compose" this span with itself to get another span in a certain way. Here is how: first we identify the set of pairs of morphisms (f, g) : C1 x C1
where the following equation is true: codomain(f) = domain(g)
. Let's call this set D_1
. Now we can make a span with C0
at the tips and D_1
in the middle:
D_1
╱ ╲
fst snd
╱ ╲
V V
C_1 C_1
╱ ╲ ╱ ╲
dom cod dom cod
╱ ╲ ╱ ╲
V V V V
C_0 C_0 C_0
------------- ↓↓↓ ---------------
D_1
╱ ╲
dom.fst cod.snd
╱ ╲
V V
C_0 C_0
Thus we have an operation on spans composeSpan : (C0 -/-> C0) x (C0 -/-> C0) -> (C0 -/-> C0)
, such that composeSpan(C1, C1) = D1
.
In fact spans of arbitrary sets can be composed whenever they share a tip, i.e. we can write more generally that: composeSpan : (Y -/-> Z) x (X -/-> Y) -> X -/-> Z
, for some sets X, Y, Z
. The formula for this composition is the same as shown above: we take the middle set of the resulting span to be the subset of pairs (f, g) : F x G
which satisfy the equation F2(f) = G1(g)
(where F
and G
are the middle sets of the spans we are composing and F2, G1
are the legs of the respective spans pointing to the shared tip).
In addition to the C1 : C0 -/-> C0
span that we discussed above, we can also construct an "identity" span whose middle only consists of the identity morphisms of the category. Since there's exactly as many identity morphisms as there are objects in the category, we can just represent this set of identity morphisms by C0
itself. So we end up with the rather unimpressive identity span C0 : C0 -/-> C0
, whose legs are:
C_0
╱ ╲
id id
╱ ╲
V V
C_0 C_0
Now here is where the "monad" word comes in. In the bicategory of categories, our familiar monads are endofunctors that go from a category to itself (hence can be composed with themselves to give another endofunctor on the same category), and which have a pair of natural transformations: return : Identity ~> M
and join : composeMonad(M, M) ~> M
(plus some laws, but I'm too tired now).
In the bicategory of spans over sets, sets take the place of categories, spans take the place of endofunctors, and "span morphisms" between spans of the same tips take the place of natural transformations between functors of the same categories. What is a morphism between spans you ask? Well imagine two spans which have the same tips: X, Y : A -/-> B
. Pictorially:
X
╱ ╲
f_x g_x
╱ ╲
V V
A B
Y
╱ ╲
f_y g_y
╱ ╲
V V
A B
We can avoid repeating ourselves if we draw the bottom span upside down:
X
╱ ╲
f_x g_x
╱ ╲
V V
A B
^ ^
╲ ╱
f_y g_y
╲ ╱
Y
A morphism of spans f : X ~> Y
is simply a function between the underlying middle sets of the spans such that when you draw it on the picture above, the diamond is bisected into two triangular equations that are satisified:
X
╱ | ╲
f_x | g_x
╱ | ╲
V | V
A f B
^ | ^
╲ | ╱
f_y | g_y
╲ V ╱
Y
f_x = f_y . f
g_x = g_y . f
Ok, great, so now we know what a span morphism is. Here is our checklist for what a monad in the bicategory of spans requires:
- A span that goes from a set to itself (
C1 : C0 -/-> C0
) - A span morphism that goes from the identity span to the specified monad:
C0 ~> C1
- A span morphism that flattens a self-composition of the specified monad:
composeSpan(C1, C1) ~> C1
Where do we get the last two things?
Well, can you think of a function C0 -> C1
that picks out a morphism for every object, and another function D1 -> C1
that assigns a pair of morphisms (f, g) : C1 x C1
where codomain(f) = domain(g)
to a new morphism from C1
?
TODO: Laws