Investigations into Graph-theoretical Constructions in Homotopy Type Theory

Abstract

Denne avhandlingen presenterer en konstruktiv og bevisrelevant utvikling av grafteorikonsepter innen Homotopi-typeteori (HoTT). HoTT er en utvidelse av Martin-Löfs intuisjonistiske typeteori og inkorporerer nyskapende elementer som Voevodskys univalensprinsipp og høyere induktive typer. Dette strukturalistiske perspektivet er mer i tråd med standard matematisk praksis enn tidligere formelle systemer fordi i HoTT forfremmes isomorfier til likheter — elementer i den korresponderende Martin-Löf identitetstypen. Denne avhandlingen går hovedsakelig inn i de grunnleggende aspektene av grafteori, med mindre vekt på de praktiske sidene. Hovedbidragene er definisjoner, lemmaer og bevis, som oppstår fra en syntese av uformell presentasjon og formalisering ved hjelp av en bevisassistent. Vi arbeider spesifikt i kategorien av rettede multigrafer i HoTT.

Inspirert av topologiske og kombinatoriske aspekter av grafer på overflater, formulerer vi en grunnleggende karakterisering av planare grafer. Dette gjøres uten å definere en overflate eller direkte arbeide med reelle tall, som man finner i annen litteratur. Vår tilnærming er basert på grafkart og flater for lokalt rettede og sammenhengende multigrafer. En graf kvalifiserer som plan hvis den inneholder et grafkart og en ytre flate, slik at enhver sti i den underliggende grafen bare er turhomotopisk til en annen.

Blant våre viktigste funn, fastslår vi at denne typen planarkart utgjør en homotopisk mengde, som er endelig når grafen er endelig. I tillegg introduserer vi utvidelser av planarkart for å induktivt generere eksempler på planære grafer. Vi ser også på konsepter som spenntrær og representasjon av grafer som rom gjennom grafkart.

This thesis presents a constructive and proof-relevant development of graph theory concepts within Homotopy Type Theory (HoTT). HoTT, an extension of Martin-Löf’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-Löf’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 the representation of graphs as spaces through graph maps.

Esta tesis presenta un desarrollo constructivo para el estudio de conceptos de teoría de grafos dentro de la Teoría de Tipos Homotópica (HoTT), la cual es una extensión de la teoría de tipos intuicionista de Martin-Löf que incorpora el principio de Univalencia de Voevodsky y tipos inductivos superiores. Su perspectiva estructuralista se alinea con la práctica matemática estándar al considerar isomorfismos como igualdades — términos del correspondiente tipo de identidad en la teoría de tipos de Martin-Löf. Aquí, profundizamos en los fundamentos de las matemáticas, nociones básicas de la teoría de grafos y en como definir los conceptos correctamente, con menor énfasis en sus aspectos prácticos. Las principales contribuciones de este trabajo son definiciones, lemas y demostraciones, que a menudo surgen de una presentación sintáctica e informal en combinación con la formalización de dichos conceptos dentro de un asistente de demostraciones. Para ser más precisos, los objetos de estudio aquí hacen parte de la categoría de multigrafos dirigidos escritos en HoTT.

Inspirados por la topología y la combinatoria de los grafos en superficies, formulamos una caracterización de grafos planares. Esto se hace sin definir una superficie o emplear números reales. Nuestro enfoque se basa en mapas combinatorios de grafos como estructura sobre el tipo de grafo y caras para multigrafos localmente dirigidos y conexos. Un grafo califica como planar si es posible asociarle un mapa combinatorio y una cara exterior, permitiendo que cualquier recorrido en el grafo embedido sea meramente homotópico a otro recorrido.

Entre nuestros descubrimientos clave, confirmamos que este tipo de mapas combinatorios planares constituye un conjunto homotópico, que es finito cuando el grafo es finito. Además, introducimos extensiones de mapas combinatorios para generar inductivamente ejemplos de grafos planares. También profundizamos en otros conceptos como árboles de expansión y la representación de grafos como espacios via tipos inductivos superiores (HITs en HoTT). Como trabajo futuro se propone una lista de conjeturas que conectan la caracterización de grafos planares en términos de mapas combinatorios con las construcciones de espacios topológicos usando tipos inductivos superiores.