Anders Mörtberg: Programming and proving with higher inductive types in Cubical Agda

Time: Wed 2019-12-04 10.00 - 11.45

Lecturer: Anders Mörtberg

Location: Kräftriket, house 5, room 16

Abstract

The recently developed cubical mode of Agda allows the user to define their own higher inductive types (HITs). The user can then also conveniently program and reason about these using pattern-matching. I will show a variety of examples, taken from computer science, logic, algebra and synthetic homotopy theory, that we have developed in Cubical Agda. Working in a system with native support for HITs has many benefits compared to working axiomatically. For example, the proof of the 3x3 lemma for pushouts is less than 200 lines in Cubical Agda which can be compared to the 3000 line proof in HoTT-Agda with postulated HITs.

Page responsible:webmaster@math.kth.se
Belongs to: Department of Mathematics
Last changed: Nov 28, 2019