Is there a known description of the **free category with both product and coproduct?**

That is, given a small category $C$, I want to consider a category $U C$ which has product and coproduct, a functor $C \to U C$ and such that $UC$ is universal for functor preserving both product and coproduct. The case $C = \emptyset$ is already interesting.

I'm also happy to focus on *finite* product and *finite* coproduct, especially if it avoids some size problems, though I don't think this is essential.

My guess is that this category should be a category of two-player games (player and opponent) with morphisms being simulation and where outcome of the game are marked by objects of $C$ (if $C = \emptyset$ we should just have a win/lose outcome):

The coproduct of a family of games is the game where the player first chooses which game he wants to play in the family, while their product is the game where the opponent chooses which game he wants to play. The initial object is the game where player loses at the start, and the final object is the one where opponent loses at the start.

But the details of this, and especially the proper definition of the morphisms are a bit involved, so I'm curious whether this has been worked out somewhere.

Of course, as soon as we assume compatibility between product and coproduct (for e.g. distributivity) there are simple description, but here I'm interested in the completely unconstrained situation.

Free bicomplete categoriesandFree bicompletion of enriched categoriesof Joyal, though I couldn't find these online. Hu–Joyal's Coherence Completions of Categories and Their Enriched Softness describes the free completion under products, coproducts and a zero object. $\endgroup$nonemptyfinite products and coproducts on discrete categories, where they state that (at point of publication) a categorical formulation of the result for non-discrete categories and empty products/coproducts was an open question. $\endgroup$