2026-07-30T14:29:16Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27031 2026-07-30T09:16:25Z ddc:004 open_access

A Data Type of Intrinsically Plane Graphs in Agda Altenmüller, Malin Mc Bride, Conor Titania planar graph spanning tree dependent types graph rewriting 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Malin Altenmüller and Conor Titania Mc Bride 2026 Is Part Of LIPIcs, Volume 384, 31st International Conference on Types for Proofs and Programs (TYPES 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2025.13 urn:nbn:de:0030-drops-270312 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.13 eng https://creativecommons.org/licenses/by/4.0/legalcode