Double Category

A double category has objects with two kinds of morphism, horizontal and vertical 1-cells, together with squares whose four sides are two horizontal and two vertical 1-cells. Each kind of 1-cell composes on its own, and squares compose in both directions. The interchange law constrains this, since the two orders of composing a grid of squares must agree. Equivalently it is a category internal to . The horizontal 1-cells with squares form a bicategory of “loose” processes, whereas the vertical 1-cells form an ordinary category of “tight” maps, and a square says how a process transforms along tight maps.

Example. Matrices over an ordered semiring

Fix an ordered semiring . In the objects are finite sets, a horizontal 1-cell is an -valued matrix (composing by ), a vertical 1-cell is a function, and a square with legs exists iff pointwise. Squares are unique when they exist, so is poset-enriched. Interchange holds cleanly only when addition is idempotent (); additive semirings satisfy it laxly. Boolean recovers ; counts, weights, and max-plus / min-plus give longest- and shortest-path composition.

Example. Spans and profunctors

Replacing the scalar entries by sets turns the same shape into the double category whose horizontal 1-cells are profunctors (or spans), the setting where composable processes sit over a category of functions. This is the shape behind optics and lens categories.

References

• Charles Ehresmann, “Categories structurees”, Ann. Sci. Ecole Norm. Sup. 80 (1963)
• Marco Grandis, Robert Pare, “Limits in double categories”, Cah. Topol. Geom. Differ. Categ. 40 (1999)