Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: polynomial functors

Jules Hedges (May 07 2020 at 14:09):

I want to draw attention and start a discussion thread on @David Spivak's new preprint https://arxiv.org/abs/2005.01894 on the category of polynomial functors

Jules Hedges (May 07 2020 at 14:11):

I suspect this category might be very folkloric, I wonder if anyone's seen it in anything old? (There's a cluster of literature beginning with https://www.cs.nott.ac.uk/~psztxa/publ/fossacs03.pdf and Michael Abbott's thesis, which I already told David about, which studies this category)

Jules Hedges (May 07 2020 at 14:12):

Bob Atkey also wrote me this: "There's even more structure in Poly! Tamara von Glehn's thesis shows that it is a model of dependent types with an equality type that refutes functional extensionality. Also, there's an interesting skew-monoidal product related to selective functors."

Jules Hedges (May 07 2020 at 14:16):

David told me about this category over a year ago, and explained it as "it's like locally ringed spaces, except you replace local rings with sets and also replace topological spaces with sets". So for a while we called it "setted sets". So I wonder if it already appears in Grothendieck or something equally old and in French?

Jules Hedges (May 07 2020 at 14:17):

(Since it looks like I'm just bashing it, I should add that I'm extremely excited about this paper)

Exequiel Rivas (May 07 2020 at 14:25):

@Joachim Kock 's notes on polynomial functors has a section of historical remarks, and probably knows much more about the history of this category.

Jules Hedges (May 07 2020 at 14:34):

http://mat.uab.es/~kock/cat/polynomial.pdf (long pdf!)

Nathanael Arkor (May 07 2020 at 14:58):

Part of the difficulty with finding references to properties of polynomial functors is that they're spread across both category theory (as "polynomial functors") and computer science (as "indexed containers").

Nathanael Arkor (May 07 2020 at 15:04):

Another thing to be aware of is that sometimes results are stated just for polynomials in $\mathbf{Set}$, like in @David Spivak's new preprint, and some for arbitrary categories with pullbacks. Some of the properties stated in the preprint are not true for the category of polynomials in an arbitrary category.

(=_=) (May 07 2020 at 16:28):

This $\textrm{Poly}$ is the same one in $\textrm{\S}$ 2.5 of Kock's notes, I take it?

(=_=) (May 07 2020 at 16:51):

Nathanael Arkor said:

Part of the difficulty with finding references to properties of polynomial functors is that they're spread across both category theory (as "polynomial functors") and computer science (as "indexed containers").

Over on the category-theoretic side, there are some interesting applications of polynomial functors (and monads) to topology. It'd be interesting to see how they can be interpreted through this lens (pun somewhat intended).

Nathanael Arkor (May 07 2020 at 16:55):

Rongmin Lu said:

This $\textrm{Poly}$ is the same one in $\textrm{\S}$ 2.5 of Kock's notes, I take it?

I believe it's the category $\mathbf{Set}[X]$ defined in §2.1 of the notes. $\mathbf{Poly}$ of Kock's notes restricts to cartesian natural transformations.

(=_=) (May 07 2020 at 17:01):

Nathanael Arkor said:

Rongmin Lu said:

This $\textrm{Poly}$ is the same one in $\textrm{\S}$ 2.5 of Kock's notes, I take it?

I believe it's the category $\mathbf{Set}[X]$ defined in §2.1 of the notes. $\mathbf{Poly}$ of Kock's notes restricts to cartesian natural transformations.

Thank you. I think restricting to Cartesian natural transformations can be useful. In the case of lenses, which can be viewed as an optic associated to a special case of polynomial functors, I think this gives you lawful lenses. (I haven't verified this, this is something I've heard in a seminar somewhere.)

Jules Hedges (May 07 2020 at 17:12):

Woah, that would be really amazing if that's true

Jules Hedges (May 07 2020 at 17:13):

I'm not sure the claim typechecks though, it doesn't make sense to talk about lawful lenses between arbitrary objects of the category

(=_=) (May 07 2020 at 17:13):

This was from a seminar at Macquarie by Mike Johnson pre-Covid. I have notes somewhere that I need to dig up.

(=_=) (May 07 2020 at 17:18):

In the context of data manipulation, lawfulness is desirable for safety purposes. Even there, however, there are also instances where you want lenses to be less lawful.

(=_=) (May 07 2020 at 17:21):

Anyway, all I'm trying to say is that Cartesian natural transformations came up in the discussion of lawfulness during Mike's seminar. It's 3 in the morning here and I'll look at this in more detail later.

