一句话：在同伦类型论中通过无序 join 这一高阶归纳类型证明 Steenrod 平方的核心性质，并给出 Cubical Agda 形式化。
Steenrod 平方是代数拓扑中重要的上同调运算，但在同伦类型论（HoTT）中，尽管 Brunerie（2017）曾给出定义，其刻画性质的证明仍长期缺失。本文重新审视该定义，通过研究一个称为无序 join 的高阶归纳类型，以合成方式证明稳定性、Cartan 公式和 Adem 关系等核心性质。由于方法本质上是合成的，许多证明与经典证明有显著差异；作者还讨论了 HoTT 作为同伦论合成语言的收获与局限。所有结果均在 Cubical Agda 中完成机器形式化。
The Steenrod squares are cohomology operations with important applications in algebraic topology. While these operations are well-understood classically, little is known about them in the setting of homotopy type theory. Although a definition of the Steenrod squares was put forward by Brunerie (2017), proofs of their characterising properties have remained elusive. In this paper, we revisit Brunerie’s definition and provide proofs of these properties, including stability, Cartan’s formula and the Adem relations. This is done by studying a higher inductive type called the unordered join. This approach is inherently synthetic and, consequently, many of our proofs differ significantly from their classical counterparts. Along the way, we discuss upshots and limitations of homotopy type theory as a synthetic language for homotopy theory. The paper is accompanied by a computer formalisation in Cubical Agda.
DOI 原文 ·
@inproceedings{paperbot8678,
title = {The Steenrod squares via unordered joins},
author = {Axel Ljungström and David Wärn},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00029}
}