Double categories

$\def\sh{\source{\text s}\black{\text{-h}}} \def\th{\target{\text t}\black{\text{-h}}} \def\sv{\source{\text s}\black{\text{-v}}} \def\tv{\target{\text t}\black{\text{-v}}}$ $\bbox[navajowhite,24px,border:4px groove red]{\begin{array}{} \cdotp & \source{\xrightarrow{\textstyle\sv}} & \cdotp \\ \llap\sh \source{\big\downarrow} & & \target{\big\downarrow} \rlap\th\\ \cdotp & \target{\xrightarrow[\textstyle\tv]{}} & \cdotp \end{array}}$

Loosely, a "double category" is a collection of abstract "squares",
of the form shown in the box at right.
Going either vertically or horizontally they form a category, with composition and identities.
Further, the compositions are compatible, a condition called the interchange law,
meaning that if four of them form a compatible 2x2 square, then
performing first horizontal, then vertical composition yields the same result as
performing first vertical, then horizontal composition.
That is a "symmetrical" definition of a double category.

There is also an unsymmetrical definition, which is also useful in many situations.
It defines a double category as an (internal) category in the category of categories, $\Cat$.

To best understand it we should briefly review the definition of internal category.
It starts with the notion of a graph in a category,
namely a diagram in that category of the form $$\begin{array}{} X_0 & \mathop\leftleftarrows\limits^{\source s}_{\target t} & X_1\end{array}$$ Here $X_0$ is the "object of objects" and $X_1$ is the "object of arrows" of the category,
and the two arrows provide the source and target for the "arrows" in $X_1$.
A morphism of such graphs is a diagram of the form $$\begin{array}{} X_0 & \mathop\leftleftarrows\limits^{s_X}_{t_X} & X_1\\ \llap{f_0}\big\downarrow && \big\downarrow\rlap{f_1}\\ Y_0 & \mathop\leftleftarrows\limits^{s_Y}_{t_Y} & Y_1\\ \end{array}$$ which serially commutes, meaning that $s_X f_0 = f_1 s_Y$ and $t_X f_0 = f_1 t_Y$.
(If we view a graph $X$ in a category as
a functor $X$ from the abstract graph shape $\leftleftarrows$ to the category,
then this condition amounts to saying
$f$ is a natural transformation from the functor $X$ to the functor $Y$.)
Finally, to make a graph $X$ a category,
there must be defined a composition operation and an identity operation for the graph.
(We skip the details, see CWM, Chapter II, Section 7
or references on the web.)

Let use that definition to define an internal category in the category of internal categories (internal to the category of small sets, $\Set$).
It has an underlying graph of the form (drawn vertically for reasons soon to appear) $$\begin{array}{} C_1\\ \llap\sv\source{\big\downarrow}\target{\big\downarrow}\rlap\tv\\ C_0 \end{array}$$ Since this is a diagram of internal categories,
$C_0$ and $C_1$ are themselves categories internal to $\Set$,
and $\sv$ and $\tv$ are internal functors, thus also graph morphisms, from $C_1$ to $C_0$.
Expanding the definitions, we have a diagram in $\Set$ $$\bbox[navajowhite,10px,border:4px groove red]{\begin{array}{} V & = & (C_1)_0 & \mathop\leftleftarrows\limits^{\source{\textstyle\sh}}_{\target{\textstyle\th}} & (C_1)_1 & = & \{\,\text{squares}\,\}\\ & & \llap\sv\source{\big\downarrow} \target{\big\downarrow}\rlap\tv & & \llap\sv\source{\big\downarrow} \target{\big\downarrow}\rlap\tv \\ \{\,\text{0-cells}\,\} & = & (C_0)_0 & \mathop\leftleftarrows\limits^{\source{\textstyle\sh}}_{\target{\textstyle\th}} & (C_0)_1 & = & H\\ \end{array}}$$ which serially commutes
(i.e., when matching top and bottom, and left and right, arrows are paired;
there are four such pairs, to be depicted momentarily).
The reasons for the $V$ and $H$ will also appear momentarily.

