Formalizing the zigzag construction of path spaces of pushouts

TL;DR

The paper addresses the formalization of a pen-and-paper zigzag construction for the path spaces of pushouts within axiomatic HoTT, implemented in Agda with the agda-unimath library. It develops a descent-data framework for pushouts, leverages sequential colimits, and constructs an identity-system-based proof that the zigzag realization fiberwise captures path spaces. The main contributions are the first formalization of Wärn's construction, a rigorous proof that the zigzag data forms an identity system, and a detailed treatment of dependent diagrams and coherence in a proof-assistant setting. This work strengthens the foundations of synthetic homotopy theory by enabling precise formal reasoning about pushouts and their path spaces, and it points toward future work in cubical type theory to streamline diagrammatic reasoning.

Abstract

A recent pre-print of Wärn 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.

Figures (4)

• Figure 1: Construction of maps $t_B^{n+1}$ and $t_A^{n+1}$
• Figure 2: Construction of the coherences $T_B^{n+2}$ and $T_A^{n+1}$. Slashed arrows indicate where an additional implicit transport is applied.
• Figure 3: Strategy for defining the coherence $t_S$.
• Figure 4: Dependencies between definitions in the zigzag construction.

Theorems & Definitions (32)

• Definition 1
• Lemma 1
• Lemma 2: descent theorem
• Definition 2
• Lemma 3: flattening
• Definition 3
• Theorem 3.1
• proof
• Definition 4
• Lemma 4