On Homotopy of Walks and Spherical Maps in Homotopy Type Theory
Jonathan Prieto-Cubides

TL;DR
This paper refines the understanding of spherical maps in homotopy type theory by introducing a combinatorial homotopy notion for walks, formalized in Agda, to characterize graph embeddings in the sphere.
Contribution
It presents a new combinatorial homotopy framework for walks in graphs, refining spherical map characterization within homotopy type theory, and formalizes results using Agda.
Findings
Walks in spherical maps are homotopic to normal forms.
A graph can be embedded in the sphere if walks with same endpoints are homotopic.
Formalization achieved in Agda.
Abstract
We work with combinatorial maps to represent graph embeddings into surfaces up to isotopy. The surface in which the graph is embedded is left implicit in this approach. The constructions herein are proof-relevant and stated with a subset of the language of homotopy type theory. This article presents a refinement of one characterisation of embeddings in the sphere, called spherical maps, of connected and directed multigraphs with discrete node sets. A combinatorial notion of homotopy for walks and the normal form of walks under a reduction relation is introduced. The first characterisation of spherical maps states that a graph can be embedded in the sphere if any pair of walks with the same endpoints are merely walk-homotopic. The refinement of this definition filters out any walk with inner cycles. As we prove in one of the lemmas, if a spherical map is given for a graph with a…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
