Code for the Agda tutorial at TPHOLs 2009