Skip to main content

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

Time: Wed 2019-12-11 10.00 - 11.45

Location: Kräftriket, house 5, room 16

Participating: Anders Mörtberg, Stockholms universitet


This will be a continuation of last week’s seminar .

The recently developed cubical mode of Agda allows the userto 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.