Investigations on graph-theoretical constructions in Homotopy type theory

Welcome, this website contains a few formalisations of graph-theoretical constructions in homotopy type theory. The formalisations are done in the proof-assistant Agda v2.6.2 with the flag --without-K, --exact-split and for some files --rewriting. A more detailed of the constructions are contained in my PhD thesis, which is in the process of revision.If you are interested in the formalisation , or any part of my work and do not know how to cite, or have any further question, please let me know to my email jonathan.cubides@uib.no.

Keywords: Homotopy type theory, planarity, combinatorial maps, Agda, formal verification

Related documents

• Prieto-Cubides, Jonathan, and Gylterud, Håkon. R. Planar graphs in univalent mathematics. Abstract. TYPES 2019. Oslo, Norway, 11 June. 2019. (PDF)

• Prieto-Cubides, Jonathan. On Homotopy of Walks and Spherical Maps in Homotopy Type Theory. (PDF) (Code)

Abstract. We work with combinatorial maps to represent graph embeddings into surfaces up to isotopy. The surface in which the graph is embedded is left implicit in this approach. The constructions herein are proof-relevant and stated with a subset of the language of homotopy type theory. This article presents a refinement of one characterisation of embeddings in the sphere, called spherical maps, of connected and directed multigraphs with discrete node sets. A combinatorial notion of homotopy for walks and the normal form of walks under a reduction relation is introduced. The first characterisation of spherical maps states that a graph can be embedded in the sphere if any pair of walks with the same endpoints are merely walk-homotopic. The refinement of this definition filters out any walk with inner cycles. As we prove in one of the lemmas, if a spherical map is given for a graph with a discrete node set, then any walk in the graph is merely walk-homotopic to a normal form.

• Prieto-Cubides, Jonathan, and Gylterud, Håkon. R. On Planarity of Graphs in Homotopy Type Theory. 2022. (PDF). (Code) (Submitted to MSCS 2022)

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.

• Prieto-Cubides, Jonathan. On Trees and Their Topological Realisations in Homotopy Type Theory. (PDF) (Code) (Draft)

Abstract. In this work, we characterise in homotopy type theory the type of rooted trees and oriented spanning trees, which are the generalisation of the notions of a tree and spanning tree for directed multigraphs. We state and prove the theorem about the mere existence of oriented spanning trees for connected graphs with a finite node set and a set of edges between any two nodes.
In addition, we look at the topological realisation for graphs, which in HoTT can be seen as a coequalizer, the higher-inductive type that considers a topological space where the nodes are points and edges are paths glued to their endpoints. In this view, a graph is connected if its geometric realisation is a connected type. A tree is a graph with no non-trivial loops, for which its topological realisation is connected and contractible. Finally, a proof is given to show that the realisation of rooted trees is a connected and contractible type, as expected. We believe the results here can help to study the fundamental group of a graph, which requires computing a spanning tree. A formalisation accompanies most results in Agda using the Cubical mode and the Cubical Agda library.

{-# OPTIONS --without-K #-}

Check Agda code/proofs here

Extra

• The source code is available here. Email me if you want the latest version.
• A list of all Agda modules is available here.
• A list of the postulates used in this formalisation is available here.
• A graph of the Agda dependencies is available here.
• This website is generated using pandoc and the Latex backend of Agda. Bash script.
• There is a Python script to list all the postulates in the whole ongoing formalisation.
• The graph image with all Agda module dependencies is generated using Agda and the png tool by GraphViz.

Latest changes

(2022-12-28)(57c278b4) Last updated: 2021-09-16 15:00:00 by jonathan.cubides
(2022-07-06)(d3a4a8cf) minors by jonathan.cubides
(2022-01-26)(4aef326b) [ reports ] added some revisions by jonathan.cubides
(2021-12-20)(049db6a8) Added code of cubical experiments. by jonathan.cubides
(2021-12-20)(961730c9) [ html ] regular update by jonathan.cubides
(2021-12-20)(e0ef9faa) Fixed compilation and format, remove hidden parts by jonathan.cubides
(2021-12-20)(5120e5d1) Added cubical experiment to the master by jonathan.cubides
(2021-12-17)(828fdd0a) More revisions added for CPP by jonathan.cubides
(2021-12-15)(0d6a99d8) Fixed some broken links and descriptions by jonathan.cubides
(2021-12-15)(662a1f2d) [ .gitignore ] add by jonathan.cubides
(2021-12-15)(0630ce66) Minor fixes by jonathan.cubides
(2021-12-13)(04f10eba) Fixed a lot of details by jonathan.cubides
(2021-12-10)(24195c9f) [ .gitignore ] ignore .zip and arxiv related files by jonathan.cubides
(2021-12-09)(538d2859) minor fixes before dinner by jonathan.cubides
(2021-12-09)(36a1a69f) [ planar.pdf ] w.i.p revisions to share on arxiv first by jonathan.cubides