Course materials for the Midlands Graduate School 2026 lecture series on Type Theory with Agda.
Lecturer: Thorsten Altenkirch (University of Nottingham)
This course introduces dependent type theory through hands-on programming in Agda. We start from the basics and work up to cubical type theory and the univalence axiom.
| Day | Topic |
|---|---|
| Monday | Introduction: natural numbers, equality, induction |
| Tuesday | Dependent types in programming: Vec, Fin, matrices |
| Wednesday | Dependent types in logic: order relations, natural deduction |
| Thursday | The mystery of equality: J, K, extensionality, h-levels |
| Friday | Cubical type theory: transp, hcomp, univalence |
Some familiarity with functional programming (Haskell, ML, or similar) is helpful. No prior experience with Agda or type theory is assumed.
Install Agda:
- Agda installation guide
- Recommended editor: VS Code with the agda-mode extension, or Emacs with agda2-mode
The course does not use the standard library. Friday's material on cubical type theory requires the Cubical Agda library.
The exercises use Agda's {! !} hole syntax — fill in the holes to complete the proofs.
Each day's exercises are in Exercises/. They build on material from the lectures, with holes ({! !}) marking what you need to prove.