# Type Theory (MGS 2021)

Type Theory is at the same time an alternative to set theory as a
mathematical foundation and a programming language originally
conceived by the Swedish philosopher and mathematician Per
Martin-Löf. The course is an introduction to Type Theory which covers
the following topics:
- (Simpy typed) λ-calculus and combinatory logic
- Propositions as types
- Classical vs intuitionistic reasoning
- Dependent types, Π- and Σ-types
- Reasoning in Type Theory, Equality
- Inductive and coinductive types
- Universes and paradoxes

I will use the agda system for examples and exercises. Chapters from my
forthcoming book (*The Tao of Types*) will be made available to the
participants.
## Lecture notes (chapters of Tao of Types):

- Simple types
- Propositional logic
- Datatypes
- Dependent types
- Predicate logic

## Material from the lectures:

- Monday (intro, functions)
- whiteboard, agda
- Tuesday (sums and products, propositional logic)
- agda
- Wednesday (classical logic, inductive datatypes)
- agda (uses mylib.agda)
- Thursday (coinductive datatypes, dependent types)
- agda (uses mylib.agda)
- Friday (Dependent types, predicate logic, equality) )
- agda (uses mylib.agda), whiteboard

## Exercises:

- Monday
- solutions
- Tuesday
- mylib.agda
- Wednesday
- mylib.agda has been extended!
- Thursday
- mylib.agda has been extended again!

Last modified: Fri Apr 16 10:07:21 BST 2021