形式化路径空间推导图构造
逻辑
2025-10-10 v1 代数拓扑
摘要
最近的预印本中，W"arn 提出了一种新颖的纸面构造方法，用于描述任意推导图路径空间的类型族，并给出其正确性的自然语言论证。我们present了该构造的第一次形式化，以及证明其在纤维上等价于路径空间的论证。该形式化在公理化同伦类型论中进行，使用 Agda 证明助理和 agda-unimath 库完成。
引用
@article{arxiv.2510.08452,
title = {Formalizing the zigzag construction of path spaces of pushouts},
author = {Vojtěch Štěpančík},
journal= {arXiv preprint arXiv:2510.08452},
year = {2025}
}
备注
15 pages, 4 figures, submitted to CPP 2026