Monads need not be endofunctors is the original paper on the subject.
Relative monads formalised is the draft paper describing the formalisation in detail.
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.