Axel Ljungström: Cohomology in Cubical Type Theory and Agda
Time: Wed 2020-12-09 10.00 - 12.00
Location: Zoom, meeting ID: 610 2070 5696
Participating: Axel Ljungström
Cubical Type Theory (CuTT) is an alternative to Homotopy Type Theory in which univalence has a constructive interpretation. In CuTT, we can easily define cohomology groups by means of Eilenberg-MacLane spaces (EM-spaces). This construction allows us to work with cohomology in a very synthetic manner which often captures a good deal of naive topological intuition. Additionally, since univalence has computational content in Cubical Agda, a proof assistant for CuTT, we should be able to make explicit computations concerning cohomology groups. These computations, however, often turn out to be incredibly complex and we run into problems already at cohomology in dimension 2.
In this talk, I will discuss my latest efforts in making cohomology compute better. In particular, I will present a more direct definition of the addition operation on EM-spaces (over the integers) which satisfies some definitional equalities that the usual definition does not satisfy. Furthermore, I will show how this definition is used to give easy proofs of the fact that loop spaces over EM-spaces are commutative and of the fact that the n:th EM-space is equivalent to the loop space of the (n+1):th EM-space. Finally, I will present direct characterisations of some cohomology groups (e.g. those of spheres, wedge sums, the torus and the klein bottle) and show some computations in Cubical Agda.