Papers
Monads need not be endofunctors (Journal version).
Monads need not be endofunctors (Conference version).
Relative monads formalised (Formalisation paper).
GitHub repository of Agda formalisations
This supercedes all the code below which was written using older versions of Agda and won't work in current versions of Agda.
The below formalisations were made using the current unstable development version (2.2.7) of Agda. The current stable version (2.2.6) will run out of memory trying to type check them.
Agda formalisation with type in type. See the enclosed file Everything.agda for an explanation of what's included.
Agda formalisation with universe polymorphism. Again, see Everything.agda.