This work develops a suitable data type for plane graph embeddings in Agda. Graphs are used as combinatorial representations for string diagrams, a graphical calculus for monoidal categories. Whenever a monoidal theory does not include any symmetry or braiding operations, it describes processes that are sensitive to their topology. To encode this information in the graphical language, we have to consider surface-embeddings of graphs. We study the simplest case, plane graphs, and present their implementation in Agda. We overcome issues like the cyclic nature of a graph by using one of its spanning trees as an underlying inductive structure. The graphs we implement are plane by construction and any operation on them is guaranteed to preserve this planarity. Additionally, we present a notion of focussing on a certain subgraph within a graph. This operation is crucial for the application of local rewrite rules which themselves are at the centre of diagrammatic reasoning in monoidal categories.

Behavioural distances provide a quantitative approach to comparing the states of transition systems, moving beyond traditional Boolean notions of equivalence. In this paper, we develop a sound and complete axiomatisation of behavioural distance for nondeterministic processes using Milner’s charts, a model that generalises finite-state automata by incorporating variable outputs. Charts provide a compelling setting for studying behavioural distances because they shift the focus from language equivalence to bisimilarity. Their axiomatic study lays the groundwork for quantitative analysis of more expressive models, such as weighted transition systems. To formalise this approach, we adopt string diagrams as our syntax of choice. String diagrams closely mirror the graphical structure of charts, while providing a rigorous formalism that supports inductive reasoning and compositional semantics. Unlike traditional algebraic syntaxes, which require additional mechanisms such as binders and substitution, string diagrams offer a variable-free representation where recursion naturally decomposes into simpler components. This makes them well-suited for reasoning about behavioural distances and aligns with broader efforts to axiomatise automata-theoretic equivalences through a unified diagrammatic framework.

We extend the synthetic theories of discrete and Gaussian categorical probability by introducing a diagrammatic calculus for reasoning about hybrid probabilistic models in which continuous random variables, conditioned on discrete ones, follow a multivariate Gaussian distribution. This setting includes important families of distributions such as Gaussian mixtures, where each Gaussian component is selected according to a discrete variable. We develop a string diagrammatic syntax for distributions of this type, give it a compositional semantics, and equip it with a sound and complete equational theory that characterises when two mixtures represent the same distribution.

The formal theory of monads shows that much of the theory of monads can be developed in the abstract at the level of 2-categories. This means that results about monads can be established once and for all and simply instantiated in settings such as enriched category theory. Unfortunately, these results can be hard to reason about as they involve more abstract machinery. In this paper, we present the formal theory of monads in terms of string diagrams — a graphical language for 2-categorical calculations. Using this perspective, we show that many aspects of the theory of monads, such as the Eilenberg–Moore and Kleisli resolutions of monads, liftings, and distributive laws, can be understood in terms of systematic graphical calculational reasoning. This paper will serve as an introduction both to the formal theory of monads and to the use of string diagrams, in particular, their application to calculations in monad theory.

String diagrams are a graphical language used to represent processes that can be composed sequentially or in parallel, which correspond graphically to horizontal or vertical juxtaposition. In this paper we demonstrate how to compute the layout of a string diagram by folding over its algebraic representation in terms of sequential and parallel composition operators. The algebraic representation can be seen as a term of a free monoidal category or a proof tree for a small fragment of linear logic. This contrasts to existing non-compositional approaches that use graph layout techniques. The key innovation is storing the diagrams in binary space-partition trees, maintaining a right-trapezoidal shape for the diagram’s outline as an invariant. We provide an implementation in Haskell, using an existing denotational graphics library called Diagrams. Our renderer also supports adding semantics to diagrams to serve as a compiler, with matrix algebra used as an example.

String diagrams are powerful graphical methods for reasoning in elementary category theory. Written in an informal expository style, this book provides a self-contained introduction to these diagrammatic techniques, ideal for graduate students and researchers. Much of the book is devoted to worked examples highlighting how best to use string diagrams to solve realistic problems in elementary category theory. A range of topics are explored from the perspective of string diagrams, including adjunctions, monad and comonads, Kleisli and Eilenberg–Moore categories, and endofunctor algebras and coalgebras. Careful attention is paid throughout to exploit the freedom of the graphical notation to draw diagrams that aid understanding and subsequent calculations. Each chapter contains plentiful exercises of varying levels of difficulty, suitable for self-study or for use by instructors.

Bimonoidal categories (also known as rig categories) are categories with two monoidal structures, one of which distributes over the other. We formally define sheet diagrams, a graphical calculus for bimonoidal categories that was informally introduced by Staton. Sheet diagrams are string diagrams drawn on a branching surface, which is itself an extruded string diagram. Our main result is a soundness and completeness theorem of the usual form for graphical calculi: we show that sheet diagrams form the free bimonoidal category on a signature.