Instantly share code, notes, and snippets.

masaeedu/catspan.md

Last active June 9, 2020 16:19
Show Gist options
• Save masaeedu/3e1ba2b7e206837d76343239e0eaa517 to your computer and use it in GitHub Desktop.
Categories are just monads in the bicategory of spans, what's the problem?

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

to join this conversation on GitHub. Already have an account? Sign in to comment