Jules Hedges (May 07 2020 at 18:29):

Rongmin Lu said:

It's definitely more restrictive, but I'm not sure what you mean by "arbitrary objects of the category" and why it doesn't "typecheck".

Not totally sure, I was kinda thinking out loud, but in the case of the category I call "bimorphic lenses" (which is apparently equivalent to the full subcategory of monomials) has objects of the form $(a, b)$ (corresponding to the monomial $ax^b$), but you can only write the definition of lawful lenses for lenses of the form $(a, a) \to (c, c)$

(=_=) (May 07 2020 at 18:42):

Right. And since I can't sleep without correcting my mistake...

I think in Kock's notes, it's stated in $\textrm{\S}$ 2.1 that "every natural transformation between polynomial functors factors as a representable one followed by a cartesian." In the case of lenses, the Cartesian thing is the put. Often, though, you want to relax the Cartesian assumption. That got garbled into the "amazing" thing that's surely not true.

Jules Hedges (May 07 2020 at 18:45):

Still very much shooting from the hip here, but it sounds like how every lens $(a,b) \to (c,d)$ factors in the form $(a,b) \to (c,b) \to (c,d)$ which comes from the fact that lenses are fibred over sets, so that's a vertical and a cartesian morphism. I'm not sure it's the same sense of "cartesian" or not!

(=_=) (May 08 2020 at 08:17):

The sense in which Kock means "Cartesian morphisms" (actually, "Cartesian natural transformations") is defined in between Lemma 2.1.5 and Remark 2.1.6. It looks like the same definition as the one in the nLab.

(=_=) (May 10 2020 at 00:23):

Somewhat off-topic, but re. your musings on quantum machine learning, this is actually an emerging research area.

Was daydreaming and it suddenly hit me that "quantum machine learning" actually makes total sense and isn't (just) buzzword soup. Machine learning is at least half linear algebra, and linear algebra is home territory for quantum computation

- julesh (@_julesh_)

Joachim Kock (May 11 2020 at 23:12):

It is indeed not so easy to trace the origin of the theory of polynomial functors. Joyal had them in the 1980s in connection with his discovery of combinatorial species and analytic functors, but did not really develop the theory because it is not rich enough to cover species and operads. Joyal himself claims that the notion should be attributed to Grothendieck :-) (I don't know exactly what this means...)

At the CT2010 in Genova, Peter Johnstone helped me draw a very interesting map of precursors to the notion of polynomial functors. I remember there were dozens of them, but unfortunately I don't have the map anymore :-( There are polynomial functors already in Arbib and Manes, but they did not see the pleasant representation of them in terms of maps E -> B.

For me the really cool feature of polynomial functors is their representability feature --- how they can be manipulated in terms of E -> B. The first printed evidence of this viewpoint that I am aware of is [Bisson-Joyal (1995): The Dyer-Lashof algebra in bordism (extended abstract), 1995]. That's some very grown-up algebraic topology they are up to, and their E -> B is really a covering space! They don't have time to talk much about polynomial functors, though. In logic, I believe the first explicit appearance is [Moerdijk-Palmgren (2000): Wellfounded trees in categories], where they show that Martin-Löf's W-types are initial algebras for polynomial endofunctors. The really nice many-variable formalism I believe was introduced by [Gambino-Hyland (2003): Wellfounded Trees and Dependent Polynomial Functors]. It is very curious though, that this shape of diagram,
I <- E -> B -> J was studied by Tambara already in 1993 --- yes! it is the same Tambara as in Tambara modules! Tambara essentially proved (without noticing it) that finite polynomial functors are the Lawvere theory theory for commutative semirings. See [Gambino-Kock (2013): Polynomial functors and polynomial monads] for this result.

Generally in [GK] we made a big effort to collect history and to unify the various developments, and in particular to bring all the container stuff into more mathematical language. I recommend that paper as a basic reference :-)

John Baez (May 11 2020 at 23:13):

Joachim wrote:

The first printed evidence of this viewpoint that I am aware of is [Bisson-Joyal (1995): The Dyer-Lashof algebra in bordism (extended abstract), 1995]. That's some very grown-up algebraic topology they are up to [...]

John Baez (May 11 2020 at 23:13):

Yeah, sounds like it! I hope I understand that stuff when I grow up!

Joachim Kock (May 11 2020 at 23:17):

