Publications

2023
Computing Cohomology Rings in Cubical Agda Doi Arxiv Pdf Slides Video
Thomas Lamiaux , Axel Ljungström , Anders Mörtberg ,
CPP 2023 , Distinguished Paper

In the paper, we explain how to formalize Cohomology Rings in synthetic mathematics. With a special focus on data structures and how they influence formalization, most noticeably the direct sum and (multivariate) polynomials.