Week 1, 14 January (17:00-19:00 Watson 310)

Study group (double session): Richard Kaye (Birmingham)


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.

About the seminar

The Midlands Logic Seminar was founded in 2011 and aims to cover all areas of mathematical logic, as well as related areas of theoretical computer science, and philosophy of mathematics.


All meetings for Term 2, 2013-14 will be Tuesday from 17:00-19:00 in room 310 of Watson Building (School of Mathematics) on the campus of the University of Birmingham.
  • campus map
  • google maps
    To get to campus, take the train from Birmingham New Street to the University stop (7 minutes).


    Dr Richard Kaye
    School of Mathematics
    University of Birmingham


    Dr Walter Dean
    Department of Philosophy
    University of Warwick