Another big source of confusion is that there is something else which is also called polynomial functor: they are endofunctors F: Vect -> Vect such that for every pair of vector spaces the the map on hom spaces is given by polynomials. Such functors come up in representation theory, for example in connection with Schur functors. The appeared in Macdonalds book Symmetric Functions and Hall Polynomials, but in fact they were first studied in the 1950s (or even 1940s?) by Eilenberg and Mac Lane in connection with group cohomology. It's a very active area of research in representation theory and algebraic topology, for example in connection with functor cohomology.

The two theories of polynomial functors --- the one in cartesian contexts (such as logic and geometry), and the one in linear contexts -- do not seem to have so much in common at this point. For example, there are no representability features in the linear case. Adamek and Velebil show that the only pullback-preserving endofunctors of Vect are 'tensoring with a fixed vector space'.

Joachim Kock (May 11 2020 at 23:42):

Regarding my Notes on polynomial functors I should apologise for them being so messy and unprocessed.

I learned about polynomial functors when I was a postdoc with André Joyal in 2003-2004. We used polynomial functors to give a combinatorial version of the Baez-Dolan construction, and they have been a central topic in my research ever since.

Since there was not much literature available, I started to write notes at that time. By 2009, when the manuscript had over 400 pages, a huge mess (and containing mistakes), I put it on hold (that's its present state), because I realised I needed to upgrade everything from sets to groupoids, in order to cover the applications I had in mind in combinatorics and operad theory. Since then I have been learning about groupoids (and infinity-groupoids).

Groupoids really make a huge difference. With David Gepner and Rune Haugseng we showed that polynomial functors over groupoids are expressive enough to cover species, analytic functors, and operads. In fact with polynomial monads over infinity-groupoids we give a neat model for infinity-operads.

I think I am now in a position where I could go back to the manuscript and finish it -- with groupoids. But meanwhile, as you all know: each research project creates a number of new research projects, so it is not clear when I will actually come around to this.

However, the remarkable recent work of David Spivak and his collaborators is very motivating, and it is enjoyable to see how powerful the polynomial-functor toolbox is even in the case of one-variable polynomial functors over Set! Congratulations, David!

(Sorry for telling about myself. Maybe I should move this post to the present-yourself section.)

Nathanael Arkor (May 11 2020 at 23:49):

@Joachim Kock: one thing I was always curious about was how generalised species had an entire chapter dedicated to them in the table of contents for the notes (though sadly the chapter appears unwritten). Is this still a topic you would reserve a chapter for in the eventual updated book?

Joachim Kock (May 12 2020 at 00:01):

Jules Hedges said:

Still very much shooting from the hip here, but it sounds like how every lens $(a,b) \to (c,d)$ factors in the form $(a,b) \to (c,b) \to (c,d)$ which comes from the fact that lenses are fibred over sets, so that's a vertical and a cartesian morphism. I'm not sure it's the same sense of "cartesian" or not!

Yes, that's right, it's the same.

(=_=) (May 12 2020 at 00:04):

Joachim Kock said:

The two theories of polynomial functors --- the one in cartesian contexts (such as logic and geometry), and the one in linear contexts -- do not seem to have so much in common at this point.

I'm probably asking for too much, but I've always wondered how Goodwillie calculus can be related to these.

Joachim Kock (May 12 2020 at 00:20):

Nathanael Arkor said:

Joachim Kock: one thing I was always curious about was how generalised species had an entire chapter dedicated to them in the table of contents for the notes (though sadly the chapter appears unwritten). Is this still a topic you would reserve a chapter for in the eventual updated book?

I don't know if I would get around to this. The generalised species stuff (Fiore-Gambino-Hyland-Winskel) is really a different brand of polynomial functors (as you surely know) than the slice-category brand I mostly work with. The generalised-species stuff is about categories instead of groupoids -- very scary! It is closely related (is equal to?) the familial functors that Todd talked about in another thread, studied deeply by Mark Weber. And which Spivak uses for data migration. I would love to know more about that, but maybe it is not my highest priority right now -- and in any case my priorities tend to get overridden...

Joachim Kock (May 12 2020 at 00:21):

Rongmin Lu said:

I'm probably asking for too much, but I've always wondered how Goodwillie calculus can be related to these.

I think the Goodwillie calculus is more closely related to the Vect-based notion of polynomial functor that I mentioned a few posts back.

sarahzrf (Feb 13 2025 at 07:29):

not sure if i should necropost this here or start a new thread but i have been trying to think about polynomial functors of this kind and i am a bit stuck

sarahzrf (Feb 13 2025 at 07:30):

in particular: if $p$ is some polynomial functor, i understand that i can recover the set of "positions" of $p$ by just evaluating $p(1)$ or equivalently by taking $\operatorname{Hom}(y^1, p)$, but given a position $i : y^1 \to p$, how do i get the set of directions $p_i$?

sarahzrf (Feb 13 2025 at 07:33):

the paper linked at the beginning of the thread seems to just take for granted that you can do so, in a way that only makes sense to me if either a) a polynomial functor is defined as a kind of "presentation" rather than a functor $\mathrm{Set} \to \mathrm{Set}$ with a given property, or b) we use choice to fix once and for all a pseudoinverse to the functor from such presentations to polynomial functors