Okay, that diagram gives the internal category representation of this structure.
But now let us redraw that same data in a form which shows how this gives
the source and target operations for squares,
and explicitly shows the four squares (in $\Set$) required to commute to give serial commutativity.
Specifically: $$\bbox[navajowhite,10px,border:4px groove red]{\begin{array}{} \\ &&& H\\[-4ex] &&& \parallel\\[-4ex] & (C_0)_0 & \source{\xleftarrow{\textstyle\sh}} & (C_0)_1 & \target{\xrightarrow{\textstyle\th}} & (C_0)_0\\ & \llap{\textstyle\sv}\source{\big\uparrow} && \llap{\textstyle\sv}\source{\big\uparrow} && \source{\big\uparrow}\rlap{\textstyle\sv}\\ V =\!\!\! & (C_1)_0 & \source{\xleftarrow{\textstyle\sh}} & (C_1)_1 & \target{\xrightarrow{\textstyle\th}} & (C_1)_0 & \!\!\!= V\\ & \llap{\textstyle\tv}\target{\big\downarrow} && \llap{\textstyle\tv}\target{\big\downarrow} && \target{\big\downarrow}\rlap{\textstyle\tv}\\ & (C_0)_0 & \source{\xleftarrow[\textstyle\sh]{}} & (C_0)_1 & \target{\xrightarrow[\textstyle\th]{}} & (C_0)_0\\[-2ex] &&& \Vert\\[-2ex] &&& H\\ \end{array}}$$ So we have:
$(C_1)_1$ = the set of all the squares,
$(C_1)_0$ = the set of all the vertical arrows, which we may call $V$,
$(C_0)_1$ = the set of all the horizontal arrows, which we may call $H$, and
$(C_0)_0$ = the set of all the 0-cells,
and $\sv$, $\tv$, $\sh$, and $\th$ give the source-target operations at all the requisite levels.

---

The sketch for the last display:  

$$\bbox[navajowhite,10px,border:4px groove red]{\begin{array}{} \\ &&& H\\[-4ex] &&& \parallel\\[-4ex] & (0,0) & \source{\xleftarrow{\textstyle (s,0) }} & (1,0) & \target{\xrightarrow{\textstyle (t,0) }} & (0,0) \\ & \llap{\textstyle (0,s) }\source{\big\uparrow} && \llap{\textstyle.(1,s)}\source{\big\uparrow} && \source{\big\uparrow}\rlap{\textstyle (0,s) }\\ V =\!\!\! & (0,1) & \source{\xleftarrow{\textstyle (s,1)}} & (1,1) & \target{\xrightarrow{\textstyle (t,1)}} & (0,1) & \!\!\!= V\\ & \llap{\textstyle (0,t) }\target{\big\downarrow} && \llap{\textstyle (1,t)}\target{\big\downarrow} && \target{\big\downarrow}\rlap{\textstyle (0,t) }\\ & (0,0) & \source{\xleftarrow[\textstyle (s,0) ]{}} & (1,0) & \target{\xrightarrow[\textstyle (t,0) ]{}} & (0,0) \\[-2ex] &&& \Vert\\[-2ex] &&& H\\ \end{array}}$$

<hr />

The sketch folded, i.e.

the endospan replaced by a parallel pair.

$$\bbox[navajowhite,10px,border:4px groove red]{\begin{array}{} V = \!\!\! & (0,1) & \mathop\leftleftarrows\limits^{\textstyle \source {(s,1)}}_{\textstyle \target {(t,1)}} & (1,1)  &  \!\!\!  =  C  \\ & \llap{\textstyle (0,s) } \source{\big\downarrow} \target{\big\downarrow} \rlap{\textstyle (0,t) }  && \llap{\textstyle (1,s)} \source{\big\downarrow} \target{\big\downarrow} \rlap{\textstyle (1,t)} \\ O  = \!\!\! &  (0,0) & \mathop\leftleftarrows\limits^{\textstyle \source {(s,0)}}_{\textstyle \target {(t,0)}} & (1,0) &  \!\!\!  = H  \\ \end{array}}$$