I was trying to add in duals to the theory, and I ran into some trouble. The fix seems to be something I’d considered a little earlier for a possible generalization, but it seems that duals force the issue. We need to tweak our definition of spans.
Now, most of the definition is fine as it stands. Our objects are just the same as in , and our 1-morphisms are spans . When I first (re)invented these things, I stopped at this level. I handled the associativity not with 2-morphisms, but with defining two spans and to be equivalent if there was an isomorphism so that and . Then I said that the 1-morphisms were equivalence classes of spans, giving me a 1-category.
Now still sits inside this category I’ll call . Indeed, if we use the same inclusion as before, the only way two arrows of can be isomorphic in (and thus equal in ) is for them to be equal already in .
But we want to pay attention to those 2-morphisms, and that’s where things start to get interesting. See, those arrows are nice as 2-morphisms, but they’re not very.. “spanny”. Instead, let’s define a 2-morphism from to to be itself a span satisfying and . Here’s the picture:
Now, we handle the associativity at the 2-morphism level by cutting off the same way we did in and say that a 2-morphism is really an equivalence class of spans. This makes the vertical composition of 2-morphisms just the same pullback construction as for the composition of 1-morphisms.
The horizontal composition of these 2-morphisms gets tricky. Here’s another picture:
Here we have our two 2-morphisms and we’ve already pulled back to get the 1-morphisms for the source and target of the composition. We write for the composite , and similarly on the other side.
Now we can pull back the diagram to get an object with arrows to and . If we follow these arrows, then up to and (respectively) the universal property of gives us a unique arrow from to . Similarly, we have a unique arrow from to . These arrows make the required squares commute, and so define a span from to which is our composite 2-morphism.
When we compose two spans, again we only have associativity up to isomorphism. In , this becomes an equality, so we’re fine. In we made this isomorphism a 2-morphism between the two composite spans. Now in we can make this isomorphism into one leg of a span 2-morphism, and everything works out as before. The exchange identity for the two compositions of 2-morphisms also works out, but it’s even more complicated than the definition of horizontal composition.
Seriously, does anyone know of a tool that will render commutative diagrams in 3-D, like with Java or something? This is getting ridiculous.
Anyhow, I think now I can throw away the request that the monoidal structures on play nice with the pullbacks. Unfortunately, it’s getting a lot more complicated now and I have other real-world obligations I’ve got to attend to. So I think I’ll back-burner this discussion and move back to something old rather than spend too much time working this stuff out live as I have been doing.