Every proof assistant: Cubical Agda – A Dependently Typed Programming Language with Univalence and Higher Inductive Types

• 10 September 2020
• Andrej Bauer
• Talks, Every proof assistant

I am happy to announce that we are restarting the "Every proof assistants" series of talks with Anders Mörtberg who will talk about Cubical Agda. Note that we are moving the seminar time to a more reasonable hour, at least as far as the working people in Europe are concerned.

Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types

Time: Thursday, September 17, 2020 from 15:00 to 16:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Anders Mörtberg (Stockholm University)
Proof assistant: Cubical Agda

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.

The talk video recording is available.

We have more talks in store, but we will space them out a bit to give slots to our local seminar.