In Homotopy Type Theory, cohomology theories are studied synthetically using higher inductive types and univalence. This paper extends previous developments by providing the first fully mechanized definition of cohomology rings. These rings may be defined as direct sums of cohomology groups together with a multiplication induced by the cup product, and can in many cases be characterized as quotients of multivariate polynomial rings. To this end, we introduce appropriate definitions of direct sums and graded rings, which we then use to define both cohomology rings and multivariate polynomial rings. Using this, we compute the cohomology rings of some classical spaces, such as the spheres and the Klein bottle. The formalization is constructive so that it can be used to do concrete computations, and it relies on the Cubical Agda system which natively supports higher inductive types and computational univalence.

翻译：在同族体类型理论中,对共生学理论进行合成研究,使用较高的感应类型和独生体来研究共生学理论。本文件扩展了先前的发展,提供了第一种完全机械化的共生环定义。这些环可被定义为共生组的直接总和,加上杯子产品引起的倍增,在许多情况下可被定性为多变量多元圆环的商数。为此,我们引入了直接数和分级环的适当定义,然后我们用这些定义来定义共生圈和多变多元圆环。我们使用这个定义来计算一些古典空间的共生组,如球体和克莱因瓶。正规化具有建设性,可以用来进行混凝土计算,它依靠Cubical Agda 系统,这个系统本地支持较高的传导型和计算独生体。