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

Vojt\v{e}ch \v{S}t\v{e}pan\v{c}\'ik

REVIEW 2 major objections 4 minor 14 references

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

T0 review · 2 major / 4 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A machine-checked proof shows that the zigzag construction describes the path spaces of every pushout.

desk verdict 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. read the letter →

arxiv 2510.08452 v2 pith:5VGS22IB submitted 2025-10-09 math.LO math.AT

Vojtěch Štěpančík This is my paper · ORCID

classification math.LOmath.AT

keywords homotopytypetheorypathspacespushoutsidentitysystemsdescentdatasequentialcolimitszigzagconstructionformalizedmathematics

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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

Load-bearing premise

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.

Editorial extensions

If this is right

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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

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.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the 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.

Where 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.

The 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.

Who 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.

Recommendation: send to peer review. The verdict should be conditional on access to the pinned artifact, not on the math.

Referee Report

2 major / 4 minor

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.

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 (2)

[§1, §4, §5.2] 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
[§5.2, Lemma 5.17, Construction 5.18] 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.

minor comments (4)

[Definition 3.6] 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)'.
[§5.1] 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.
[References] Several access dates appear malformed (e.g., '2025-13-09', '2025-17-07', '2023-30-09'). Please correct them.
[§1] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found: the zigzag construction is checked against an external identity-system criterion; deferred Agda coherences are a verifiability gap, not a circular reduction.

full rationale

No load-bearing circular step could be exhibited. The central claim, Theorem 5.19, is that the explicitly constructed zigzag descent data (P∞_A, P∞_B, −•∞_s) pointed with refl∞ is an identity system in the sense of Definition 3.6. This property is not assumed or baked into the definition of the data: it is proved by constructing sections (t_A, t_B, t_S) for arbitrary descent data QΣ over the total span, using the dependent universal properties of pushouts and sequential colimits. The final equivalences to path spaces are then obtained by the external fundamental theorem of identity types via Theorem 3.8, not by definition. The type families P∞_A and P∞_B are built recursively from (a0 = −) and the empty type, not from the target path-space equivalences, so the conclusion is genuinely derived rather than presupposed. Cited prior results (descent, flattening, sequential colimits from [7], [8], [10], [11]) are standard and are not self-citations of the author; the one self-related item, [14], is explicitly described as an incomplete prior attempt and is not used as support. The manuscript does contain real verification gaps: Lemma 4.7 states its coherence 'is not fully reproduced here', Lemma 4.8 and Theorem 5.3 defer to the formalization, and the prism pasting for Construction 5.18 is summarized as 'mechanical' path algebra (Appendix B). These are omissions of proof details, not circular reasoning: the deferred coherences are promised outputs of the Agda artifact, not assumed inputs. If the artifact is missing or does not typecheck, the paper's machine-checked claim is unsupported, but that is a correctness/verifiability concern, not a circularity. Therefore the circularity score is 0.

Assumptions & free parameters 0 free parameters · 7 assumptions · 0 invented entities

No free parameters exist: this is pure formal mathematics — the construction depends only on the span (A ← S → B), the basepoint a₀, and the axioms below; nothing is fitted, tuned, or chosen to make the proof work. The axioms are the standard ones of axiomatic HoTT (univalence, function extensionality, path induction) plus the existence postulates for pushouts and sequential colimits, which the paper explicitly adopts because it works without computational higher inductive types (§2–§4). The descent theorem, flattening lemma and [10, Lemma 3.6] are imported as established library results. No new ontological entities are invented: 'zigzag construction data', 'section cocones', and the approximation diagrams P•_A, P•_B are definitions inside the framework with no independent-existence commitment beyond what the axioms provide. The one assumption not captured as a mathematical axiom is the paper's self-description that the Agda artifact exists, is complete, and matches the prose; that is a verification condition, not an axiom of the mathematics.

assumptions (7)

standard math Univalence axiom
Used throughout: descent theorem (Lemma 3.3), structure identity principle, and the descent/flattening step in Theorem 3.8 all rely on univalence. Assumed as an axiom of the framework ([8, 11]), not proved in the paper.
standard math Function extensionality
Used implicitly in every homotopy-level statement (e.g. homotopies of sections in §4, Lemma 4.10). Follows from univalence in HoTT; background.
domain assumption Existence of pushouts satisfying the (dependent) universal property
§3: 'We don't have higher inductive types, so instead we define pushouts to be structures satisfying a certain universal property.' Pushouts are built at every stage of the construction (Construction 5.5, 5.7, 5.8); this is a postulate of the formalization, and the whole paper is vacuous without it.
domain assumption Existence of sequential colimits satisfying the (dependent) universal property; shifted colimits
§4 (Definition 4.1 and following) takes sequential colimits as postulated structures with a universal property; Theorem 5.3 further relies on [10, Lemma 3.6] that dropping the first cocone component yields a colimit of the shifted diagram. 'The proof is not included here' (§4).
standard math Descent theorem and flattening lemma (Rijke)
Lemmas 3.3 and 3.5, imported from Rijke [7, Chapter 2]. These convert type families over pushouts to descent data, which is the representational skeleton of the entire zigzag construction and of the identity-system criterion (Definition 3.6).
standard math Fundamental theorem of identity types
Invoked in the proof of Theorem 3.8 ('By the fundamental theorem of identity types...') to conclude that a family equivalent to an identity system is an identity system; cited [8, Theorem 11.2.2].
standard math Path induction and transport computation in identity types
Universal: the zero-stage families are P⁰_A(a) := (a₀ = a) (Construction 5.5), eliminated by path induction; transport computations such as [11, Lemma 2.11.2] are used in Construction 3.7.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Formalization of the zigzag construction of path spaces of pushouts in homotopy type theory." pith.science (2026). https://pith.science/paper/5VGS22IB

