Till innehåll på sidan
Till KTH:s startsida Till KTH:s startsida

Axel Ljungström: Computing Cohomology with Cubical Agda

MSc Thesis Presentation

Tid: Ti 2020-08-25 kl 10.00 - 11.00

Plats: Zoom, meeting ID: 61549286742

Medverkande: Axel Ljungström

Handledare: Guillaume Brunerie, Anders Mortberg

Exportera till kalender


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.