{"id":"a1f51027-b174-4d85-a9e5-6b4d902326c8","arxiv_id":"2510.08452","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"low","formal_verification":"full","parameter_count":0,"one_line_summary":"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.","lead":"This paper presents the first machine-checked formalization of the zigzag construction, a way of describing paths in any pushout — a shape made by gluing two pieces together along a seam. A generalist might read it as evidence that intricate homotopy-theory arguments can be verified by computer, and as a reusable building block for formalized mathematics.","discovery_kind":"replication","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Deferred-coherence gap: the 'first formalization' claim is unverifiable without the pinned Agda artifact; if the code is missing or contains postulates, Theorem 5.19 is unsupported.","rationale":"The reader's weakest assumption is the same load-bearing concern I identify: the artifact's existence and typechecking. The paper explicitly says some proofs are only in the formalization and gives no URL/hash in the text I reviewed; for a formalization claim this is not a stylistic issue but a missing premise for the central claim. The mathematical exposition does not contain an obvious internal contradiction; the construction follows Wärn and the detailed discussion of computation rules is difficult to explain unless the formalization is real. Still, Lemmas 4.7, 4.8, 5.17 and the prism pasting are exactly the places where a 'complete' formalization could silently be incomplete, so a typecheck against the pinned library is the decisive test. I considered whether a purely mathematical gap exists (e.g. Section 5.2's use of Lemma 4.11 depends on cubes not fully specified), but that too routes through the same artifact concern. Thus no new verdict adjustment is needed; the verdict should remain CONDITIONAL until the artifact is independently verified.","tokens_in":25002,"tokens_out":5695,"duration_ms":67814,"concrete_test":"Pin the exact commit (e.g. ask the author for the URL/commit of the 'fixed version' mentioned in §1); then run `agda` on the modules implementing Constructions 5.5–5.18 and Theorem 5.19 against that pinned agda-unimath version, with a check that these files contain no `postulate`, `admit`, or disabled termination/positivity checks for the zigzag results. If the typecheck succeeds and Theorem 5.19 is a top-level definition whose type matches Definition 3.6, the deferred-coherence gap is closed.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central claim is the existence of a complete machine-checked proof (Theorem 5.19 + Corollary 5.20). The prose repeatedly defers load-bearing coherences to the artifact: Lemma 4.7's coherence is 'not fully reproduced here', Lemma 4.8 and Theorem 5.3 say 'The full proof is available in the formalization', and the §5.2 prism pasting is presented as a diagram plus 'mechanical' adjustment (Appendix B.2/B.3, Lemma 5.17). These are precisely the steps where an axiomatic-HoTT encoding can fail: pasting prisms/cubes and matching top faces involves dependent path algebra that is easy to misstate. No URL or commit hash appears in the reviewed text, so the reader cannot check whether the formalization exists, whether it typechecks against the pinned agda-unimath, or whether it uses postulates/admits. If the artifact is absent or does not close these gaps, the asserted theorem is not established. This concern is about verifiability of the claim, not about the pen-and-paper construction, which appears coherent.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper claims the first formalization of Wärn's zigzag construction of path spaces of pushouts, carried out in Agda using the agda-unimath library. It introduces pushouts via universal properties, descent data, identity systems for descent data (Section 3), sequential colimits and lemmas about sections and induced maps (Section 4), and then constructs the zigzag descent data (P∞_A, P∞_B, -•∞_s) in Section 5. The central result is Theorem 5.19, which states that this descent data, pointed at refl∞, is an identity system; Corollary 5.20 derives the expected fiberwise equivalences with based path spaces. The presentation mixes prose, dependent diagrams, and references to the Agda formalization, with several coherences deferred to the artifact.","tokens_in":25079,"tokens_out":10707,"duration_ms":78486,"significance":"If the formalization is complete and typechecks, this is a significant contribution: it provides the first machine-checked proof of a non-trivial path-space characterization in axiomatic homotopy type theory, with reusable library infrastructure. The paper's strengths include the careful discussion of definitional behavior in the absence of judgmental computation rules for higher inductive types, the section-cocone formulation (Definition 5.11, Construction 5.12), and the explicit technical lemmas in Appendix B. The main unresolved issue is verifiability: the central evidence is the Agda artifact, but the submitted text does not permit an independent check that it exists, typechecks, and contains the deferred coherences.","major_comments":[{"comment":"The central claim is the existence of a complete machine-checked proof (Theorem 5.19 and Corollary 5.20). The manuscript states in §1 that 'A fixed version of the library with the formalization is available on the Internet', but no URL, commit hash, or library version appears in the text, and the ' ' symbol mentioned there is not rendered. This is not a cosmetic issue: load-bearing steps are explicitly deferred. Lemma 4.7 says its coherence is 'not fully reproduced here'; Lemma 4.8 and Theorem 5.3 say 'The full proof is available in the formalization'; and the §5.2 prism pasting plus Lemma 5.17 are presented as diagrams with 'mechanical' adjustments in Appendix B. If the artifact is absent, does not typecheck against the pinned agda-unimath version, or uses postulates/admits in these places, Theorem 5.19 is unsupported. The revision must provide the exact repository location, commit hash","section":"§1, §4, §5.2"},{"comment":"The final coherence t_S is assembled in Construction 5.18 by pasting two prisms and then adjusting the resulting top square by Lemma 5.17. Lemma 5.17 depends on the 'mechanical' adjustments of Construction B.1 and Lemma B.2, and its proof in Appendix B.3 is a proof sketch that normalizes to refl and then invokes the coherence datum of a half-adjoint equivalence. These are exactly the dependent path-algebra steps in which an axiomatic-HoTT formalization can hide gaps. Since Construction 5.18 feeds directly into Theorem 5.19, this is load-bearing. The manuscript must make these coherences checkable: either reproduce them fully or provide precise, citable pointers to the corresponding Agda definitions and confirm that those definitions are part of the verified artifact.","section":"§5.2, Lemma 5.17, Construction 5.18"}],"minor_comments":[{"comment":"The displayed type of the evaluation map has 'sect(QΣA,QΣB,QΣB)' and the codomain is written as QΣA(a0,p0); the first should presumably be 'sect(QΣA,QΣB,QΣS)'.","section":"Definition 3.6"},{"comment":"The two connecting families are both rendered as '-•^n_s' in the plain text, but they appear to have different directions and types (P^n_A(fs)→P^{n+1}_B(gs) versus P^n_B(gs)→P^n_A(fs)). This makes the construction hard to follow. Please use distinct symbols or explicitly disambiguate them in the notation section.","section":"§5.1"},{"comment":"Several access dates appear malformed (e.g., '2025-13-09', '2025-17-07', '2023-30-09'). Please correct them.","section":"References"},{"comment":"The text refers to a ' ' symbol containing links to the formalization, but no such links appear in the reviewed version. Actual URLs should be included, ideally as persistent DOIs or archive identifiers.","section":"§1"}],"recommendation":"major_revision","confidential_remarks":"The paper's central claim is contingent on an Agda artifact that I could not verify from the submitted text. If the artifact is public, pinned to a specific commit, and typechecks without postulates, I would expect the paper to be suitable for publication after the authors add precise pointers, clarify the notation for the two connecting maps, and map each deferred coherence to a named formalized definition. My report is based solely on the manuscript text as provided."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: this is a serious formalization paper. The main theorem is Wärn's — the zigzag family does characterize pushout path spaces — and the author says so. What is new here is the complete Agda proof in agda-unimath, including the encodings needed to make the informal construction go through: dropping the −•ⁿₛ component from the induction motive, defining section cocones to avoid non-uniform computation, carrying refl witnesses. That encoding work is the real contribution, and the paper explains it in unusual detail. If the code typechecks, the result is established; machine-checked proofs in axiomatic HoTT are exactly the kind of evidence we should rely on.\n\nWhere I'd want care: the formalization is the load-bearing part, and several coherences are explicitly deferred to code. Lemma 4.7's coherence is 'not fully reproduced here'; Lemma 4.8 and Theorem 5.3 defer to the formalization; the prism pasting in §5.2 is diagram plus 'mechanical' adjustment. None of that is suspicious by itself — pasting prisms in axiomatic HoTT is exactly the sort of path algebra you don't reproduce in a paper. But it means the paper's central claim cannot be independently verified from the arXiv text alone. The text says a fixed version is on the Internet and that links appear under a symbol, but no URL or commit hash is visible in the extracted version. That is an addressable problem: pin the repository, the agda-unimath commit, and the Agda version, and ideally say whether the file uses postulates anywhere. I don't see it as a math flaw; it's a packaging/verifiability flaw. It would be fixed by a one-line artifact note, and a referee should be able to typecheck.\n\nThe framework assumptions (pushouts and sequential colimits via universal properties, descent, flattening, [10, Lemma 3.6]) are library results, cited and trusted. That's fine; they're established. No circularity: the target is shown to be an identity system using descent and the fundamental theorem, checked against external criteria. Self-citation [14] is an earlier incomplete attempt and is honestly labeled, not an inflation.\n\nWho should read this: anyone working in formalized HoTT or using agda-unimath; also people proving connectivity/truncation results about pushouts, since this gives the machine-checked path-space family they'd want. It's a solid specialized contribution, not a conceptual breakthrough.\n\nRecommendation: send to peer review. The verdict should be conditional on access to the pinned artifact, not on the math.","headline":"First machine-checked formalization of Wärn's zigzag path spaces of pushouts — the math is Wärn's, the formalization work is real and substantial; referee it, but require a pinned artifact.","tokens_in":25760,"tokens_out":2273,"would_cite":true,"duration_ms":43097,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A machine-checked proof shows that the zigzag construction describes the path spaces of every pushout.","keywords":["homotopy type theory","path spaces","pushouts","identity systems","descent data","sequential colimits","zigzag construction","formalized mathematics"],"falsifier":"Open the development linked from the paper and run the checker on the file containing Theorem 5.19; any admitted goal, unsolved meta-variable, or failed definition there would immediately falsify the claimed formalization. A second, more abstract falsifier: construct a model of homotopy type theory in which the zigzag descent data (P∞_A, P∞_B, −•∞_s) pointed at refl∞ is not an identity system; then Theorem 5.19 and Corollary 5.20 would fail together.","tokens_in":24720,"feed_emoji":"🧩","tokens_out":5111,"duration_ms":50257,"temperature":0.7,"pith_summary":"The paper formalizes a known pen-and-paper construction, called the zigzag construction, that gives explicit type families describing the path spaces of any pushout. The central claim is that the zigzag descent data—two sequential-colimit families over the left and right pushout components, joined by an equivalence over the glue—forms an identity system at the basepoint refl∞. By a general theorem about descent data, this single identity-system statement is exactly what is needed to conclude fiberwise equivalences between the usual identity types and the zigzag families for every point in the pushout. This matters because pushouts build spheres, suspensions, wedge sums, and smash products, and explicit path-space descriptions are the first step toward proving truncation and connectivity results about such spaces. Every construction and coherence is claimed to exist as a verified term in a proof-assistant development.","feed_headline":"Formal proof verifies zigzag description of pushout path spaces","feed_subtitle":"Using descent data and identity systems, one theorem turns the zigzag approximations into the exact path-space equivalences.","key_machinery":"The central machinery is the notion of descent data for pushouts, repackaged as an identity system: a pointed pair of type families over the two legs plus a family of equivalences over the glue satisfies an induction principle for sections. The zigzag construction builds this descent data as sequential colimits of stages, where each stage is itself a pushout, and a zigzag of sequential diagrams supplies the equivalence between the two colimit families. The load-bearing formal device is Theorem 3.8, which says that for descent data, being an identity system is equivalent to being fiberwise equivalent to the based path-space family.","core_discovery":"On the paper's own terms, the discovery is that the zigzag construction can be encoded in axiomatic homotopy type theory without judgmental computation rules for higher inductive types, and that its correctness proof can be completed. Theorem 5.19 states exactly that the pointed descent data (P∞_A, P∞_B, −•∞_s, refl∞) is an identity system. Theorem 3.8 then turns that statement into equivalences (inl(a₀)=inl(a)) ≃ P∞_A(a) and (inl(a₀)=inr(b)) ≃ P∞_B(b), compatible with the glue path. The paper also reports the key adjustment that made the induction work: removing the backwards connecting map from the inductively defined data and defining it instead as the right point constructor at each stag","pith_inferences":["A concrete next step the paper leaves implicit is to use these path-space families to formalize the truncation theorem for pushouts along 0-truncated maps, since the explicit families are designed to make connectivity and truncation arguments tractable.","The same descent-data-as-identity-system pattern could be adapted to other colimit shapes, such as general colimits, coequalizers, or higher pushouts, where an explicit zigzag approximation would again characterize path spaces.","The paper's three-case induction trick for t_{n+1}—carrying a computation witness rather than forcing uniform definition—may become a reusable technique for formalizing recursive constructions over inductively indexed higher types.","If the machine-checked development is complete, an independent cubical formalization, which the paper suggests would transcribe diagrams more directly, could serve as a cross-check of the same theorem."],"forward_implications":["If the formalization is correct, the path spaces (inl(a₀) = inl(a)) and (inl(a₀) = inr(b)) of any pushout have explicit, computable descriptions as sequential colimits of stages built from previous stages by pushouts.","The single identity-system theorem automatically yields both families of equivalences in Corollary 5.20, including compatibility with the glue path.","The proof is carried out in axiomatic homotopy type theory, so it does not rely on judgmental computation rules for higher inductive types; this makes it portable both to settings with such rules and to settings without them.","All deferred coherences—the path algebra of Lemma 4.7, the cube fillers of Section 5.2, and the adjustment lemmas in Appendix B—are claimed to exist as verified terms rather than as diagram sketches."],"fun_headline_variants":["First Agda formalization of zigzag path spaces in HoTT","Zigzag path spaces of pushouts: now formally proven in Agda","Formal proof: zigzag construction yields pushout path spaces","Identity system proof for pushout path spaces in Agda","Pushout path spaces via zigzag: Agda formalization"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The central claim collapses if the linked machine-checked development is not actually available, does not typecheck against the pinned version of the proof assistant and its libraries, or contains unfinished goals, because several key coherences are only sketched in prose and deferred to the formalization.","fun_headline_variants_meta":{"raw":{"variants":["First Agda formalization of zigzag path spaces in HoTT","Zigzag path spaces of pushouts: now formally proven in Agda","Formal proof: zigzag construction yields pushout path spaces","Identity system proof for pushout path spaces in Agda","Pushout path spaces via zigzag: Agda formalization"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000193,"raw_usage":{"total_tokens":1131,"prompt_tokens":634,"completion_tokens":497,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":378,"completion_tokens_details":{"reasoning_tokens":422}},"tokens_in":378,"tokens_out":497,"duration_ms":5111,"temperature":1.0,"reasoning_tokens":422,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T10:45:25.487969+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Open the development linked from the paper and run the checker on the file containing Theorem 5.19; any admitted goal, unsolved meta-variable, or failed definition there would immediately falsify the claimed formalization. A second, more abstract falsifier: construct a model of homotopy type theory in which the zigzag descent data (P∞_A, P∞_B, −•∞_s) pointed at refl∞ is not an identity system; then Theorem 5.19 and Corollary 5.20 would fail together.","supporting_citations":[],"review_version":1}