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.

翻译：在本文中,我们展示了图表理论的建设性和与证据相关的发展,包括地图概念、其面貌和嵌入球体的图形图示,以同质类型理论的形式。这使我们能够为本地定向定点和连接的多面图提供基本规划性特征,这些多面图谱的灵感来自地貌图理论,特别是将图形嵌入表面的组合嵌入图示。一个图如果有地图和外面,嵌入的图形中的任何行走都是行进式-热位图,则是一个平面图。其结果是,这种平面图形成一个同质图集。作为构建图形图示范例的一种方法,我们引入了平面图图图的扩展。我们在证据辅助者阿格达中将这项工作的基本部分正规化为证据辅助者阿格达(Agda) 支持同质式理论。