Balanced Tensor Product of Module Categories (Moved from MSE)
Let $\mathcal{C}$ be a $k$-linear ($\operatorname{Vect}_k$-enriched) monoidal category and consider the 2-category $\operatorname{Mod}_\mathcal{C}$ of $k$-linear $(\mathcal{C}, \mathcal{C})$-bimodule categories in the sense of Ostrik (https://arxiv.org/abs/math/0111139). Roughly speaking, this construction can be thought of as a categorification of a module over a ring. Let $\otimes$ denote the tensor product of $k$-linear $(\mathcal{C}, \mathcal{C})$-bimodule categories (as defined in the work of Douglas, Schommer-Pries, and N. Snyder in https://arxiv.org/abs/1406.4204).
Does $\otimes$ endow $\operatorname{Mod}_\mathcal{C}$ with the structure of a monoidal 2-category?
 A: Yes, but I don't believe there is a paper on arXiv containing all details (I would love to be corrected!), and if I were refereeing a paper claiming it to be so, I would give the author a hard time. Edit: Per Matthew Titsworth's comment below, Gregor Schaumann's thesis contains these details. Original post:
The balanced tensor product is defined by universal property, and this makes everything work out.  Let $\mathcal M_n$ denote the bicategory whose objects are $n$-simplices with the following decorations: 


*

*On each edge (with endpoints $i<j$), put a $C$-$C$ bimodule $M_{ij}$.

*On each 2-dimensional face (with corners $i<j<k$) put a natural equivalence of bifunctors witnessing $M_{ik}$ as the balanced tensor $M_{ij} \otimes M_{jk}$.

*On each 3-dimensional face put a natural isomorphism of equivalences.

*On each 4-dimensional face put an equality of natural isomorphisms.


I say "the bicategory" but I will not try to write out precisely the 1- or 2-morphisms.  This is one of the things that if I were a referee I would demand.
Then the bicategories $\mathcal M_n$ together form a simplicial bicategory $\mathcal M_\bullet$.  (For degeneracies, put the standard identity bimodule and standard natural equivalences, etc.)  Moreover, $\mathcal M_1 = {_C\mathrm{Mod}_C}$ is the bicategory of $C$-$C$-bimodules and $\mathcal M_0 = \{*\}$ is the terminal bicategory.  The work of Douglas, Schommer-Pries, and Snyder implies that this simplicial bicategory satisfies the "Segal condition" that the bifunctor $\mathcal M_n \to (\mathcal M_1)^{\times n}$ remembering only the $n$ bimodules $M_{01},M_{12},M_{23},\dots, M_{(n-1)n}$ is an equivalence of bicategories.  So we have constructed a Segal bicategory, and if anything deserves the name "monoidal bicategory", that does.  One could then invoke strictification results to give ${_C\mathrm{Mod}_C}$ the structure of Gray monoidal bicategory if one so desired.
Remark: An alternate approach to giving ${_C\mathrm{Mod}_C}$ a monoidal structure, and indeed to defining the 3-category whose objects are $k$-linear monoidal and morphisms are bimodules, should be straightforward using my joint work with Scheimbauer.  One would need to compare carefully Ostrik's definitions (since you say "in the sense of Ostrik") with, probably, Haugseng's version of bimodules (or the version from Calaque and Scheimbauer, but I don't know of any paper that explains how to handle unpointed bimodules in their framework).  I think everyone expects Ostrik's and Haugseng's notions to match, and the requisite ideas to match them go back to the halcyon days of bicategories.  Haugseng's definition (as well as the version of Calaque and Scheimbauer) requires that $k$-linear categories (no monoidal anything) comprise a symmetric monoidal 2-category in the sense of $\Gamma$-categories.  Building this is no easier than what I outlined above, but not really harder either.  If you are willing to grant the existence of symmetric monoidal structure, then the main thing to check is that certain bicategories admit colimits of shape $\Delta$ ("geometric realizations"), and that tensor products distribute over colimits of shape $\Delta$.  (Probably (b) follows just from universal property considerations.)  I have been told that David Jordan and his collaborators have checked these types of properties for the bicategory $\mathrm{Rex}_k$ of small $k$-linear categories and right-exact functors, but I don't know a reference where details are written down.
