  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.
