All this is closely related to the huge bulk of work surrounding polynomial functors, e.g., the category of polynomial endofunctors on $Set$ is equivalent to the free distributive category on one object. This might suggest pathways through the literature to get back to original sources.

I might have a crack at a direct proof myself. Not necessarily getting into the details of distributive laws on 2-monads (I imagine some Australian has already written out the connection between composite 2-monads and 2-distributive laws – something to look up), but just observing directly that for locally small $C$, letting $Prod(C) = Coprod(C^{op})^{op}$ be the small product completion, that the canonical inclusions $C \hookrightarrow Prod(C) \hookrightarrow Coprod(Prod(C))$ induce equivalences

$DistCat(Coprod(Prod(C)), D) \to ProdCat(Prod(C), D) \to Cat(C, D)$which is to say that $Coprod(Prod(C))$ is the free distributive category on $C$ [I believe Urs has already written out the proof of a claim whose corollary is that $Coprod(Prod(C))$ is in fact a distributive category].

]]>The statement sounds plausible and might not be hard to prove (though just stating/unwinding the definition of distributivity of 2-monads is a mouthful!) but if we have neither proof nor reference at the moment, then we must not state it as if we did.

So I have adjusted the wording accordingly (here). But if this motivates you to sit down and type out the proof into some nLab entry, I’d be more than happy to re-word again!

]]>Yes: there are a few more details that would need to be checked, but this statement suggests that the free product completion 2-monad lifts to the 2-category of algebras for the free coproduct cocompletion 2-monad, which is equivalent to having a distributive law. (The remaining details to check is that the multiplication and unit of the free product completion 2-monad also lift.)

]]>Let me see if I am following.

That corollary 5.9 seems to state that:

If A is cartesian, the free distributive completion is $\mathcal{S}//A^\ast$.

and you are claiming that this contains implicitly your statement that

the 2-monad for free product completion distributes over the 2-monad for free coproduct cocompletion

?

]]>I’m sure it must appear explicitly somewhere in the literature – I’ll try to have a look later – but it’s implicit in Corollary 5.9 of Cockett’s Introduction to distributive categories.

]]>Thanks!

Can we substantiate this remark (I gave it a numbered environment, here), by pointing to a proof?

]]>Mention the relation with distributive categories.

]]>added statement and dicussion (here) that the free coproduct completion of a category with products itself has products which distribute over the coproduct

]]>Just for completeness, I made explicit the proof of the first quoted proposition (here),

]]>added this to the list of References:

As categorical semantics for dependent linear type theories (in the context of quantum programming languages with “dynamic lifting”, such as proto-Quipper), the free coproduct completion of symmetric closed monoidal categories is considered in

- Francisco Rios, Peter Selinger, §3.2 in:
*A Categorical Model for a Quantum Circuit Description Language*, EPTCS**266**(2018) 164-178 [arXiv:1706.02630, doi:10.4204/EPTCS.266.11]

and its followups.

]]>

added pointer to:

- Michael Makkai, Robert Paré, §5.2.2 (pp. 116) in:
*Accessible categories: The foundations of categorical model theory*, Contemporary Mathematics**104**, American Mathematical Society, (1989) [ISBN:978-0-8218-7692-3]

and (here) their statement that the free coproduct completion of an accessible category is itself accessible

]]>added (here) mentioning of the example of the 1-category of skeletal groupoids as the free coproduct completion of that of groups (or their delooping groupoids).

]]>added (here) an example spelling out how the coproduct completion of a category that is already extensive to start with is equivalently that of bundles over sets in that category.

]]>added pointer to

- Jean Bénabou, §3 in:
*Fibered Categories and the Foundations of Naive Category Theory*, The Journal of Symbolic Logic, Vol.**50**1 (1985) 10-37 [doi:10.2307/2273784]

with a remark that this paragraph essentially describes the perspective as a Grothendieck-construction (without however using that or any related terminology).

]]>added a paragraph (here) making explicit that the free coproduct completion on $\mathcal{C}$ is also equivalently the Grothendieck construction $\int_{S \in Set} \, \underset{s \in S}{\prod} \mathcal{C}$.

]]>added (here) statement of Lemma 42 in:

- Aurelio Carboni, Enrico Vitale,
*Regular and exact completions*, Journal of Pure and Applied Algebra**125**1–3 (1998) 79-116 (doi:10.1016/S0022-4049(96)00115-6)

added (here) the example of $G Set$ as the free coproduct completion of $G Orbt$.

]]>some bare minimum on the free coproduct cocompletion.

The term used to redirect to the entry *free cartesian category*, where however the simple idea of free coproduct completion wasn’t really brought out.