Axel Ljungström: An Excursion Into Algebraic Topology and Homotopy Type Theory
Time: Wed 2021-03-03 14.00 - 14.45
Location: Zoom, meeting ID: 611 3329 7865
Participating: Axel Ljungström
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.