Axel Ljungström: Computing Cohomology with Cubical Agda

Abstract

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.