Adam Lobski and Fabio Zanasi (“String Diagrams for Layered Explanations”) give an algebra of explanation, in which a system is described at several levels at once and the movement between levels is itself part of the diagrammatic structure. That movement is the act of explaining.
A layered prop is the 2-category presented by a layered monoidal theory, a family of props, one per level of description, whose generators and equations may differ level by level. Two adjacent levels are connected by a refinement
Explanations are packaged as special diagram shapes. A window descends one level, applies the finer level’s more flexible rewrite rules, and returns. It gives a reductive explanation, in which a coarse box is understood by what it becomes underneath. A cowindow is a functorial box that pushes structure the other way, a functional explanation of a fine mechanism by the coarse role it plays.
Example. Window as reductive explanation
To justify a coarse-level equation, open a window into the level below, where the two sides both refine to diagrams that the finer rules identify; closing the window transports the equality back up. The coarse law holds because of the finer mechanism, and the window records exactly that dependence.
Remark. Adjointness of the levels
Windows and cowindows compose coherently because
and are adjoint monoidal profunctors. Descending then ascending is comonad-like, whereas ascending then descending is monad-like, so layered explanations stack without ambiguity across many levels.