Consider the diagonal functor $\Delta_\mathcal{J} : \mathrm{Set} \to \mathrm{Set}^\mathcal{J}$, given by $\Delta_{\mathcal{J}}(X) = J \mapsto X$. This has left and right adjoints, which in the case that $\mathcal{J}$ is discrete we may call $\Sigma_{\mathcal J} \dashv \Delta_{\mathcal J} \dashv \Pi_{\mathcal J}$; these represent "$\mathcal J$-indexed coproduct" and "$\mathcal J$-indexed product" of sets, respectively. For example, $\Sigma_{\mathcal J} F = \coprod_{j \in \mathcal J} F(j)$.

Now consider the groupoid $\mathbb{B}$ of finite sets and bijections. Unlike $\mathrm{Set}$, $\mathbb{B}$ has no products or coproducts (any category with all products or coproducts is necessarily connected). However, it is monoidal in (at least) two ways, given by disjoint union and Cartesian product of finite sets. For discrete $\mathcal J$ with a finite set of objects, we can construct an analogue to $\Sigma_{\mathcal J}$ in $\mathbb{B}$, namely, $\Sigma^{\mathbb{B}}_{\mathcal J} : \mathbb{B}^{\mathcal J} \to \mathbb{B}$, which intuitively "acts just like $\Sigma_{\mathcal J}$"; this works because disjoint union is functorial in $\mathbb B$ and preserves finiteness. However, I am not sure how to formally relate $\Sigma_{\mathcal J}$ and $\Sigma^{\mathbb{B}}_{\mathcal J}$. Since $\mathbb B$ does not have coproducts, $\Sigma^{\mathbb B}_{\mathcal J}$ does not arise as a left adjoint to $\Delta_{\mathcal J}$. We can define a functor $\Sigma_{\mathcal J}(U \circ -) : \mathbb B^{\mathcal J} \to \mathrm{Set}$ (where $U : \mathbb B \to \mathrm{Set}$ is the forgetful functor), but extending this to a functor $\mathbb B^{\mathcal J} \to \mathbb B$ seems problematic since there are no interesting functors $\mathrm{Set} \to \mathbb B$; intuitively, $\Sigma_{\mathcal J}(U \circ -)$ "forgets" too much.

Is there a "nice" way to construct $\Sigma^{\mathbb B}_{\mathcal J}$? My real goal is to generalize this to other categories besides $\mathbb B$; so, more generally, what properties does a monoidal category $(\mathcal{C},\oplus,0)$ need to have in order to be able to define some sort of "indexed monoidal product" $\bigoplus_{\mathcal J} : \mathcal C^{\mathcal J} \to \mathcal C$?

J, then use this to take theJ-iterated monoidal product" approach, because you're working in a constructive setting. However, what definition of "finite" are you using forJ? In such settings there are several options for this? If you assume thatJiscardinal-finite, then you can use the indexed-monoidal-product approach without difficulty. In fact, I may expand this into an answer. – Peter LeFanu Lumsdaine Apr 29 at 21:50