lin-0021

0.6 Reading coherent change in two dimensions

There are two standard two-dimensional ways to depict the data of \(\mathbf{CAT}\). The first raises the directed diagrams of Section 0.3 by one categorical dimension. In the pasting scheme associated with Bénabou, categories are vertices, functors are directed edges, and a natural transformation is a 2-cell drawn between parallel functor edges [ Bénabou , 1967 ] . This convention remains common in category theory texts; see, for example, Riehl [ 2017 ] .

Street’s string-diagram convention gives the planar dual picture [ Street , 1996 ] . Natural transformations become vertices or boxes, functors become the wires incident on them, and categories become the regions separated by those wires. Vertical stacking expresses composition of natural transformations, while horizontal attachment expresses whiskering by a functor. Nothing mathematical has changed: the two drawings encode the same typed 2-cell, but make different dimensions visually prominent.

This second graphical language belongs to the calculational tradition developed by Marsden and subsequently presented systematically by Hinze and Marsden [ Marsden , 2014 , Hinze and Marsden , 2023 ] . It treats category theory itself diagrammatically, including natural transformations, adjunctions, monads, and Kan extensions. Cockett and Cruttwell specialize the calculus to tangent-category reasoning, using it to simplify calculations with tangent functors, lifts, flips, and Lie brackets [ Cockett and Cruttwell , 2015 ] . The diagrams in this book specialize it once more: they form a LINCS dialect for displaying structural declarations, observers, obstructions, coherent repairs, and their transport.

Figure 1 compares the two conventions and then fixes the Street convention used in this book: functors point from the region on the left to the region on the right, and 2-cells are read from bottom to top. The first two panels depict the same 2-cell \(\eta :F\Rightarrow G\). The third gives its first LINCS reading. A fixed-sketch repair \(\rho :D\Rightarrow D'\) is not a collection of unrelated component edits; it is one coherent change between two realization functors.

Two planar presentations of the same 2-cell, followed by its LINCS reading. The Street diagram is the planar dual of the pasting scheme: categories move from vertices to regions and the 2-cell moves from an arrow between parallel edges to a vertex on a wire. Region colors are… — Figure 1 Two planar presentations of the same 2-cell, followed by its LINCS reading. The Street diagram is the planar dual of the pasting scheme: categories move from vertices to regions and the 2-cell moves from an arrow between parallel edges to a vertex on a wire. Region colors are pedagogical; the typing is carried by the category and functor labels.

This notation supplements rather than replaces the other diagram languages in the book. A commutative diagram displays obligations among objects and morphisms. A monoidal string diagram displays processes, tensor products, copying, and discarding. A \(\mathbf{CAT}\)-diagram displays coherent changes of whole structured systems. The distinction matters: moving a box through a crossing is licensed only when the corresponding 2-categorical coherence law has been stated.

Design principle

Use graphical deformation only as a typed proof step. A visually smooth redrawing is not evidence of equality unless the relevant naturality, interchange, or tangent-coherence law licenses it.