This paper discusses the development of synthetic cohomology in Homotopy Type Theory (HoTT), as well as its computer formalisation. The objectives of this paper are (1) to generalise previous work on integral cohomology in HoTT by the current authors and Brunerie (2022) to cohomology with arbitrary coefficients and (2) to provide the mathematical details of, as well as extend, results underpinning the computer formalisation of cohomology rings by the current authors and Lamiaux (2023). With respect to objective (1), we provide new direct definitions of the cohomology group operations and of the cup product, which, just as in (Brunerie et al., 2022), enable significant simplifications of many earlier proofs in synthetic cohomology theory. In particular, the new definition of the cup product allows us to give the first complete formalisation of the axioms needed to turn the cohomology groups into a graded commutative ring. We also establish that this cohomology theory satisfies the HoTT formulation of the Eilenberg-Steenrod axioms for cohomology and study the classical Mayer-Vietoris and Gysin sequences. With respect to objective (2), we characterise the cohomology groups and rings of various spaces, including the spheres, torus, Klein bottle, real/complex projective planes, and infinite real projective space. All results have been formalised in Cubical Agda and we obtain multiple new numbers, similar to the famous `Brunerie number', which can be used as benchmarks for computational implementations of HoTT. Some of these numbers are infeasible to compute in Cubical Agda and hence provide new computational challenges and open problems which are much easier to define than the original Brunerie number.

翻译：本文讨论了同伦类型论（HoTT）中综合上同调的发展及其计算机形式化。本文的目标是：（1）将当前作者与Brunerie（2022）在HoTT中关于整系数上同调的先前工作推广到任意系数的上同调；（2）提供当前作者与Lamiaux（2023）关于上同调环的计算机形式化所依赖结果的数学细节，并对其进行扩展。针对目标（1），我们给出了上同调群运算和杯积的新直接定义，与（Brunerie et al., 2022）类似，这些定义显著简化了综合上同调理论中的许多早期证明。特别是，杯积的新定义使我们能够首次完整形式化将上同调群转化为分次交换环所需的公理。我们还证明该上同调理论满足Eilenberg-Steenrod上同调公理的HoTT表述，并研究了经典的Mayer-Vietoris序列和Gysin序列。针对目标（2），我们刻画了多种空间的上同调群和环，包括球面、环面、克莱因瓶、实/复射影平面以及实无限射影空间。所有结论已在Cubical Agda中形式化，并获得了多个类似于著名"Brunerie数"的新数值，这些数值可作为HoTT计算实现的基准。其中部分数值在Cubical Agda中计算不可行，因此提供了比原始Brunerie数更易定义的新计算挑战和开放问题。