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!
|
Table of 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.