
At long last, here we are. We’ve explored categories, internal categories, and functors, all to be able to look at the flavour of category that I have been focused on for the last couple of years: double categories. So, here we go…
“A double category is a category with two kinds of morphisms”
…is something I might say if I had three minutes or less to talk about my research (this is also something I could have introduced in my second post, right after introducing categories). But this “definition” really doesn’t do double categories justice in my opinion, and at this point, I’ve been building it up for far too long to feel okay accepting such an unsatisfying punch line, and I hope that you feel the same way.
So let’s approach this from a different angle. Remember the diagram for internal categories that we came up with two posts ago, and imagine that we interpret it as being inside the category of categories from last time:

Let’s look at C0 first. Since we’re operating inside the category of categories, C0 is just a category with objects and arrows. Actually, C1 is too, but its objects and arrows have some additional meaning because of s and t.
Interpreting the s and t arrows, which would be functors in this context, this means that each object in C1 is assigned to two objects in C0. Following how we interpreted this when we first came up with this diagram, we can think of this as meaning that each object in C1 has a source and a target, making them morphisms in a sense. These are distinct from the arrows in C0 though, so this structure has two different types of morphisms.
We can think of this latter type of morphisms as being “external” in some sense, since they don’t act as morphisms inside their home of C1, and are only interpreted that way because of the added context of s and t. This is in contrast to the “internal” morphisms that are explicitly part of C0. When drawing diagrams of parts of structures like this we typically distinguish between the two types on morphisms by adding a dash to the stem of the external morphisms.
So for example, the i arrow, which assigns identity arrows to each object of C0, in this case assigns external identity arrows to each of those objects, in addition to the internal ones that already exist due to C0 being a category.
You may have noticed that if the objects of C1 are considered to be “arrows” in the above sense, then the morphisms of C1 are somehow “arrows between arrows”! But what does that look like?
Well, we could simply draw exactly that: an arrow between two arrows, and use a doubled arrow to distinguish between the two types of arrows involved here.

This doesn’t give the whole picture though. Since we are operating in the category of categories, s and t are both functors, and functors preserve arrows as well as objects. What this means for us is that this “arrow between arrows” also has a source and target, which are morphisms of Co i.e. arrows in our double category. If you follow everything through, you find that those arrows fit in the top and bottom of our little diagram, leaving us with a box like this:
The remaining conditions on our diagram essentially amount to making sure that the external morphisms have the properties that we would expect of them in a category.
This is all well and good, but what do double categories actually do for us? Well, I’ll be the first to admit that my interest in double categories is for more esoteric reasons (and don’t worry, we’ll get to those), but double categories can generally be applied in situations where one cares about some collection of objects, and two distinct but related ways of relating these objects to one another. Taking the flight map example from a couple posts ago, we could create a double category from that by adding new arrows between cities A and B whenever it is possible to travel from A to B by car, plus some intuitive compatibility conditions for travel paths that use both planes and cars.
But I’m looking for something a little more abstract from my double categories. In essence, I want to be able to talk about different flavours of logic using the language of double categories, in much the same way that we’ve used the language of categories to talk about categories, which is how we got to our diagram for an internal category. But what do I mean by “logic” if it‘s something that can have “different flavours”? Well, I’m nearly out of space, so that’ll have to wait for next time.