Bicategory of Monads and Bimodules

[tillrampe]

Given a bicategory, one can construct a new bicategory whose objects are monads and whose morphisms are so called bimodules. This is special case of Shulman, 'Framed Bicategories', Ch. 11 [https://arxiv.org/abs/0706.1286].

I've formalised this construction in the agda-categories library, and I'll make a pull request in the next couple of days.

[JacquesCarette]

Great, thanks! Looking forward to it.