Double categories

Question

So, I wanted to ask a question about double groupoids until I find myself having the answer, meanwhile I wrote a lot of stuff about double categories, so I decided to create a question and answer my own question:

what is a double category?

---

I put it here so others can correct me if I'm wrong or benefit from this definition.

Answer 1

A double category is a category internal to $\mathsf{Cat}$, namely:

1. A category $C_0=(C_0^0,C_0^1,s_0,t_0,\circ_0,id_0)$ of objects
2. A category $C_1=(C_1^0,C_1^1,s_1,t_1,\circ_1,id_1)$ of morphisms
3. Two functors $s,t:C_0\rightarrow C_1$ which then define two (pairs of) maps $s^0,t^0:C_0^0\rightarrow C_1^0$ and $s^1,t^1:C_0^1\rightarrow C_1^1$ called the object (resp. arrow) maps of source (resp. target) functors
4. A partial functor $\circ:C_1\times C_1\rightarrow C_1$ which then defines two maps $\circ:C_1^0\times C_1^0\rightarrow C_1^0$ and $\circ:C_1^1\times C_1^1\rightarrow C_1^1$ called the object (resp.arrow) map of composition functor
5. A functor $id:C_0\rightarrow C_1$ which defines two maps $id:C_0^0\rightarrow C_1^0$ and $id:C_0^0\rightarrow C_1^0$ called the object (resp. arrow) maps of the identity functor

With certain axioms defining the category structure.

These axioms with the three last properties permit to define two other categories defining a double category:

3'. A category $(C_0^0,C_0^1,s_0,t_0,\circ_0,id_0)$

4'. A category $(C_0^0,C_0^1,s_0,t_0,\circ_0,id_0)$

Thus, 1, 2, 3' and 4' fully define a double category:

• What are called horizontal morphisms are objects in $C_1$ (I like calling them morphisms's objects) between objects in $C_0$ (I call them objects's objects)
• What are called vertical morphisms are morphisms in $C_0$ (objects's morphisms) between objects in $C_0$ (objects's objects)
• What are called 'squares' or '2-cells' are a couple of morphisms: objects in $C_1$ (morphisms's objects) between objects in $C_0$ (objects's objects) and morphisms in $C_1$ (morphism's morphisms) between morphisms of $C_0$ (objects's morphisms)

The first two morphisms come from the fact that the "collection" of objects and morphisms of that category are categories themselves.

The last two morphisms come from the category structure of $C$ and from the fact that the composition map is in fact a functor (it has object and arrow maps)

Composition

• Composition of H-morphisms is $\circ^0$ (composability is guaranteed by $s^0,t^0$)
• Composition of V-morphisms is $\circ_0$ (composability is guaranteed by $s_0,t_0$)
• H-composition of squares is $\circ^1$ (composability is guaranteed by $s^1,t^1$)
• V-composition of squares is $\circ_1$ (composability is guaranteed by $s_1,t_1$)

Diagrammatic

A single square is depicted by:

$\alpha$ must not be seen as going from $x$ to $y'$ but from the edge containing H-morphisms $f$ and $\tilde{f}$ to the one containing V-morphisms $g$ and $\tilde{g}$

Answer 2

A double category consists of a set [or class] of squares, a set of horizontal arrows, a set of vertical arrows and a set of points, boundary information of these, and associative horizontal and vertical composition of squares and arrows, admitting local unit elements,

$ \ \longrightarrow \longrightarrow \\ \downarrow\alpha\downarrow\beta\downarrow \\ \ \longrightarrow \longrightarrow \\ \downarrow\varphi\downarrow\psi\downarrow \\ \ \longrightarrow \longrightarrow \quad\quad$ such that $ \quad\quad\displaystyle\frac\alpha\varphi|\frac\beta\psi = \frac{\alpha\,|\ \beta}{\varphi\,|\ \psi} \quad$ for all composable setting of squares.