Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I have made the requested cellular redirect to the existing entry cellular homology. (Once an entry cellular cohomology exists we should change this).
Also, I have hyperlinked homomotopy type theory (please keep doing this, it cannot be assumed to be self-explanatory in the wider context of the nLab).
Finally, I have made cohomology point to ordinary cohomology, for better user experience
In adding the missing publication data, I have taken the liberty of re-formatting. Does it not look much better the following way:
Ulrik Buchholtz, Kuen-Bang Hou (Favonia):
Cellular Cohomology in Homotopy Type Theory
Logical Methods in Computer Science, 16 2 (2020)
Abstract. We present a development of cellular cohomology in homotopy type theory. Cohomology associates to each space a sequence of abelian groups capturing part of its structure, and has the advantage over homotopy groups in that these abelian groups of many common spaces are easier to compute in many cases. Cellular cohomology is a special kind of cohomology designed for cell complexes: these are built in stages by attaching spheres of progressively higher dimension, and cellular cohomology defines the groups out of the combinatorial description of how spheres are attached. Our main result is that for finite cell complexes, a wide class of cohomology theories (including the ones defined through Eilenberg-MacLane spaces) can be calculated via cellular cohomology. This result was formalized in the Agda proof assistant.
1 to 3 of 3