Formalizing the zigzag construction of path spaces of pushouts
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _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 |