Esta tesis presenta un desarrollo novedoso, constructivo y proof-relevant de conceptos de graph theory dentro de Homotopy Type Theory (HoTT). HoTT es una extensión de la type theory intuicionista de Martin-Löf que incorpora el principio de Univalence de Voevodsky y higher inductive types. Su perspectiva estructuralista se alinea con la práctica matemática estándar al promover isomorfismos a igualdades — habitantes del identity type correspondiente de Martin-Löf. Esta tesis profundiza principalmente en las matemáticas fundacionales de los grafos, con menos énfasis en aspectos aplicados. Las contribuciones centrales son definiciones, lemas y pruebas, que surgen de una síntesis entre la presentación informal y la formalización con un proof assistant. Trabajamos específicamente en la categoría de directed multigraphs en HoTT.

Inspirados por las facetas topológicas y combinatorias de grafos en superficies, formulamos una caracterización elemental de los grafos planares. Esto se logra sin definir una superficie ni trabajar directamente con números reales, a diferencia de otros enfoques en la literatura. Nuestra estrategia se basa en graph maps y faces para multigrafos localmente dirigidos y conexos. Un grafo es planar si tiene un graph map y una outer face, de modo que cualquier walk en el grafo embebido sea merely walk-homotopic a otro.

Entre los resultados clave, determinamos que este tipo de planar maps constituye un homotopy set, que es finito cuando el grafo es finito. Además, introducimos extensiones de planar maps para generar inductivamente ejemplos de grafos planares. También exploramos spanning trees y representaciones de dimensión superior de grafos como espacios a través de graph maps.