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.
André Muricy Santos (Jan 07 2024 at 12:14):Our master's thesis on implementing Poly and mode-dependent dynamical systems in Cubical Agda was finally published :)
https://odr.chalmers.se/server/api/core/bitstreams/774ba4a2-58b4-407f-aa6b-b0209b6c7d70/content
John Baez (Jan 07 2024 at 13:51):Congratulations! Do you think someone will apply this?
André Muricy Santos (Jan 07 2024 at 13:57):Thank you John! I don't know, but I want to see if poly is helpful to dynamical systems experts, I have a meeting with a researcher at Chalmers later this month where I'll show this and other work, maybe something comes out of that :)
John Onstead (Jan 11 2024 at 00:28):Thanks for sharing your work!
I'm currently learning category theory and I was wondering about a few things in the paper. First, I was wondering what the relation of Poly and Chart is to the functor category of all endofunctors on Set - are they subcategories, and if so, in what way? If they are subcategories, would that make the monoid objects in Poly monads? Lastly I am confused by the note that Chart could also be called the "arrow category" of Set. Usually I think of arrow categories of C as being where the objects are morphisms in C and morphisms are commuting squares in C, IE, a functor category from the interval category to C. In which sense of "arrow category" is Chart an example of?
André Muricy Santos (Jan 11 2024 at 11:54):Thanks for the questions :)
Poly is a subcategory of [Set,Set], but Chart is not! The reason I know this is because arrows between charts are not natural transformations. I don't know which canonical categorical structure they are, but they are not NTs :thinking: I believe I've asked this before on this Zulip in fact. So yes monoids in Poly are monads, and comonoids are comonads.
As for that note, here's how to see charts as commuting squares.
Imagine this polynomial instead as a function from the directions to the positions, so the domain is the union of the direction at every position, and the codomain is the positions. Then you can view a chart as a pair of functions that form a square; each polynomial is a function, and the upper part of the chart (the map on directions) is the upper part of the square and the lower part (the map on positions) is the lower part of the square. This square commutes because in the context of charts, maps on directions are limited to be maps at that position.
This example from the thesis shows that. If you were to start at a direction of the left polynomial, go right to the right polynomial, then down to its position, you'll always land at the same position as if you had gone down to a position first (so you stay at the left polynomial) then left to a position on the right.
