String diagrams are a well established graphical syntax for morphisms in monoidal categories. Reasoning with arrows in a category can be implemented as an instance of diagrammatic
reasoning in its graphical language. This thesis presents work on string diagrams for monoidal categories that do not necessarily
contain a symmetry map, that is, a SWAP operation of two wires across each other. While abstract graphs provide a suitable combinatorial structure for string diagrams of symmetric monoidal categories, they are not sufficient in our case and we will extend the framework to surface-embedded graphs to be able to capture the absence of symmetry in a category and the corresponding topological properties of its string diagrams. We develop the necessary categorical structure of surface-embedded graphs to implement their rewriting as an instance of double-pushout rewriting. Further, we implement the particular case of graphs embedded in the plane in the dependently typed programming language Agda. We develop a suitable, inductive, and finite representation of plane graphs in the setup of Agda’s dependent type theory. We show how splitting a graph into a substructure of interest and its context, which is a crucial operation for a rewriting step, can be implemented, and establish a context comonad structure not just for plane graphs but for a much larger class of tree-like data types.
| Date of Award | 2 Mar 2026 |
|---|
| Original language | English |
|---|
| Awarding Institution | - University Of Strathclyde
|
|---|
| Sponsors | University of Strathclyde |
|---|
| Supervisor | Conor McBride (Supervisor) & Fredrik Nordvall Forsberg (Supervisor) |
|---|