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.
added to polynomial functor the evident but previously missing remark why it is called a “polynomial”, here.
I added some remarks to polynomial functor: “being polynomial” is a mere property of a (strong) functor once its domain and codomain are identified with slices of an ambient category, cartesian transformations between polynomial functors can be identified on the polynomial data, and the bicategory of polynomial functors enhances to a double category.
I made what I thought were similar remarks at the section on polynomial endofunctors at tree, in particular about a double category structure. Could you please have a look, Mike?
Yes, this is all in Gambino-Kock, right? I guess maybe they don’t explicitly write down a version of the double category that contains only cartesian cells.
I don’t remember seeing Gambino-Kock; I just took a guess based on what was in Kock’s article referenced in tree.
here’s the link; the double category is in section 3.
Added reference
It would be nice to mention some of the results in this paper in the body too, but I don’t have time.
Added pointer to
Added the example of how a “literal polynomial” endofunctor of a lextensive category really is a polynomial functor (here), with a sketch proof.
And included a little discussion of how this almost works for more general extensive categories, except one can really only talk about the composite , as the dependent product itself fails to exist in the absence of all pullbacks.
Also mentioned the version with a “literal power series” functor in the case that countable coproducts exist.
Actually, if we are happy to permit a partial right adjoint to pullback along the copairing map , namely only defined for those objects of (isomorphic to those) of the form , then a literal polynomial makes sense in any extensive category with finite products and can be seen as a polynomial endofunctor using the partially defined dependent product functor.
Added a reference
1 to 14 of 14