A Data Type of Intrinsically Plane Graphs in Agda

Reference. A Data Type of Intrinsically Plane Graphs in Agda

Malin Altenmüller, Conor McBride · TYPES · 2026 · string-diagrams · DOI

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.

Cite

Cite as @altenmuller-2026-a (helia, typst) · \cite{altenmuller-2026-a} (LaTeX)

BibTeX

bibtex · 14 lines

@inproceedings{altenmuller-2026-a,
  doi = {10.4230/LIPICS.TYPES.2025.13},
  url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.13},
  author = {Altenmüller, Malin and Mc Bride, Conor Titania},
  keywords = {planar graph, spanning tree, dependent types, graph rewriting, Theory of computation → Type theory, Mathematics of computing → Graphs and surfaces, Theory of computation → Rewrite systems},
  language = {en},
  title = {A Data Type of Intrinsically Plane Graphs in Agda},
  volume = {384},
  pages = {13:1-13:24},
  publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
  year = {2026},
  copyright = {Creative Commons Attribution 4.0 International license},
  booktitle = {31st International Conference on Types for Proofs and Programs (TYPES 2025)}
}

hayagriva YAML (typst)

yaml · 16 lines

altenmuller-2026-a:
  type: article
  title: A Data Type of Intrinsically Plane Graphs in Agda
  author:
  - Altenmüller, Malin
  - Mc Bride, Conor Titania
  date: 2026
  page-range: 13:1-13:24
  url: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.13
  serial-number:
    doi: 10.4230/LIPICS.TYPES.2025.13
  parent:
    type: proceedings
    title: 31st International Conference on Types for Proofs and Programs (TYPES 2025)
    publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
    volume: 384

Download: altenmuller-2026-a.bib · altenmuller-2026-a.yml

Cites 27 works (0 here)

External (27)

Combinatorial Presentations of String Diagrams for Non-Symmetric Monoidal Categories (2025)
A category of surface-embedded graphs (2022)
Algebraic graphs with class (functional pearl) (2017)
Rewriting modulo symmetric monoidal structure (2016)
Regular behaviours with names - on rational fixpoints of endofunctors on nominal sets (2016)
A generic method for bijections between blossoming trees and planar maps (2015)
Equational reasoning with context-free families of string diagrams (2015)
A correspondence between rooted planar maps and normal planar lambda terms (2015)
Open-graphs and monoidal theories (2013)
On building cyclic and shared structures in haskell (2012)
Interacting quantum observables: categorical algebra and diagrammatics (2011)
A survey of graphical languages for monoidal categories (2011)
Type inference in context (2010)
Initial algebra semantics for cyclic sharing structures (2009)
Formal proof–the four-color theorem (2008)
The four colour theorem: Engineering of a formal proof (2008)
Bijective counting of tree-rooted maps and shuffles of parenthesis systems (2007)
Types for quantum computing (2006)
Representing cyclic structures as nested datatypes (2006)
Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions (2004)
Inductive graphs and functional graph algorithms (2001)
Topological Graph Theory (2001)
Graphs on Surfaces (2001)
The zipper (1997)
Lazy depth-first search and linear graph algorithms in haskell (1993)
A combinatorial representation for oriented polyhedral surfaces (1960)
Über das problem der nachbargebiete (1891)