Thesis
Combinatorial presentations of string diagrams for non-symmetric monoidal categories
- Creator
- Rights statement
- Awarding institution
- University of Strathclyde
- Date of award
- 2026
- Thesis identifier
- T17662
- Person Identifier (Local)
- 201887086
- Qualification Level
- Qualification Name
- Department, School or Faculty
- Abstract
- 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.
- Advisor / supervisor
- Duncan, Ross
- McBride, Conor
- Resource Type
- DOI
Relations
Items
| Thumbnail | Title | Date Uploaded | Visibility | Actions |
|---|---|---|---|---|
|
|
PDF of thesis T17662 | 2026-04-21 | Public | Download |