This thesis presents a novel constructive and proof-relevant development of graph theory concepts within Homotopy Type Theory (HoTT). HoTT, an extension of Martin-Lof’s intuitionistic type theory, incorporates novel features like Voevodsky’s Univalence principle and higher inductive types. Its structuralist perspective aligns with standard mathematical practise by promoting isomorphisms to equalities — inhabitants of the corresponding Martin-Lof’s identity type. This thesis primarily delves into the foundational mathematics of graphs, with less emphasis on their practical aspects. The core contributions are definitions, lemmas, and proofs, which often arise from a synthesis of informal presentation and formalisation within a proof assistant. We specifically work within the category of directed multigraphs in HoTT.

Inspired by the topological and combinatorial facets of graphs on surfaces, we formulate an elementary characterisation of planar graphs. This is done without defining a surface or directly working with real numbers, as found in some literature. Our approach hinges on graph maps and faces for locally directed and connected multigraphs. A graph qualifies as planar if it features a graph map and an outer face, allowing any walk in the embedded graph to be merely walk-homotopic to another.

Among our key discoveries, we ascertain that this kind of planar maps constitutes a homotopy set, which is finite when the graph is finite. Additionally, we introduce extensions of planar maps to inductively generate examples of planar graphs. We also delve into further concepts such as spanning trees and higher dimensional representations of graphs as spaces through graph maps.