Double categories

Perhaps the most fundamental idea in category theory is internalisation. This lets you take some concept familiar from classical mathematics and set theory, and then turn it into an internal concept in some category. With a sufficiently advanced category, with a powerful enough internal language like a topos, you can really remake all mathematics internal to that category. This creates a different perspective on everything.

A particular example of internalisation is that of a double category. This is a category internal to the category of categories $Cat$. These double categories are the first in a line of different types of n-fold categories. Looking back at it now, I believe these n-fold categories, categories internal to the category of categories, are more fundamental then bicategories because internalisation is more interesting and fundamental then enrichment.

I want to escape from set-theoretic preconceptions which are still so ubiquitous even as category theory gains traction. The only way I think that you can do that is through internalisation, and the concept of mathematics internal to some category other then $Sets$. If you just go with enrichment, then you have all the assumptions about $Set$-categories packed in, you are just adding on more structure to the $Set$-category without doing anything really different.

Perhaps you could then do enriched category theory internal to a given category, e.g internal enriched category theory. That would resolve all issues. But the point is that this internalisation notion is more fundamental, and you want a bit of it even if you do enriched category theory. This gives me the impression that double categories are more fundamental then category enriched categories.

The perception that double categories are more fundamental then 2-categories is formalised by the notion that any 2-category can be converted in to a double category. This can be achieved by defining the horizontal or the vertical morphisms of the double category to be identities. So an advantage of a double-categorical framework is that it can subsume 2-categories as a special case.

Double categories:
A category internal to the category of categories $Cat$ is a structure $C$ that has six components:

• A category of objects $Ob(C)$
• A category of morphisms $Arrows(C)$
• A source functor $S: Arrows(C) \to Ob(C)$
• A target functor $T: Arrows(C) \to Ob(C)$
• An identity functior $id: Ob(C) \to Arrows(C)$
• A composition functor $\circ: Arrows(C) \times_{Ob(C)} \times Arrows(C) \to Arrows(C)$.

The key takeaway is that for any category $C$ then the category of its commutative squares $Sq(C)$ forms a double category. This formalizes the fact that commutative squares can be composed either horizontally or vertically. This is a very important part of the theory of commutative squares.

References:
Double categories