On Planarity of Graphs in Homotopy Type Theory

TL;DR

This paper presents 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, and introduces extensions of planar maps.

Abstract

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.

Figures (13)

• Figure 1: It is shown a graph along with three different planar embeddings, namely $e_1$, $e_2$, and $e_3$. We have shaded with different colours the three faces in each embedding.
• Figure 2: The graph $K_{3,3}$. Each arrow in the picture represents a pair of edges, one in each direction.
• Figure 3: Two graph homomorphisms $\varphi_0$ and $\varphi_1$ from $P_{3}$ to $K_{2}$. The dashed arrows represent how $\varphi_0$ and $\varphi_1$ map the nodes of $P_3$ into $K_2$. We represent the colours of the $2$-coloring of $P_3$ by the nodes black and white in $K_2$.
• Figure 4: We show in (a) the drawing of a graph $G$ with edge crossings. A representation of the graph $G$ embedded in the sphere is shown in (b). The graph embedded $U(G)$ serves as the symmetrisation of the graph $G$. Recall an edge $e$ in $G$ from $x$ to $y$ induces an edge in $U(G)$ from $x$ to $y$ and an edge from $y$ to $x$. For brevity, we only draw a segment representing such a pair of related edges. The corresponding faces of the graph embedding shaded in (b) are named $F_i$ for $i$ from $1$ to $6$. It is shown in (c) with fuchsia colour the incident edges at the node $a$ in $U(G)$. The rotation system at $a$, i.e. the cyclic set denoted by $(ba\,ax\,ad)$, is shown in green colour. The dashed lines represent edges not visible to the view.
• Figure 5: On the right side, we shade the face $F_1$ of the graph $G$ embedded in the sphere given in \ref{['fig:drawing-graph']}. We have the cycle graph $C_3$ and $h:\mathsf{Hom}(C_3,U(G))$ given by $(\alpha, \beta)$ on the left side. $C_3$ and $h$ can be used to define the face $F_1$ using $C_3$ as the graph $A$ in \ref{['def:face']}.

Theorems & Definitions (60)

• definition 1
• definition 2
• definition 3
• definition 4
• lemma 1
• definition 5
• lemma 2
• definition 6
• lemma 3
• lemma 4