Skip to main content
To KTH's start page To KTH's start page

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

Time: Wed 2019-12-04 10.00 - 11.45

Location: Kräftriket, house 5, room 16

Participating: Anders Mörtberg

Export to calendar


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.