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
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.
Forward citations
Cited by 1 Pith paper
-
Formalization of the zigzag construction of path spaces of pushouts in homotopy type theory
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.
Discussion (0). Continue with ORCID to comment.