Timings and Venue:

• Lectures: Tuesday, Thursday 9:30 a.m. to 11:00 a.m.

• Venue: Lecture Hall - III (ground floor), Department of Mathematics.

• First lecture: Tuesday, January 6, 2015 at 9:30 a.m.

Instuctor : Siddhartha Gadgil

E-mail: siddhartha.gadgil@gmail.com

Exercise submission:

To submit an exercise please e-mail the instructor with the subject containing LTS (as a separate word). All exercises in the blog/lectures are to be submitted within a week of posting.

Grades

The grades will be based on a composite score consisting of

• Assignments - 20% (code)
• Project - 30% (code)
• Midterm - 20% (theory)
• Final - 30% (theory)

For the project, the student is expected to formalize some mathematical structures and results in Homotopy type theory using Agda (as a literate agda file).

Course description:

The following is an overview of the topics in the course. We shall try to work most of the time within the language/formal proof system Agda.

Reasoning with types.

Traditionally, foundations of mathematics are based on the Axioms of Set theory with the rules of reasoning given by First-order Logic. While these are in principle solid foundations, in practice most mathematics is so far removed from its set theoretic description that even the existence of such a description is essentially an act of faith. Type theoretic foundations are much closer to actual mathematics, and have many other advantages. Furthermore, (dependent) type theory provides in a uniform way both the objects of study and the methods of reasoning about them. In the first part of this course, we shall see basic type theoretic foundations, including how to reason with types.

Limits of Reasoning.

Among the most fascinating aspects of logic are the limits of reasoning - the existence of (true) theorems we cannot prove, functions we cannot compute, objects we cannot describe. In the second part of the course we shall study these. Specifically we see the proof due to Chaitin of Godel’s incompleteness theorem and a proof of the existence of uncomputable functions.

First order logic and models.

First order logic (predicate calculus) is in many ways the best behaved system of reasoning. In particular the completeness theorem of Godel shows that its reasoning rules are in some sense correct, and Godel’s compactness theorem has applications outside logic. We shall study the basic concepts of first-order logic, including models. These will be viewed as objects within type theory.

Homotopy type theory.

Types can be interpreted as spaces, with terms of a type points of the corresponding space. This analogy turns out to give deep connections between various aspects of type theory and homotopy theory. We shall introduce this new and beautiful subject.

Resouces:

• The code for this course is available on Github, with the code in lectures in a folder called livecode.

• Our main reference is the HoTT book.

• The Agda wiki contains many Tutorials.

• There is a nice introduction to Agda for HoTT by Guillaume Brunerie.