同伦类型论中图的平面性

在本文中，我们在同伦类型论中给出图论的构造性与证明相关的发展，包括映射、其面以及嵌入球面的图的映射的概念。这使我们能够受拓扑图论（特别是图的组合嵌入曲面）启发，为局部有向有限连通多重图提供一种平面性的初等刻画：一个图是平面的，当且仅当它有一个映射和一个外表面，使得嵌入图中的任意游走都与另一条游走在游走同伦意义下等价。一个结果是此类平面映射对某个图构成一个同伦集合。作为归纳构造平面图实例的方法，我们引入了平面映射的扩展。我们在支持同伦类型论的证明辅助工具 Agda 中形式化了本工作的核心部分。