Do pro-objects in a monoidal category have a completed tensor product?

Question

Given a monoidal category C it seems natural to define a completed tensor product in its category of pro objects Pro(C) by $$("lim_{a\in A}" X_a) \hat\otimes ("lim_{b\in B}" X_b)="lim_{(a,b)\in A\times B}" (X_a\otimes X_b)$$ but there seems to be nothing written down in this generality. Is there a catch?

Answer 1

For every class of weights $\Psi$ (or, more specifically, classes of shape for limits), the $\Psi$-completion of a monoidal category inherits the monoidal structure via (a restricted form of) Day convolution. For instance, this is Proposition 3.2 of Johnson's Monoidal Morita equivalence (note that Johnson considers the dual case, of free cocompletions). In your case, take $\Psi$ to be the class of cofiltered categories.