单向 homotopy type theory 中的计算合成上同调理论

本文讨论了在单向 homotopy type theory (HoTT) 中 developing synthetic cohomology 及其计算机形式化的工作。本文的目标包括：(1) 将作者们及 Brunerie (2022) 关于整数上同调在 HoTT 中的工作推广至任意系数的上同调；(2) 提供以及扩展支撑作者们及 Lamiaux (2023) 进行上同调环计算机形式化所需的数学细节。针对目标 (1)，我们提供了上同调群运算和 cup product 的新型直接定义，这些定义如同 (Brunerie 等，2022) 那样，使许多早期证明在合成上同调理论中得到显著简化。特别是，新的 cup product 定义使得我们能够给出将上同调群构成graded交换环所需的公理的第一次完整形式化。我们还证明该上同调理论满足 HoTT 表述的 Eilenberg-Steenrod 上同调公理，并研究经典的 Mayer-Vietoris 序列和 Gysin 序列。针对目标 (2)，我们描述了各种空间的上同调群和环，包括球面、环面、Klein 瓶、实/复射影平面以及无限实射影空间。所有结果均在 Cubical Agda 中形式化，我们获得了多个新的数值（类似著名的 Brunerie 数），可作为计算实现 HoTT 的基准。其中一些数值在 Cubical Agda 中难以计算，从而提供了新的计算挑战和开放问题，这些问题比原始 Brunerie 数更容易定义。