Homotopy Type Theory (HoTT) develops Martin-Lof Intuitionistic Type Theory (ITT) by adding axioms for equality that are directly inspired by analogies with Homotopy Theory in Mathematics. The key source of information is http://homotopytypetheory.org/ and we shall be loosely following the HoTT book which is freely available at http://homotopytypetheory.org/2013/06/20/the-hott-book/

I will aim to cover the material in Chapter 1. I'll summarise the foundations (as I understand them), remind people about the idea of dependent types, and explain the various basic constructs and the associated induction principles. I hope to be able to get as far as path induction, which is the point where HoTT starts to look different and interesting. I might be able to state (but not say anything about) univalence.

To get to campus, take the train from Birmingham New Street to the University stop (7 minutes).

School of Mathematics

University of Birmingham

http://web.mat.bham.ac.uk/R.W.Kaye/

Dr Walter Dean

Department of Philosophy

University of Warwick

http://go.warwick.ac.uk/whdean