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.
David Corfield (Apr 03 2023 at 09:16):Having watched David Spivak's very interesting talk "Dynamic organizational systems", it seems the polynomial functors are everywhere in computer science. And all these even before generalising to dependent polynomials, which also find their use in CS, in e.g. Graph Neural Networks are Dynamic Programmers.
What prospects then for dependent polynomial functors with symmetries? Not just working in a topos like G-Set, but allowing data types to have symmetries, as in Joachin Kock's Data types with symmetries and polynomial functors over groupoids. Perhaps some form of equivariant learner?
There must be plenty of useful work already done in mathematics. There's the use of generalised polynomials in representation theory, known there as Tambara functors. And we were seeing here that double dimension reduction from physics is also an instance.
@DavidCorfield8 @myers_jaz @mattecapu @bgavran3 Hi, I had a similar curiosity in the past! Suppose we consider nLab polynomial (∞,1)-functors [https://ncatlab.org/nlab/show/polynomial+%28%E2%88%9E%2C1%29-functor] for ∞-groupoids. If I choose f: pt --> BG, it sounds like I should have a polynomial of the form p(X) = Hom(G,X)//G. Makes sense?
- Luigi Alfonsi (@alfonsi_luigi) David Corfield (Apr 04 2023 at 08:23):It seems that the direction of travel is towards higher h-level, as with the polynomials in groupoids in A Cartesian Bicategory of Polynomial Functors in Homotopy Type Theory. We might imagine then a double-category formulation, following Mike Shulman here:
The notion of cartesian bicategory was defined (by Carboni, Walters, Kelly, Verity, and Wood) to capture examples like these, but it is quite complicated. Moreover, to someone familiar with double categories, it is crying out to be reformulated in double-category language
John Baez (Apr 04 2023 at 18:15):That article was from 2018. I'd be sort of amazed if nobody had formulated cartesian bicategories using double categories yet. Maybe someone like Mike has done it by now?
Nathanael Arkor (Apr 04 2023 at 20:34):It is shown in Proposition 3.1 of Lambert's Double Categories of Relations that the underlying loose bicategory of a cartesian equipment is a cartesian bicategory.
Evan Patterson (Apr 04 2023 at 22:05):In addition to Michael's nice paper, Aleiferi's PhD thesis is all about cartesian double categories and cartesian equipments, which are the double-categorical analogue of the ideas around cartesian bicategories.
David Corfield (Apr 05 2023 at 08:10):Double categories of polynomial functors go back at least to Gambino and Kock's Polynomial functors and polynomial monads.
Jacques Carette (Apr 27 2023 at 19:42):"Dependent polynomials with symmetries": isn't the first case of that Species?
The mathematics of that is, of course, well understood. The applications to Computer Science are much more elusive. "Mathematician's symmetry" is rather hard to achieve in a computational setting. Oh, it's possible to do single cases in ad hoc ways, but what's hard is to do it uniformly, as the theory promises that it is possible to do.
Conor McBride and I are actively working on that. We put out various cryptic comments about that on Mastodon, and our working notes are public on github.
[And yes, we do know about QITs in HoTT. No, that's not a good answer.]