Cellular Cohomology in Homotopy Type Theory

摘要

We present a development of cellular cohomology in homotopy type theory.Cohomology associates to each space a sequence of abelian groups capturing partof its structure, and has the advantage over homotopy groups in that theseabelian groups of many common spaces are easier to compute. Cellular cohomologyis a special kind of cohomology designed for cell complexes: these are built instages by attaching spheres of progressively higher dimension, and cellularcohomology defines the groups out of the combinatorial description of howspheres are attached. Our main result is that for finite cell complexes, a wideclass of cohomology theories (including the ones defined throughEilenberg-MacLane spaces) can be calculated via cellular cohomology. Thisresult was formalized in the Agda proof assistant.