Proof and Computation Autumn School 2022: Universes of data types in constructive type theory

Slides

• Lecture 1: Martin-Löf Type Theory
• Lecture 2: Inductive data types (SP.agda, decEq.agda)
• Lecture 3: Inductive families, and inductive-recursive definitions (fin.agda, SPF.agda, IR.agda, small-IR-to-SPF.agda)

Last modified: Fri Sep 30 19:01:27 BST 2022.