- Lecture 1: Administrivia and getting started with Agda (20 Sep)
- Lecture 2: Making use of precise types (22 Sep)
- Lecture 3: Logic in type theory (27 Sep)
- Lecture 4: Predicates, and basic equality (29 Sep)
- Lecture 5: Classical logic, and forall and exists (4 Oct)
- Lecture 6: More about equality (6 Oct)
- Lecture 7: Inductively defined relations (11 oct)
- Lecture 8: Discussion of Coursework 1 [no recording] (13 Oct)
- Lecture 9: Hutton's Razor (18 Oct)
- Lecture 10: Relating typed and untyped expressions, and proving optimisations correct (20 Oct)
- Lecture 11: Definition and examples of categories (25 Oct)
- Lecture 12: Functors (27 Oct)
- Lecture 13: The category of categories, and natural transformations (1 Nov)
- Lecture 14: Monads (3 Nov)
- Lecture 15: Kleisli categories (8 Nov)
- Lecture 16: Adjunctions (10 Nov)
- Lecture 17: Free categories (15 Nov)
- Lecture 18: The free-forgetful adjunction for categories, and monads from adjunctions (17 Nov)
- Lecture 19: Every monad arises from an adjunction (22 Nov)
- Lecture 20: Cancelled due to deteriorating pension and working conditions in UK higher education (24 Nov)
- Coursework.One due Monday 10 October (beginning of Week 4)
- Coursework.Two due Monday 31 October (beginning of Week 7)
- Coursework.Three due Monday 5 October (beginning of Week 12)