Given two categories $\mathcal{C}$ and $\mathcal{D}$, we can describe the following category $\mathcal{E}$. It is the initial category whose object set contains $\mathrm{Obj}(\mathcal{C}) \times \mathrm{Obj}(\mathcal{D})$ and which is equipped with

- A strict monoidal structure $\otimes : \mathcal{E} \times \mathcal{E} \to \mathcal{E}$
- For each $c \in \mathcal{C}$ a functor $F_c : \mathcal{D} \to \mathcal{E}$ with $F_c(d) = (c, d)$.
- For each $d \in \mathcal{D}$ a functor $G_d : \mathcal{C} \to \mathcal{E}$ with $G_d(c) = (c, d)$.

$\mathcal{E}$ can be explicitly constructed in the usual syntactic way, but it is a bit painstaking to describe and I think maybe obscures the idea anyway. On the other hand, if you haven't seen this kind of thing much before it's not immediately clear that the above category exists. Is there a better way to describe $\mathcal{E}$ to make it clearer that it exists, or is perhaps belief in the existence of such things an atomic mental widget?

It seems to me the clearest thing to say is the above definition followed by a few examples of morphisms, but I would be happy if there were an elegant way of easily describing the syntactic construction which yields $\mathcal{E}$.

shouldmean such things is that otherwise you will write down constructions that are not well-behaved under equivalences of categories. $\endgroup$ – Theo Johnson-Freyd Nov 11 '16 at 2:39shoulddo, but it's certainly good to at least be aware of when you violate equivalence-invariance. $\endgroup$ – Mike Shulman Nov 11 '16 at 22:39