sarahzrf (Feb 13 2025 at 07:34):

or to turn it around: my question essentially is: is there a nice, choiceless construction for defining such a pseudoinverse?

sarahzrf (Feb 13 2025 at 17:01):

uh, maybe "pseudoinverse" is a term i invented in my head, sorry—i just meant the other direction of the equivalence. "homotopy inverse"?

John Baez (Feb 13 2025 at 17:24):

@Todd Trimble has written "pseudo-inverse" in a paper of ours, expecting me to understand it, and I did. So I think it's fine. Personally I'd tend to say "weak inverse", or "homotopy inverse" if I were trying to evoke sensations of homotopy theory.

Todd Trimble (Feb 13 2025 at 17:31):

I think I've seen other people use the term "quasi-inverse", but I used pseudo-inverse because of the use of the word "pseudo" elsewhere to suggest "up to isomorphism", as opposed to "strict" or on-the-nose.

John Baez (Feb 13 2025 at 17:32):

Indeed I like "pseudo-" here better than "quasi-", for exactly that reason: we also have pseudofunctors, pseudonatural transformations, pseudomonads, etc., so you can stick "pseudo" in front of almost anything and I'll get it.

Kevin Carlson (Feb 13 2025 at 18:21):

This is a very good question. First, how do you recover the set of directions of a monomial $m=y^A$? Well, the monomials are the image of $\mathbf{Set}^{\mathrm{op}}$ under Yoneda, which is fully faithful, so in a non-constructive sense we know that non-isomorphic sets give non-isomorphic monomials. Can't we just evaluate on some nice set to actually get $A$ out? Well...no, not really. The smallest set that would make sense is $2,$ and in fact it's consistent with ZFC that $2^A$ could be isomorphic to $2^B$ without $A$ being isomorphic to $B$ (this doesn't quite contradict Cantor's theorem, though they sound similar.) Of course this is an infinities problem, and if you're only looking at finitary polynomials, you can readily recover $A$ as $\log_2|m(2)|.$

Kevin Carlson (Feb 13 2025 at 18:23):

For general polynomials, you can somewhat analogously prove that the only way they could be isomorphic is if there's a bijection between the positions inducing bijections at all the corresponding directions. This is an example of the behavior of free coproduct completions, in general: in free coproduct completions, the "presentation" you ask about is unique up to permutation of the coproduct indices. But all the moreso, there's no simple way to compute the directions just by plugging in, if you're handed a polynomial you only know how to evaluate.

sarahzrf (Feb 13 2025 at 18:36):

right, i figured this much out and wondered if i was missing something clever, like if evaluating some sort of limit or colimit can recover the directions

sarahzrf (Feb 13 2025 at 18:37):

actually, i would note that even for the finitary case we still have a problem—your $\log_2$ is a decategorification of what i actually want, and by performing that decategorification you lose information

sarahzrf (Feb 13 2025 at 18:41):

like, if you take the subcategory of $[\mathrm{FinSet}, \mathrm{Set}]$ of functors that can be written as coproducts of representables, i don't think the $\log_2$ construction actually defines the pseudo-inverse i was talking about

sarahzrf (Feb 13 2025 at 18:45):

Let's be a bit more precise: Say $\mathrm{PolyF}$ is defined to be the subcategory of $[\mathrm{Set}, \mathrm{Set}]$ on those functors for which there merely exists some way to write them as a coproduct of representables, $\mathrm{PolyB}$ is defined to be the category whose objects are maps of sets understood as bundles and whose morphisms are $(f, f^\#)$ pairs.

sarahzrf (Feb 13 2025 at 18:47):

define also $\mathrm{PolyF}_\mathrm{fin}$ to be the subcategory of $[\mathrm{FinSet}, \mathrm{Set}]$ on coproducts of reps and $\mathrm{PolyB}_\mathrm{fin}$ to be the subcategory of $\mathrm{PolyB}$ on finite-fibered bundles

