1: \begin{abstract}

2:   We present a development of cellular cohomology in homotopy type theory.

3:   Cohomology associates to each space a sequence of abelian groups

4:   capturing part of its structure,

5:   and has the advantage over homotopy groups in that

6:   these abelian groups of many common spaces are easier to compute.

7:   Cellular cohomology is a special kind of cohomology designed for cell complexes:

8:   these are built in stages by attaching spheres of progressively higher dimension,

9:   and cellular cohomology defines the groups out of the combinatorial description

10:   of how spheres are attached.

11:   Our main result is that for finite cell complexes,

12:   a wide class of cohomology theories

13:   (including the ones defined through Eilenberg-MacLane spaces)

14:   can be calculated via cellular cohomology.

15:   This result was formalized in the Agda proof assistant.

16: \end{abstract}

17: