Evaluation of typed terms in Agda using the Delay monad.