Skip to main content

Axel Ljungström: Computing Cohomology with Cubical Agda

MSc Thesis Presentation

Time: Tue 2020-08-25 10.00 - 11.00

Location: Zoom, meeting ID: 61549286742

Participating: Axel Ljungström

Supervisor: Guillaume Brunerie, Anders Mortberg


Cubical Agda is a proof assistant for Cubical Type Theory (CuTT), a recent flavour of Homotopy Type Theory (HoTT), which gives a constructive interpretation of univalence. The goal of this thesis is to characterise, formally in Cubical Agda, the zeroth, first and second cohomology groups with integer coefficients of the torus and of the wedge sum of a sphere and two circles. We first introduce type theory, HoTT, CuTT and Cubical Agda. We then work our way up to cohomology, defined in terms of Eilenberg-MacLane spaces, and the Mayer-Vietoris sequence. Finally, we characterise some of the cohomology groups of the unit type, n-spheres, 0-connected types and wedge sums. Using these results, we characterise the cohomology groups in question.