data-ex
Monad.agda
Proved two definition of monad is equivalent (assuming function extensionality).
lambda ex
DtEx.agda
Normalization by evaluation of dependent type.
Proved two definition of monad is equivalent (assuming function extensionality).
Normalization by evaluation of dependent type.