Verified Functional Programming in Agda