Axel Ljungström: An Excursion Into Algebraic Topology and Homotopy Type Theory

Abstract

I will give an overview of the fundamental concepts of algebraic topology and discuss how these concepts underpin Homotopy Type Theory, a relatively new constructive foundation of mathematics. I will then present some ongoing work on developing computationally efficient integer cohomology in Cubical Agda, a proof assistant for Homotopy Type Theory.