On homotopy of walks and spherical maps in homotopy type theory
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 discrete node set, then any walk in the graph is merely walk-homotopic to a normal form.
The proof assistant Agda contributed to formalising the results recorded in this article.
Tue 18 JanDisplayed time zone: Eastern Time (US & Canada) change
16:30 - 18:10
|Implementing a category-theoretic framework for typed abstract syntaxRemote|
Benedikt Ahrens TU Delft, The Netherlands, Ralph Matthes IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse, Anders Mörtberg Department of Mathematics, Stockholm UniversityDOI Pre-print Media Attached
|(Deep) Induction Rules for GADTsRemote|
CPPPre-print Media Attached
|On homotopy of walks and spherical maps in homotopy type theoryRemote|
Jonathan Prieto-Cubides University of BergenPre-print Media Attached
|Windmills of the minds: an algorithm for Fermat's Two Squares TheoremRemote|
Hing Lun Chan Australian National UniversityDOI Pre-print Media Attached File Attached