Course Description: 

Martin-Löf type theory (MLTT) provides an alternative to the usual set-theoretic foundations of mathematics where the fundamental notions are type and term rather than set and element. An unusual feature of this theory is that it is expressive enough to both define mathematical objects, e.g. the natural numbers, and also to provide a kind of internal logic sufficient to state theorems, aid in the formulation of proofs, and check their correctness.  It therefore functions as a constructive logic which subsitutes for the predicate calculus. Proof verification rests on the Curry-Howard Correpondence: the idea that propositions can be formulated as types, in which case proofs are given by terms of those types.
The aim of the first part of this course is to present the basics of MLTT, showing how it can be used to construct a small repertoire of mathematical objects, and showing how the internal logic is set up and used to build proofs.  We will give special attention to the theory of the identity type, a particularly subtle notion that underlies almost all applications. 
The last part of the course will be devoted to Homotopy Type Theory, an extension of MLTT in which types are viewed as spaces up to homotopy, terms are viewed as points, and terms of the identity type are viewed as paths up to homotopy.  The result is a kind of fusion of computer science, logic, and topology.

Course Schedule:

  8   April,  11:00-12:30

  10 April,  11:00-12:30

  15 April,  11:00-12:30

  17 April,  11:00-12:30

  22 April,  11:00-12:30

  24 April,  11:00-12:30

  29 April,  11:00-12:30

  1   May,  11:00-12:30