Suppose we have any category $\mathcal{C}$. Define the product closure $\mathcal{C}_p$ of $\mathcal{C}$ as the category-with-binary-products freely generated by the objects, morphisms, and equations of $\mathcal{C}$.
Basically, we form $\mathcal{C}_p$ by starting with $\mathcal{C}$, and adding an object named $A \times B$ for every pair of objects $A$ and $B$ (and doing that recursively), and then adding morphisms and equations asserting that the object named $A \times B$ really is a product object of $A$ and $B$.
(Note, by the way, that if $\mathcal{C}$ already has product objects, then they may cease to be product objects in $\mathcal{C}_p$.)
Intuitively, it seems more or less obvious that $\mathcal{C}$ is a full subcategory of $\mathcal{C}_p$, or, in other words, the inclusion functor $\mathcal{C} \to \mathcal{C}_p$ is full and faithful. Stated yet another way, if $A$ and $B$ are objects in $\mathcal{C}$, then $\mathcal{C}_p$ does not have any "extra" morphisms $A \to B$, nor has it taken any pair of distinct morphisms $A \to B$ and made them equal. (This fact is what I mean when I say that forming the product closure is "safe.")
However, how easy is it to prove this fact? So far, I've only managed to prove that the inclusion functor is full, not that it's faithful, and the proof was much more difficult than I was hoping. Here's the approach that I took:
- I started by noticing that if $A_1, \ldots, A_n, B_1, \ldots, B_p$ are objects in $\mathcal{C}$, then the hom-set $\mathrm{Hom}(A_1 \times \cdots \times A_n, B_1 \times \cdots \times B_p)$ seems to be the cartesian product of the hom-sets $\mathrm{Hom}(A_1 \times \cdots \times A_n, B_j)$ for each $j$, and each of these, in turn, seems to be the disjoint union of the hom-sets $\mathrm{Hom}(A_i, B_j)$ for each $i$.
- Knowing this, I defined a "normal form" for expressions for morphisms in $\mathcal{C}_p$, with the property that if $A$ and $B$ are objects in $\mathcal{C}$, then an expression for a morphism $A \to B$ in $\mathcal{C}_p$ is in normal form only if the expression consists merely of a morphism in $\mathcal{C}$.
- I then used several different kinds of proofs by induction to ultimately prove that every expression for a morphism in $\mathcal{C}_p$ can be reduced to an expression in normal form.
In order to prove that the inclusion functor is faithful, it seems like I'm going to have to prove that every expression reduces to normal form in only one way.
All of this business with defining normal forms, and then using induction to prove things about expressions, feels awfully tedious. Is there an easier way to prove that the inclusion functor is full and faithful, or is my approach pretty much the way to go?
Eventually, I'd like to learn whether or not, say, the topos freely generated by a category includes the original category as a full subcategory. If proving this fact for finite products really is as complex as it seems, then the idea of proving it for topoi seems rather horrifying.
Best Answer
This won't handle your topos problem, but completing and cocompleting under some class of limits or colimits is easy. One of the most fundamental theorems in category theory says that $\mathrm{Set}^{C^{\mathrm{op}}}$ is the free cocompletion of $C$ under all small colimits, if $C$ is small, with the canonical map given by Yoneda. (The smallness condition on $C$ can be gotten around if you need to.) Therefore, $\left(\mathrm{Set}^{C^{\mathrm{op}}}\right)^{\mathrm{op}}$ is the free completion of $C^{\mathrm{op}}$ under all small limits. You can show in any particular case you're interested in that the free completion of $C$ under some class of limits is the subcategory of $\left(\mathrm{Set}^C\right)^{\mathrm{op}}$ spanned by limits of representables from that class; in particular, the binary product completion is the full subcategory on the products of a positive finite number of representables in there.
Thus the binary product completion is the opposite of the subcategory of $\mathrm{Set}^C$ spanned by positive finite coproducts of representables, which you can easily check has the same description you've given. In particular, the only maps are those that have to be there once the product projections are given. This perspective gets you out of all those "normal form" issues since you have a well-specified candidate in hand.