@misc{pith2026251008452,
  author       = {Pith},
  title        = {Pith review of: Formalization of the zigzag construction of path spaces of pushouts in homotopy type theory},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/5VGS22IB}},
  note         = {Machine review of arXiv:2510.08452}
}

read the original abstract

A pre-print of W\"arn gives a pen-and-paper construction of a type family characterizing the path spaces of an arbitrary pushout, and a natural language argument for its correctness. This paper presents 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

Figures reproduced from arXiv: 2510.08452 by the authors.

**Figure 1.** Construction of maps 𝑡 𝑛+1 𝐵 and 𝑡 𝑛+1 𝐴 To define 𝑡 𝑛+1 𝐵 , the behavior on point constructors consists of maps 𝑡 𝑛+1 𝐵 (incl𝑛 𝐵 (−)) : (𝑝 : 𝑃 𝑛 𝐵 (𝑏)) → 𝑄 𝑛+1 Σ𝐵 (incl𝑛 𝐵 𝑝) 𝑡 𝑛+1 𝐵 (− •𝑛 𝑠) : (𝑝 : 𝑃 𝑛 𝐴 (𝑓 𝑠)) → 𝑄 𝑛+1 Σ𝐵 (𝑝 •𝑛 𝑠). We need to distinguish between 𝑡 𝑛+1 𝐵 and 𝑡 𝑛+1 𝐵 , because they have different computational properties. Since we work in a type theory without judgmental computation rules for pushou… view at source ↗

**Figure 3.** Strategy for defining the coherence 𝑡𝑆 . The prisms of sections, depicted below, involve simple functions at the base, sections of type families pointing upwards, fiberwise functions at the top lying over the functions below them, vertical commuting squares, a commuting triangle at the base, and a dependent triangle at the top, lying over the bottom triangle. 𝑄 𝑛 Σ𝐴 𝑄 𝑛+1 Σ𝐴 𝑄 𝑛+1 Σ𝐵 𝑃 𝑛 𝐴 (𝑓 𝑠) 𝑃 𝑛+1 𝐴 (𝑓 𝑠) 𝑃 𝑛+… view at source ↗

**Figure 4.** Dependencies between definitions in the zigzag construction. 𝑑 𝑄 𝑛+1 Σ𝐴 (𝑥) 𝑄 𝑛+1 Σ𝐴 (𝑦) 𝑏 • • 𝑄 𝑛+2 Σ𝐵 (𝑧) 𝑄 𝑛+2 Σ𝐵 (𝑥 •𝑛+1 𝑠) 𝑄 𝑛+2 Σ𝐵 (𝑧) 𝑄 𝑛+2 Σ𝐵 (𝑦 •𝑛+1 𝑠), Ψ𝑛+1 𝑟# 𝑆 id (𝑡•ap−•𝑛+1 𝑠 (𝑟 −1 ) )−1 # 𝑡# Ψ −1 𝑛+1 where the right square is Construction B.1, inverting it to get a dependent path from 𝑑 to Ψ −1 𝑛+1 (𝑡#𝑑) over 𝑟, then inverting it as a dependent path to get a dependent path from Ψ −1 𝑛+1 (𝑡#𝑑) to 𝑑 over… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

14 extracted references · 3 linked inside Pith

[14]

commuting squares of sections

Vojtěch Štěpančík. 2024. Formalization of Homotopy Pushouts in Homotopy Type Theory. A Commuting shapes and coherences We use two kinds of diagrams: non-dependent ones, which express commutativity of non-dependent functions between types, and commutativity of such homotopies; and depen- dent ones, which can express diagrams involving type fami- lies, fibe...

2024
[1]

2025.Agda.https://agda.readthedocs.io/

Agda Developers. 2025.Agda.https://agda.readthedocs.io/

2025
[2]

Steve Awodey and Michael A. Warren. 2009. Homotopy theoretic mod- els of identity types.Mathematical Proceedings of the Cambridge Philo- sophical Society146, 1 (2009), 45–55. doi:10.1017/S0305004108001783

doi:10.1017/s0305004108001783 2009
[3]

Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shul- man, Matthieu Sozeau, and Bas Spitters. 2017. The HoTT library: a formalization of homotopy type theory in Coq. InProceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs(Paris, France)(CPP 2017). Association for Computing Machinery, New York, NY, USA, 164–172. doi:10.1...

