mathlib3

4698e35c - feat(category_theory/monoidal): define the bicategory of algebras and bimodules internal to some monoidal category (#14402)

feat(category_theory/monoidal): define the bicategory of algebras and bimodules internal to some monoidal category (#14402) We generalise the [well-known construction](https://ncatlab.org/nlab/show/bimodule#AsMorphismsInA2Category) of the 2-category of rings, bimodules, and intertwiners. Given a monoidal category `C` that has coequalizers and in which left and right tensor products preserve colimits, we define a bicategory whose - objects are monoids in C; - 1-morphisms are bimodules; - 2-morphisms are bimodule homomorphisms. The composition of 1-morphisms is given by the tensor product of bimodules over the middle monoid. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>