Bicategory of bimodules over internal monoids In a monoidal category $(C,\otimes)$ one can consider internal monoids and bimodules over these monoids (provided some additional requirements like existence of coequalizers hold). These monoids together with bimodules as 1-morphisms and bimodule morphisms as 2-morphisms should constitute a bicategory $\mathsf{Bimod}$.
Does anyone know a reference for this result? The only thing I could find so far is this page on nLab, but there is no proof given.
 A: This example of a bicategory (in the case of monoids in Ab, i.e. rings) appears already in Benabou's original Introduction to bicategories (example 2.5), although he does not provide the detailed proof you seem to be looking for.
In searching the 2-categorical literature, you may want to look for constructions of the larger bicategory of profunctors (a.k.a. distributors or bimodules) whose objects are enriched categories, the bicategory of monoids and bimodules being its full sub-bicategory on the one-object categories.  I believe the earliest references for this include Benabou's Les Distributeurs and Lawvere's Metric spaces, generalized logic, and closed categories, though on a quick glance I do not see a detailed proof in either of them either.
For actually checking axioms of this sort, it is often convenient to exhibit the operations as having a universal property.  In the case of bicategories, or more generally pseudo double categories (the bicategory Bimod enlarges to a pseudo double category whose additional morphisms are monoid homomorphisms), such a universal property can be expressed in terms of virtual double categories (a.k.a. fc-multicategories).  A construction of the virtual double category of monoids and bimodules can be found in section 5.3 of Leinster's Higher operads, higher categories, though he doesn't give a detailed proof of the conditions under which it is a pseudo double category.  A sketch of the latter --- but, again, with details left to the reader --- can be found in Appendix A of Cruttwell-Shulman, A unified framework for generalized multicategories.
