### 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. 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.

Original language | English (US) |
---|---|

Title of host publication | Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 |

Publisher | Institute of Electrical and Electronics Engineers Inc. |

Pages | 521-529 |

Number of pages | 9 |

ISBN (Electronic) | 9781450355834, 9781450355834 |

DOIs | |

State | Published - Jul 9 2018 |

Externally published | Yes |

Event | 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 - Oxford, United Kingdom Duration: Jul 9 2018 → Jul 12 2018 |

### Publication series

Name | Proceedings - Symposium on Logic in Computer Science |
---|---|

ISSN (Print) | 1043-6871 |

### Conference

Conference | 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 |
---|---|

Country | United Kingdom |

City | Oxford |

Period | 7/9/18 → 7/12/18 |

### Keywords

- Cellular cohomology
- Homotopy type theory
- Mechanized reasoning

## Fingerprint Dive into the research topics of 'Cellular cohomology in homotopy type theory'. Together they form a unique fingerprint.

## Cite this

*Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018*(pp. 521-529). (Proceedings - Symposium on Logic in Computer Science). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1145/3209108.3209188