There's a small amount of documentation (a "reference card" and some other things on Anton's page at: http://www.cs.swan.ac.uk/~csetzer/lectures/intertheo/04/). Maybe Anton has some other material, or valuable experience of teaching using agda. Peter