Material for the course: Inductive and Inductive-Recursive Definitions in Type Theory, OPLSS 2015, Eugene, Oregon
Articles:
Peter Dybjer and Erik Palmgren,
Intuitionistic Type Theory
, article to appear in Stanford Encyclopedia of Philosohpy (2015).
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:
My papers on the syntax and semantics of inductive and inductive-recursive definitions
My paper and talk on generic programming in dependent type theory
(the talk is recommended reading!)
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