Material for the course: Intuitionistic Type Theory, Summer School on Types, Sets and Constructions Hausdorff Research Institute for Mathematics, Bonn, 3 - 9 May, 2018
Slides:
Lecture 1
Lecture 2
Lecture 3
Articles:
Peter Dybjer and Erik Palmgren,
Intuitionistic Type Theory
, Stanford Encyclopedia of Philosohpy (2016).
Per Martin-Löf,
An Intuitionistic Theory of Types
(1972)
Per Martin-Löf,
Constructive Mathematics and Computer Programming
(LMPS 1979)
Per Martin-Löf,
Intuitionistic Type Theory
(Bibliopolis 1984)
Further reading:
An Introduction to Programming and Proving in Agda
, Jan 2018
My papers on the syntax and semantics of inductive and inductive-recursive definitions
My paper and talk on generic programming in dependent type theory
Agda files:
The Logical Framework
Predicate logic and Martin-Löf type theory
Inductive types
Some small proofs
Inductive families
Induction-recursion
Semantics
Aczel's iterative sets and CZF
Records
Identity
Finite subsets
Categories with families
Tar-file with all of the above
Exercises:
Agda exercises