Bicategory of Monads and Bimodules

[tillrampe]

This PR contains

• some lemmas and definitions concerning coequalizers
• definition of bicategory with local coequalizers (this is the premise for the construction of the bicategory of monads and bimodules)
• definition of bimodule between monads
• given two monads, construction of 1-category of bimodules
• construction of bicategory of monads and bimodules

[JacquesCarette]

Note that I would have preferred this in 3-4 PRs rather than one big one. I won't ask that you split this one up, but please try to make smaller ones in the future.

[tillrampe]

I can still split it up. Wouldn't take long.

[JacquesCarette]

If you're going to split, then definitely the improvements to the current library should come in their own PR. You can choose how you want to 'incrementalize' the rest.

[tillrampe]

Thanks for the feedback. What I will do is the following. I'll split up the pull request into

• coequalizer (improvements on the existing library)
• local coequalizers (improvements on the existing library)
• bimodules (new feature)
• 1-category of bimodules (new feature)
• bicategory of monads and bimodules (new feature). I'll incorporate your first round of comments before making the pull requests and wait for the approval of the previous pull request before making the next one. I hope that sounds good to you.

[JacquesCarette]

Sounds perfect. And feel free to discuss some of my suggestions, when you feel that your names have distinct advantages that I might have missed.

[TOTBWF]

If you merge master into this PR, then CI should start working :)