Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2510.08452 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909833187295232 |
|---|---|
| author | Štěpančík, Vojtěch |
| author_facet | Štěpančík, Vojtěch |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_08452 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formalizing the zigzag construction of path spaces of pushouts Štěpančík, Vojtěch Logic Algebraic Topology 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. |
| title | Formalizing the zigzag construction of path spaces of pushouts |
| topic | Logic Algebraic Topology |
| url | https://arxiv.org/abs/2510.08452 |