Conor McBride - Dependently-Typed Metaprogramming 5/8: Induction-Recursion I
Channel: Ohad Kammar
Date: 27/08/2013

Lecture 5 of 8 in Conor McBride's "Dependently-Typed Metaprogramming (in Agda)" given at the Cambridge University Computer Laboratory during August 2013.

Course materials (lecture notes, exercises) are available at the course webpage: http://www.cl.cam.ac.uk/~ok259/agda-course-13/