Matthew Burke

Title: Introduction to univalence in Coq III
Abstract: This week we continue our sequence of talks on homotopy type theory (HoTT) for which we are approaching the denouement. First we define h-propositions and what it means to be a contractible type. Then we distinguish between a couple of different types of equivalence and show that a particular choice satisfies all the conditions for being an h-proposition. If we have time we will formulate the univalence axiom and make some straightforward deductions that illustrate its use.
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.