On Planarity of Graphs in Homotopy Type Theory
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2021
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866916487247167488 |
|---|---|
| author | Prieto-Cubides, Jonathan Gylterud, Håkon Robbestad |
| author_facet | Prieto-Cubides, Jonathan Gylterud, Håkon Robbestad |
| contents | In this paper, we present a constructive and proof-relevant development of graph theory, including the notion of maps, their faces, and maps of graphs embedded in the sphere, in homotopy type theory. This allows us to provide an elementary characterisation of planarity for locally directed finite and connected multigraphs that takes inspiration from topological graph theory, particularly from combinatorial embeddings of graphs into surfaces. A graph is planar if it has a map and an outer face with which any walk in the embedded graph is walk-homotopic to another. A result is that this type of planar maps forms a homotopy set for a graph. As a way to construct examples of planar graphs inductively, extensions of planar maps are introduced. We formalise the essential parts of this work in the proof-assistant Agda with support for homotopy type theory. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2112_06633 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | On Planarity of Graphs in Homotopy Type Theory Prieto-Cubides, Jonathan Gylterud, Håkon Robbestad Logic in Computer Science Combinatorics In this paper, we present a constructive and proof-relevant development of graph theory, including the notion of maps, their faces, and maps of graphs embedded in the sphere, in homotopy type theory. This allows us to provide an elementary characterisation of planarity for locally directed finite and connected multigraphs that takes inspiration from topological graph theory, particularly from combinatorial embeddings of graphs into surfaces. A graph is planar if it has a map and an outer face with which any walk in the embedded graph is walk-homotopic to another. A result is that this type of planar maps forms a homotopy set for a graph. As a way to construct examples of planar graphs inductively, extensions of planar maps are introduced. We formalise the essential parts of this work in the proof-assistant Agda with support for homotopy type theory. |
| title | On Planarity of Graphs in Homotopy Type Theory |
| topic | Logic in Computer Science Combinatorics |
| url | https://arxiv.org/abs/2112.06633 |