arXiv 2017
[4]

Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mört- berg. 2018. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In21st International Conference on Types for Proofs and Programs (TYPES 2015) (Leibniz International Proceed- ings in Informatics (LIPIcs), Vol. 69), Tarmo Uustalu (Ed.). Schloss Dagstuhl – Leibniz-Zentrum für...

doi:10.4230/lipics.types.2015.5 2018
[5]

2024.Coq-HoTT — Zigza- gIdentity branch.https://github.com/ThomatoTomato/HoTT/blob/ ZigzagIdentity/theories/PushoutPath/PushoutPath.vAccessed on 2025-13-09

Ben Connors and Thomas Thorbjørnsen. 2024.Coq-HoTT — Zigza- gIdentity branch.https://github.com/ThomatoTomato/HoTT/blob/ ZigzagIdentity/theories/PushoutPath/PushoutPath.vAccessed on 2025-13-09

2024
[6]

Nicolai Kraus and Jakob von Raumer. 2019. Path Spaces of Higher Inductive Types in Homotopy Type Theory. InProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science(Vancou- ver, Canada)(LICS ’19). IEEE Press, Article 7, 13 pages

2019
[7]

Egbert Rijke. 2019. Classifying Types. arXiv:1906.09435 [math.LO] https://arxiv.org/abs/1906.09435

arXiv 2019

Show all 14 references

[8]

2022.Introduction to Homotopy Type Theory

Egbert Rijke. 2022.Introduction to Homotopy Type Theory. arXiv:2212.11082 [math.LO]

2022 arXiv
[9]

2025.The agda-unimath library

Egbert Rijke, Elisabeth Stenholm, Jonathan Prieto-Cubides, Fredrik Bakke, Vojtěch Štěpančík, and others. 2025.The agda-unimath library. https://github.com/UniMath/agda-unimath/Accessed on 2025-17-07

2025
[10]

Kristina Sojakova, Floris van Doorn, and Egbert Rijke. 2020. Sequential Colimits in Homotopy Type Theory. InProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science(Saarbrücken, Germany)(LICS ’20). Association for Computing Machinery, New York, NY, USA, 8...

2020
[11]

2013.Homotopy Type Theory: Univalent Foundations of Mathematics.https://homotopytypetheory

The Univalent Foundations Program. 2013.Homotopy Type Theory: Univalent Foundations of Mathematics.https://homotopytypetheory. org/book, Institute for Advanced Study

2013
[12]

David Wärn. 2023. Path Spaces of Pushouts. (2023).https://dwarn.se/ po-paths.pdfAccessed on 2023-30-09

2023
[13]

David Wärn. 2024. Path Spaces of Pushouts. arXiv:2402.12339 [math.AT]

2024 arXiv

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.

[1] [14]

commuting squares of sections

Vojtěch Štěpančík. 2024. Formalization of Homotopy Pushouts in Homotopy Type Theory. A Commuting shapes and coherences We use two kinds of diagrams: non-dependent ones, which express commutativity of non-dependent functions between types, and commutativity of such homotopies; and depen- dent ones, which can express diagrams involving type fami- lies, fibe...

2024

[2] [1]

2025.Agda.https://agda.readthedocs.io/

Agda Developers. 2025.Agda.https://agda.readthedocs.io/

2025

[3] [2]

Steve Awodey and Michael A. Warren. 2009. Homotopy theoretic mod- els of identity types.Mathematical Proceedings of the Cambridge Philo- sophical Society146, 1 (2009), 45–55. doi:10.1017/S0305004108001783

doi:10.1017/s0305004108001783 2009

[4] [3]

Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shul- man, Matthieu Sozeau, and Bas Spitters. 2017. The HoTT library: a formalization of homotopy type theory in Coq. InProceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs(Paris, France)(CPP 2017). Association for Computing Machinery, New York, NY, USA, 164–172. doi:10.1...

arXiv 2017

[5] [4]

Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mört- berg. 2018. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In21st International Conference on Types for Proofs and Programs (TYPES 2015) (Leibniz International Proceed- ings in Informatics (LIPIcs), Vol. 69), Tarmo Uustalu (Ed.). Schloss Dagstuhl – Leibniz-Zentrum für...

doi:10.4230/lipics.types.2015.5 2018

[6] [5]

2024.Coq-HoTT — Zigza- gIdentity branch.https://github.com/ThomatoTomato/HoTT/blob/ ZigzagIdentity/theories/PushoutPath/PushoutPath.vAccessed on 2025-13-09

Ben Connors and Thomas Thorbjørnsen. 2024.Coq-HoTT — Zigza- gIdentity branch.https://github.com/ThomatoTomato/HoTT/blob/ ZigzagIdentity/theories/PushoutPath/PushoutPath.vAccessed on 2025-13-09

2024

[7] [6]

Nicolai Kraus and Jakob von Raumer. 2019. Path Spaces of Higher Inductive Types in Homotopy Type Theory. InProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science(Vancou- ver, Canada)(LICS ’19). IEEE Press, Article 7, 13 pages

2019

[8] [7]

Egbert Rijke. 2019. Classifying Types. arXiv:1906.09435 [math.LO] https://arxiv.org/abs/1906.09435

arXiv 2019