Matthew Burke

Title: Introduction to univalence in Coq
Abstract: This week we begin a sequence of talks on homotopy type theory (HoTT). In this first talk we introduce the elementary definitions and tactics that are required to get started with HoTT using the Coq proof assistant. We endeavour to introduce as little programming syntax as possible and develop the theory using only a very few syntactic constructs that have clear mathematical interpretations.
The audience is encouraged to follow the development of the theory on their own computers so please bring a laptop if you want to do this! (You will need about 300mb of space to install the Coq proof assistant.) There will be short exercises that the audience can complete at their own pace which will not be vital to the theory but rather are intended to familiarise the audience with the proof assistant and tactics.