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
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.