DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2025.13

A Data Type of Intrinsically Plane Graphs in Agda

Authors: Malin Altenmüller and Conor Titania Mc Bride

Published in: LIPIcs, Volume 384, 31st International Conference on Types for Proofs and Programs (TYPES 2025)

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.

Cite as

Malin Altenmüller and Conor Titania Mc Bride. 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), Volume 384, pp. 13:1-13:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{altenmuller_et_al:LIPIcs.TYPES.2025.13,
  author =	{Altenm\"{u}ller, Malin and Mc Bride, Conor Titania},
  title =	{{A Data Type of Intrinsically Plane Graphs in Agda}},
  booktitle =	{31st International Conference on Types for Proofs and Programs (TYPES 2025)},
  pages =	{13:1--13:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-441-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{384},
  editor =	{Nordvall Forsberg, Fredrik and McKinna, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.13},
  URN =		{urn:nbn:de:0030-drops-270312},
  doi =		{10.4230/LIPIcs.TYPES.2025.13},
  annote =	{Keywords: planar graph, spanning tree, dependent types, graph rewriting}
}

Search Results

Documents authored by Mc Bride, Conor Titania

A Data Type of Intrinsically Plane Graphs in Agda

Abstract

Cite as

Thanks for your feedback!

Could not send message