On homotopy of walks and spherical maps in homotopy type theory
summary
Defines a decidable loop-reduction on directed multigraph walks and proves a normalization theorem: every walk reduces to a normal form that is walk-homotopic to the original. Introduces quasi-simple walks (no inner cycles) and shows for graphs with discrete node sets that two walk-homotopy definitions of spherical maps are equivalent. Formalization in Agda verifies the lemmas and yields a brute-force algorithm for finite graphs to decide sphericity.
AI-written summary · about