1-Category of Bimodules

[tillrampe]

This pull request constructs a 1-category of bimodules and bimodule homomorphism given two monads in a bicategory (cf. Shulman - Framed Bicategories and Monoidal Fibrations, Ch. 11). This is part of a larger project constructing a bicategory of monads and bimodules.

[JacquesCarette]

Build failed - problem with moving things around?

[tillrampe]

Yes, I've found the problem and with it a couple more things to improve. I will push the commits all together when they are ready for review.

[tillrampe]

The main purpose of this file is to show that a bimodule homomorphism is invertible if its underlying 2-cell is invertible. As this requires considering two different categories plus the ambient bicategory, there is a big potential for overloaded variable names. I'm employing using commands to avoid overloads, but don't rename. If you see a better way to strike a balance between being clear and being concise please let me know.

[JacquesCarette]

I tend to use named private modules, with the same name as the (bi)category of interest, to give the reader more 'local context' to help resolve which (bi)category is being talked about.

I tend to them use non-subscripted names when I do that, as that makes things harder to read.

[tillrampe]

I prefer mixfix notation for _≅_ and _⇒_, and that is not possible unless you open the modules.

[JacquesCarette]

C.⇒ works just fine infix BTW.

[tillrampe]

This looks like it can be eta-reduced to hom.Equiv but in fact it cannot. The issue is that how.Equiv is a proof that hom._≈_ is an equivalence, but we need a proof that λ h₁ h₂ → α h₁ ≈ α h₂ is an equivalence.

[JacquesCarette]

A one liner comment (like "must be delta expanded to typecheck as at different types") would be good.

[JacquesCarette]

As the last thing discussed was quite cosmetic (in a way that is not covered by the library's style guide), I'm not going to hold up this PR because of that.