Another repository with Agda samples can be found at
In the folders:
protocols/
Verification of some communication protocols in Isabelle, Coq and Agda.
cpdt
Some stuff from
- Certified Programming with Dependent Types
by Adam Chlipala
puzzles
Logic Puzzles by John P. Pratt
(now just a single one).
sf
Some stuff from
- Software Foundations
by Benjamin C. Pierce, ...