Agda files for LMCS paper "What monads can and cannot do with a few extra pages"

These agda files accompany the paper "What monads can and cannot do with a few extra pages", by Rasmus Møgelberg and Maaike Zwart. In the agda files, claims about existing distributive laws and algebraic combinations of the delay monad with the reader, writer, state, and selection monad are proven.