Agda Lecture Notes

Anton Setzer offers good course documents on interactive theorem proving with Agda:
http://www.cs.swan.ac.uk/~csetzer/lectures/intertheo/