A data type of intrinsically plane graphs in Agda

Tools

Altenmüller, Malin and Mc Bride, Conor Titania; Nordvall Forsberg, Fredrik and McKinna, James, eds. (2026) A data type of intrinsically plane graphs in Agda. In: 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics, LIPIcs . Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Saarbrücken/Wadern. ISBN 9783959774413 (https://doi.org/10.4230/LIPICS.TYPES.2025.13)

[thumbnail of Altenmuller-McBride-TYPES-2025-A-data-type-of-intrinsically-plane-graphs-in-Agda]
Preview
 Text. Filename: Altenmuller-McBride-TYPES-2025-A-data-type-of-intrinsically-plane-graphs-in-Agda.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (2MB)| Preview

Abstract

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.

ORCID iDs

Altenmüller, Malin and Mc Bride, Conor Titania ORCID logoORCID: https://orcid.org/0000-0003-1487-0886; Nordvall Forsberg, Fredrik and McKinna, James
CORE (COnnecting REpositories)