If you’re interested in learning Agda, you might want to check out Conor McBride’s courses, given at the University of Cambridge: “Introduction to dependently

If you’re interested in learning Agda, you might want to check out Conor McBride’s courses, given at the University of Cambridge: “Introduction to dependently typed programming using Agda”, 2011: http://www.cl.cam.ac.uk/~ok259/agda-course/ http://www.cl.cam.ac.uk/~ok259/agda-course/ Course materials: https://github.com/mietek/agda-introduction https://github.com/mietek/agda-introduction “Dependently typed metaprogramming (in Agda)”, 2013: http://www.cl.cam.ac.uk/~ok259/agda-course-13/ http://www.cl.cam.ac.uk/~ok259/agda-course-13/ Course materials: https://github.com/pigworker/MetaprogAgda https://github.com/pigworker/MetaprogAgda