Core Concepts
HoTTにおける合成コホモロジー理論の開発とコンピュータ形式化に焦点を当てる。
Abstract
この論文は、HoTT(Homotopy Type Theory)における合成コホモロジーの発展とそのコンピュータ形式化について議論しています。主な目的は、前作であるBrunerieらによるHoTT内の整数コホモロジーの一般化と、現在の著者らとLamiaux(2023)による共変係数を持つコホモロジーへの拡張を含む。新しい直接的な定義やカップ積などが提供され、多くの以前の証明が簡素化されます。さらに、Eilenberg-Steenrod公理やMayer-Vietoris列なども検討されます。
合成コホモロジー理論の新しい定義と操作方法が提供されます。
HoTTでEilenberg-Steenrod公理を満たすことが確立されます。
様々な空間のコホモロジーグループやリングが特徴付けられます。
Cubical Agdaで全ての結果が形式化され、計算上の課題やオープン問題も提示されます。
Stats
HoTT(Homotopy Type Theory)
Brunerie et al. [2022]
Lamiaux et al. [2023]
Cubical Agda