After more delays that I would like to admit, I finally got around to making this. Perhaps some explanation of what’s going on in the picture is in order. We begin with a category with (all) pushouts, starting with some objects and morphisms arranged as chained spans. A pushout is used to compose the two spans on the left. This gives a new span, , which in turn can be composed with the span to its right via pushout. This is just one way that we can compose the chain of three spans. If we had built up from right to left instead of left to right, we would have at the top instead of .
The associative property is really nice, so it would be good to show those two ways of composing spans are “the same” in some appropriate sense. Spoiler: that sense is “up to isomorphism.” Instead of directly finding them isomorphic to each other, it is easier to show each is isomorphic to some other thing – the colimit of the entire diagram we started with. This colimit will here be called an associator; it is something that both compositions of all three spans will be isomorphic to. I’m just going to sweep under the rug the question of whether that colimit will exist and just assume it does in this post.
So we’ve got the groundwork set, now we need to take advantage of some universal properties to give unique maps that make sub-diagrams commute. The first universal property taken advantage of is that of the first pushout. The associator has arrows going to it from and , so there will exist a unique morphism, . such that everything commutes. Going up a step and using the arrow we just made, we can play the same game to get a unique morphism that still makes everything commute.
To go in the reverse direction, we need morphisms from each of the Gammas to . We already have one from , and the other two can be built by composing morphisms. We can join two arrows together, tail to tip, to get a single arrow regardless of what category we are in. Now the universal property of the associator kicks in, giving a unique morphism , but there’s a catch. We only know it makes some of the diagram commute. We have to put in a bit more effort to show the arrows involved in the pushouts will commute, too. The first step of this isn’t too bad — the three arrows that don’t point directly at will commute because the morphisms from and to commute with them by construction.
The universal pushout maps are a bit trickier, but since both legs of the pushouts commute with everything else, the universal maps will commute as well. Without the picture, that sentence might be a bit hard to understand. Look at the picture. They say those things are worth a thousand words. As parts of the diagram are shown to commute with the blue arrow on top, those part turn dark green. The arrows that already commute with everything get highlighted when they are used to show other arrows commute with everything. That should clarify what the picture is doing. Once everything commutes, the arrows turn black again, and we are left with unique maps in both directions at the top of the diagram that commute with each other. Long story short, this gives an isomorphism between the composition of spans by pushouts and the composition of spans “all at once” by associator. Watching the animation in a mirror gives the other way of composing spans by pushouts as isomorphic to this as well.
So this picture together with its mirror image shows , which is really the best we could possibly hope for when pushouts themselves are only unique up to isomorphism.