Creative Commons Attribution 4.0 license (CC BY 4.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2022.11
URN: urn:nbn:de:0030-drops-157310
URL: https://drops.dagstuhl.de/opus/volltexte/2022/15731/
Brunerie, Guillaume ; Ljungström, Axel ; Mörtberg, Anders
Synthetic Integral Cohomology in Cubical Agda
| pdf-format: |
|
Abstract
This paper discusses the formalization of synthetic cohomology theory in a cubical extension of Agda which natively supports univalence and higher inductive types. This enables significant simplifications of many proofs from Homotopy Type Theory and Univalent Foundations as steps that used to require long calculations now hold simply by computation. To this end, we give a new definition of the group structure for cohomology with ℤ-coefficients, optimized for efficient computations. We also invent an optimized definition of the cup product which allows us to give the first complete formalization of the axioms needed to turn the integral cohomology groups into a graded commutative ring. Using this, we characterize the cohomology groups of the spheres, torus, Klein bottle and real/complex projective planes. As all proofs are constructive we can then use Cubical Agda to distinguish between spaces by computation.
BibTeX - Entry
@InProceedings{brunerie_et_al:LIPIcs.CSL.2022.11,
author = {Brunerie, Guillaume and Ljungstr\"{o}m, Axel and M\"{o}rtberg, Anders},
title = {{Synthetic Integral Cohomology in Cubical Agda}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {11:1--11:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/15731},
URN = {urn:nbn:de:0030-drops-157310},
doi = {10.4230/LIPIcs.CSL.2022.11},
annote = {Keywords: Synthetic Homotopy Theory, Cohomology Theory, Cubical Agda}
}
| Keywords: | Synthetic Homotopy Theory, Cohomology Theory, Cubical Agda | |
| Seminar: | 30th EACSL Annual Conference on Computer Science Logic (CSL 2022) | |
| Issue date: | 2022 | |
| Date of publication: | 27.01.2022 | |
| Supplementary Material: |
A complete formalization of all results in the paper can be found at: Software (Source Code): https://github.com/agda/cubical/blob/master/Cubical/Papers/ZCohomology.agda |
