Monday 14-16, HS B 252, start 16th October 2017

The objective is to encourage students to make use of proof assistants in their study of mathematics. I use Agda for demonstration.

**Outline**

- Introduction
- Computer assisted formalisation of mathematics
- Martin-Löf type theory & "Proofs as Programs"
- Introduction to the Agda proof assistant

- Continuity in type theory

I will present some results about continuity from my PhD thesis to show- the subtle problem of expressing "existence" in type theory, and
- how to make axioms computational.

- The Fan theorem

Dr. Josef Berger is lecturing a course on the Fan theorem (Wednesday 14-16, B040). I'd like to invite students to attend his lectures and formalise some results of the Fan theorem in Agda. - Real numbers

The last part of the course is to develop a basic fragment of the theory of real numbers in Agda, following the method of Prof. Helmut Schwichtenberg in his previous course on constructive analysis.

**Literature**

- Agda and type theory
- The Agda wiki
- Dependently Typed Programming in Agda. U.Norell and J. Chapman
- Chapter 1 of the HoTT book

- Continuity and the Fan theorem
- A continuous computational interpretation of type theories. Chuangjie Xu, PhD thesis, 2015.
- The webpage of Dr. Berger's course on the Fan theorem

- Analysis
- Constructive analysis with witnesses. Helmut Schwichtenberg, lecture notes, wintersemester 2016/17, LMU.

**Lecture codes and exercises**

- 16.10.2017: Introduction I (Agda file, html format). Exercise: Install Agda and run the example in the lecture codes.
- 23.10.2017: Introduction II (unfilled lecture codes, lecture codes, html format). Exercise: Prove the 5 logical axioms left in the lecture codes.
- 30.10.2017: Arithmetic (unfilled lecture codes, lecture codes, html format). Exercise: Prove the 4 properties of multiplications left in the lecture codes.
- 06.11.2017: Continuity in Type Theory I (slides, informal proof, unfilled lecture codes, lecture codes).
- 13.11.2017: Continuity in Type Theory II (slides, unfilled lecture codes, lecture codes, html format). Exercise: Complete the logic of propositions.
- 20.11.2017: Uniform Continuity in Type theory (slides, unfilled lecture codes, lecture codes).

Last modified: Mon 20th Nov 2017