Material for the course: Inductive and Inductive-Recursive Definitions in Type Theory, OPLSS 2015, Eugene, Oregon

Articles: Further reading: Agda files: Exercises: