Added a really interesting example.
Added a simple denotational haskell implementation..
Moved agda denotational stuff.