Commit 2022-10-16 11:47 4698e35c

feat(category_theory/monoidal): define the bicategory of algebras and bimodules internal to some monoidal category (#14402) We generalise the well-known construction 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.