Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
added (here) statement of Lemma 42 in:
added pointer to
with a remark that this paragraph essentially describes the perspective as a Grothendieck-construction (without however using that or any related terminology).
added pointer to:
and (here) their statement that the free coproduct completion of an accessible category is itself accessible
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
and its followups.
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.
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
?
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.)
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!
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].
1 to 20 of 20