A (strict) double category is a category internal to the category \mathsf {Cat} of categories.
Concretely, it consists of:
A set of objects \operatorname {\mathbf {ob}} \mathbb {C}
A collection of vertical morphisms forming a category \mathbb {C}_v with \operatorname {\mathbf {ob}} \mathbb {C}_v = \operatorname {\mathbf {ob}} \mathbb {C}
A collection of horizontal morphisms forming a category \mathbb {C}_h with \operatorname {\mathbf {ob}} \mathbb {C}_h = \operatorname {\mathbf {ob}} \mathbb {C}
An a collection of squares. Each square has a left and right boundary given by vertical morphisms l,r, and top and bottom boundary given by horizontal morphisms t,b so that \operatorname {\mathrm {dom}} t = \operatorname {\mathrm {dom}} l, \operatorname {\mathrm {cod}} t = \operatorname {\mathrm {dom}} r and so on:
The squares compose horizontally and vertically in the obvious way, each of which form a category (in particular, there are identity squares for each vertical and horizontal map).
A double functor is a mapping on objects, vertical and horizontal morphisms, and squares, which preserves all the identities and composition.
