Ok, so this is very interesting, I see others think so too, as they upvote it, but could someone offer an explanation of what exactly is going on here? I would love to have a little glossary of Agda syntax and concepts to go with this post; as it is now it's completely undecipherable for me, unfortunately :(
(these are just cribbed from the agda wikipedia page but..) check these out: