Formalizing the zigzag construction of path spaces of pushouts
Logic
2025-10-10 v1 Algebraic Topology
Abstract
A recent pre-print of W\"arn gives a novel pen-and-paper construction of a type family characterizing the path spaces of an arbitrary pushout, and a natural language argument for its correctness. We present the first formalization of the construction and a proof that it is fiberwise equivalent to the path spaces. The formalization is carried out in axiomatic homotopy type theory, using the Agda proof assistant and the agda-unimath library.
Cite
@article{arxiv.2510.08452,
title = {Formalizing the zigzag construction of path spaces of pushouts},
author = {Vojtěch Štěpančík},
journal= {arXiv preprint arXiv:2510.08452},
year = {2025}
}
Comments
15 pages, 4 figures, submitted to CPP 2026