sarahzrf (Feb 13 2025 at 18:47):

then there are evident functors $\mathrm{PolyB} \to \mathrm{PolyF}$ and $\mathrm{PolyB}_\mathrm{fin} \to \mathrm{PolyF}_\mathrm{fin}$ that are easy to write down explicit formulae for

sarahzrf (Feb 13 2025 at 18:48):

we can show that these functors are ff and eso so choice says we have pseudo-inverses, but i want explicit formulae for those pseudo-inverses

sarahzrf (Feb 13 2025 at 18:49):

the $\log_2$ construction defines an object mapping $\mathrm{PolyF}_\mathrm{fin} \to \mathrm{PolyB}_\mathrm{fin}$ but since you decategorify in the process i'm super skeptical that you can easily make it an actual functor

sarahzrf (Feb 13 2025 at 18:51):

if there were a way to recover the order structure on the subsets then it would be easy, but I don't see any clear way of doing that

sarahzrf (Feb 13 2025 at 20:13):

um. hm. actually i think in a HoTT setting these categories are all univalent so the HoTT proof that constructs a pseudoinverse from ff+eso w/o using choice might apply here...

sarahzrf (Feb 13 2025 at 20:14):

i don't know how that proof goes though :sweat_smile: i'm looking at the hott book rn to see if i can parse anything out

sarahzrf (Feb 13 2025 at 20:19):

oh right this doesn't give you a formula the way i want it just tells you that it's licit to talk about the stuff hidden inside the "merely exists". that's sort of unsatisfying though... i guess in my gut i want a construction that only uses the interface of "a functor $\mathrm{Set} \to \mathrm{Set}$" and which happens to give the right result in the case that the input is actually polynomial

Kevin Carlson (Feb 13 2025 at 21:05):

Well, once you have the object mapping of the pseudo-inverse of a functor, the functoriality is uniquely defined since the hom mappings are bijections.

sarahzrf (Feb 13 2025 at 23:12):

hmmmmm

sarahzrf (Feb 13 2025 at 23:15):

i think you actually also need one of the natural isomorphisms witnessing the fact that it's a pseudoinverse unless your object mapping is an inverse on the nose?

sarahzrf (Feb 13 2025 at 23:22):

say we have $F : \mathrm{C} \to \mathrm{D}$ ff and eso and we define an object mapping $G : \mathrm{D} \to \mathrm{C}$. say $A, B \in \mathrm{D}$; then you're saying to invert some map $\operatorname{Hom}(GA, GB) \to \operatorname{Hom}(A, B)$. but to get my hands on such an invertible map, i either need to

• know that $A, B$ are in the image on-the-nose of $F$ and substitute
• have isomorphisms $FGA \cong A$ and $FGB \cong B$

sarahzrf (Feb 13 2025 at 23:36):

This does rephrase the problem to "show a natural isomorphism of $F : \mathrm{FinSet} \to \mathrm{Set}$ with $X \mapsto \sum_{p : y1 \to F} X^{\log_2 |\{s : y2 \to F \mid s \circ ! = p\}|}$"

Spencer Breiner (Feb 13 2025 at 23:52):

Another possibility is to use the derivative. I believe $p'(1)$ is the set of all directions.

sarahzrf (Feb 14 2025 at 00:03):

i'm not sure what kind of derivative you mean

sarahzrf (Feb 14 2025 at 00:03):

that said, i want to get the set of directions at a given position, not just the set of all directions

Kevin Carlson (Feb 14 2025 at 00:38):

sarahzrf said:

This does rephrase the problem to "show a natural isomorphism of $F : \mathrm{FinSet} \to \mathrm{Set}$ with $X \mapsto \sum_{p : y1 \to F} X^{\log_2 |\{s : y2 \to F \mid s \circ ! = p\}|}$"

I'm having trouble seeing how your question doesn't reduce to "show a natural isomorphism of $y^A$ to $y^B$ when $A,B$ are sets of the same cardinality."

Spencer Breiner (Feb 14 2025 at 01:17):

Just the ordinary derivative of a polynomial. There is a canonical map from the base of $p'$ into the base of $p$ that will allow you to recover the fibers.

sarahzrf (Feb 14 2025 at 01:38):

Kevin Carlson said:

sarahzrf said:

This does rephrase the problem to "show a natural isomorphism of $F : \mathrm{FinSet} \to \mathrm{Set}$ with $X \mapsto \sum_{p : y1 \to F} X^{\log_2 |\{s : y2 \to F \mid s \circ ! = p\}|}$"

