Pith. sign in

REVIEW 1 cited by

Path spaces of pushouts

Not yet reviewed by Pith; the record is open.

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2402.12339 v2 pith:ZGLQELEK submitted 2024-02-19 math.AT math.CT

classification math.ATmath.CT
keywords constructionhomotopyspaceszigzagdescriptionlooppullbackpushout
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
abstract

Given a span of spaces, one can form the homotopy pushout and then take the homotopy pullback of the resulting cospan. We give a concrete description of this pullback as the colimit of a sequence of approximations, using what we call the zigzag construction. We also obtain a description of loop spaces of homotopy pushouts. Using the zigzag construction, we reproduce generalisations of the Blakers-Massey theorem and fundamental results from Bass-Serre theory. We also describe the loop space of a wedge and show that it splits after suspension. Our construction can be interpreted in a large class of $(\infty,1)$-categories and in homotopy type theory, where it resolves the long-standing open problem of showing that a pushout of 0-types is 1-truncated. The zigzag construction is closely related to the James construction, but works in greater generality.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Formalization of the zigzag construction of path spaces of pushouts in homotopy type theory

    math.LO 2025-10 conditional novelty 5.0 of 10 full

    The zigzag construction for path spaces of arbitrary pushouts is fully formalized in Agda, with a machine-checked proof that it is fiberwise equivalent to the actual path spaces.

Pith tools