These are some working notes to Programming and Proving in Agda by Jesper Cockx.
The notes are quite rough for now — reviewing these and writing them up (probably in pretty LaTeX) will be the next step.
Spoiler alert these notes contain solutions to the exercises.
Quality alert the solutions have not yet been reviewed...
...by a human, at least. Agda has typechecked them and pleasantly coloured in the code. Therefore, the proofs can be considered valid. Which is rather neat when you think about it.