I'm having trouble seeing how your question doesn't reduce to "show a natural isomorphism of $y^A$ to $y^B$ when $A,B$ are sets of the same cardinality."

sorry, clarification: i mean an isomorphism natural in $F$ actually, wait, the rhs isn't a functor in $F$ so now I'm not sure what I'm asking for—I guess I mean "an explicit, general formula that gives an isomorphism for each $F$ without invoking choice". so in that sense, it is essentially similar to what you wrote indeed—there is no nice general formula giving an isomorphism $y^A \cong y^B$ as a function of finite sets $A, B$ of the same cardinality! you have to invoke some kind of choice

sarahzrf (Feb 14 2025 at 01:40):

Spencer Breiner said:

Just the ordinary derivative of a polynomial. There is a canonical map from the base of $p'$ into the base of $p$ that will allow you to recover the fibers.

okay, but if I have the data of a functor and not a polynomial, how do I do this?

Kevin Carlson (Feb 14 2025 at 01:53):

To narrow in on a claim that's at least quite clear although it may be off target of your exact question, I do not agree that you need any kind of choice to get from an isomorphism $\alpha:y^A\cong y^B$ an isomorphism $A\cong B$. For one thing, the Yoneda embedding is fully faithful, so the choice is unique. For another, you have an explicit formula for it given by evaluating $\alpha$ at the identity map of $A.$

sarahzrf (Feb 14 2025 at 02:31):

you certainly don't need choice to pass between isomorphisms $y^A \cong y^B$ and $A \cong B$, but the knowledge that $|A| = |B|$ is not the data of an isomorphism $A \cong B$, it's the propositional truncation thereof

sarahzrf (Feb 14 2025 at 02:31):

that's what i meant about decategorification

sarahzrf (Feb 14 2025 at 02:32):

in general, if i know that $|A| = |B| = 3$ for example, that furnishes me with no choice of a bijection $A \cong B$, it only tells me that one exists. There will in fact be six possible bijections, none of which are preferred without further structure on $A$ or $B$

JR Learnstomath (Feb 14 2025 at 09:37):

Sorry I'm late to the party, but I was really delighted to find @Joachim Kock 's lecture, "Polynomial functors — from elementary arithmetic to infinity-operads" where he explains the link between the Poly he works on and @David Spivak and all's at about 32:00 minutes.

There seems to be also another category Poly, which is a left-additive one that I first met in @Bruno Gavranović 's dissertation, which is also different. So if I understand it well, there are 4 different "kinds" of Poly, is that right? (These 3, of which I think one is a "sub-concept" of another but I'm not sure which way it goes, and the Vect-related Poly that Joachim mentioned above.)

JR Learnstomath (Feb 14 2025 at 09:45):

I've been trying to do a "descent" on each of these Polys and have been getting pretty confused on the "gluing". (Sorry for all of the ""'s, it's hard to talk in normal language now that I've discovered that there are precise and agreed-upon definitions of particular things). To help keep the different Polys separate in my mind, I'm using the following names:

• Poly Combi Pal (Kock et. al.)
• Poly R&U (for rainbows and unicorns, from David Spivak's I love poly blog post, which I can't seem to find anymore)
• Poly Lala (left additive, as mentioned by Gavranović)
• Poly Victor (obviously the vect one)
  Are there actual, official ways to call each of the different ones?

JR Learnstomath (Feb 14 2025 at 09:47):

(I thought to post these questions here to keep it close to Joachim's and other's references, and to maybe clarify future discussion on it, but now I'm wondering whether I should have put it on learning channel -- please let me know whether these questions should have gone there, thank you)

Matteo Capucci (he/him) (Feb 14 2025 at 15:05):

If someone from ACT/Topos-sphere mentions Poly I usually assume they mean polynomial functors over Set of one variables, but otherwise most category theorist mean polynomials à là Gambino-Kock, which are defined on any LCCC category $\cal E$ and strictly related to the first for $\cal E=\bf Set$. There are also Ghani-Abbott containers, and Spivak dependent lenses, which are again equivalent presentation of polynomial functors Set of one variables.

David Corfield (Feb 14 2025 at 15:32):

Like Bob Dylan going electric, are there signs people like @David Spivak are going homotopic?

image.png

Matteo Capucci (he/him) (Feb 14 2025 at 15:34):

It's... ineluctable

Matteo Capucci (he/him) (Feb 14 2025 at 15:35):

There is, needless to say, also a theory of $\infty$-polynomials, as worked out e.g. here