Anders Mörtberg: Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types
Attention: we meet at a non-standard time on Thursday, 17. 9. 2020 at 15:00!
Anders Mörtberg (Stockholm University)
The talk will be recorded and posted online.
Abstract: The dependently typed programming language Agda has recently been extended with a cubical mode which provides extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically to proof assistants based on dependent type theory which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. In the talk I will discuss how Agda was extended to a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. I will also show a variety of examples of how to use Cubical Agda in practice to reason about mathematics and computer science.
