Every proof assistant seminar series: Cubical Agda (September 17, 2022)

[Andrej Bauer]

It is my pleasure to announce the next talk in the Every proof
assistant on-line seminar series. We are starting the Fall season with
Anders Mörtberg who will talk about Cubical Agda.

With kind regards,

Andrej

CUBICAL AGDA: A DEPENDENTLY TYPED PROGRAMMING LANGUAGE WITH UNIVALENCE
AND HIGHER INDUCTIVE TYPES

Anders Mörtberg
Stockholm University

Thursday, September 17, 2020
15:00 to 16:00 (Central European Summer Time, UTC+2)

Location: online at Zoom ID 989 0478 8985, https://zoom.us/j/98904788985
Proof assistant: Cubical Agda, https://github.com/agda/cubical

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.