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: event: ACT20

Topic: July 7: David Spivak's talk

Paolo Perrone (Jul 02 2020 at 02:15):

Hello all! This is the thread of discussion for the talk of David I. Spivak, "Poly: An abundant categorical setting for mode-dependent dynamics".
Date and time: Tuesday July 7, 21:10 UTC.
Zoom meeting: https://mit.zoom.us/j/7055345747
YouTube live stream: https://www.youtube.com/watch?v=5Rs_7ZCH1Wc&list=PLCOXjXDLt3pZDHGYOIqtg1m1lLOURjl1Q

David Spivak (Jul 07 2020 at 20:43):

slides for my talk today:
Poly_dynamics-ACT2020.pdf

Paolo Perrone (Jul 07 2020 at 21:05):

5 minutes!

Paolo Perrone (Jul 08 2020 at 02:34):

Here's the video!
https://www.youtube.com/watch?v=ajGRZkAwxWc&list=PLCOXjXDLt3pYot9VNdLlZqGajHyZUywdI

Johannes Drever (Jul 08 2020 at 10:14):

Thank you for the great talk, @David Spivak ! The slide on "mode-dependence" reminded me of state dependent behaviour in the actor model. E.g. a mailbox which accepts a number of messages up until a certain capacity and rejects message when it is full (as described here). I would be interested if these ideas relate to Poly, do you see analogies to the actor model?

Guillaume Boisseau (Jul 08 2020 at 14:04):

@David Spivak Very interesting talk! The lens-based wiring diagrams gave me the following idea: in a lens $(S, S) \to (B, A)$, you care about what happens on $A$ and $B$, but not really what happens on $S$. In some sense it might be nice to quotient or existentially quantify the $S$ away. Turns out that you do that with a coend, you get $\int^S Lens((S,S), (B, A)) \cong \int^C Poly(C \times A, C \times B)$. Mario mentioned this thing in passing in his talk; this is the Hom-set of the free category with feedback on $Poly$. I would guess that the reason your wirings are allowed to have loops is because they secretly live in that category.

David Jaz (Jul 08 2020 at 14:07):

Guillaume Boisseau said:

David Spivak Very interesting talk! The lens-based wiring diagrams gave me the following idea: in a lens $(S, S) \to (A, B)$, you care about what happens on $A$ and $B$, but not really what happens on $S$. In some sense it might be nice to quotient or existentially quantify the $S$ away. Turns out that you do that with a coend, you get $\int^S Lens((S,S), (A,B)) \cong \int^C Poly(C \times A, C \times B)$. Mario mentioned this thing in passing in his talk; this is the Hom-set of the free category with feedback on $Poly$. I would guess that the reason your wirings are allowed to have loops is because they secretly live in that category.

I'm not sure how this coend works. In the expression, $S$ appears contravariantly both times. Is this just a colimit?

Guillaume Boisseau (Jul 08 2020 at 14:15):

$S$ does appear both co- and contravariantly: $Lens((S,S),(A,B)) \cong C(S, A) \times C(S \times B, S) \cong \int^X C(S, X \times A) \times C(X \times B, S)$

Guillaume Boisseau (Jul 08 2020 at 14:17):

The objects of $Lens$ are morally those of $C \times C^{op}$, and the pair $(S, S)$ should be read as living there.

Guillaume Boisseau (Jul 08 2020 at 14:20):

Actually by quotienting $S$ we lose the capacity of provinding an initial $S$, so we might want something a bit different

Toby Smithe (Jul 08 2020 at 14:21):

Yes, this is almost what I did with my hacky definition of Dyn on slide 36 of my talk (def 4.2 of the abstract), but I decided against it because of the problem you just sketched. But otherwise the idea you described of "not caring about S" is what I was aiming for with my dependent sum.

Toby Smithe (Jul 08 2020 at 14:22):

With that definition, I was also trying to say "there is some state space, but I don't really care what"

Guillaume Boisseau (Jul 08 2020 at 18:50):

It's not too hard to add an initial state to this: simply require some additional $C(1, S)$. Once coended away, if the category has coproducts, we get $\int^X C(X \times A, X \times B) \times C(1, X) \times C(1, B)$. So you have to provide the initial $X$ and initial output. I guess we could also ignore the first output. So it's not quite free feedback anymore, but maybe not too different.

Guillaume Boisseau (Jul 15 2020 at 11:18):

And of course, like every time I think I'm onto something, @Mario Román was there before: https://ioc.ee/~mroman/notes/initializedfeedback.pdf

Jules Hedges (Jul 15 2020 at 12:53):

What society would look like if Guillaume and Mario collaborated rather than competed: Eb6s8w5XkAEPTOY.jpg

Mario Román (Jul 15 2020 at 17:21):

Jules Hedges said:

What society would look like if Guillaume and Mario collaborated rather than competed: Eb6s8w5XkAEPTOY.jpg

Hi Jules! Guillaume and I have actually been for quite a while discussing, exchanging ideas and working on problems together. Luckily for everyone, that has not resulted in an increase in flying cars (we already have enough with the ordinary ones). Your comment could be misinterpreted, but to make it totally clear: limited only by the time I dedicate to work, I have been always happy to collaborate with as many people as possible, and I think Guillaume has as well. :)

Mario Román (Jul 15 2020 at 17:24):

On the topic. I think this is page 47 on the slides of the ACT talk (https://ioc.ee/~mroman/talks/opendiagrams-act20.pdf) and sections 2.4 and 3.2 of the submission (https://ioc.ee/~mroman/publications/opendiagrams.pdf). The notes on traced profunctors by Exequiel Rivas are probably also relevant (https://dcc.fceia.unr.edu.ar/~erivas/traced.pdf).

Once we have that coend expression for feedback, a natural next step is to consider a different category in which the feedback occurs, by making the variable bounded by the coend range over a different category (this follows the idea of "algebraic lenses" from the ACT paper and the "achromatic lenses" of Guillaume's dissertation).

Actually, "categories with feedback" in the original by Katis, Sabadini and Walters, are the case where the coend is taken over the subgroupoid of isos of the category; and I understand from their work that these had other nice properties. Taking pointed objects instead of objects on the definition of feedback (if I am remembering correctly), one gets categories with "initialized feedback".

I think, at least, that this can be used to give further conceptual explanation to why lenses and feedback should be related at all. The observation of lenses/moore machines comes precisely from Schultz, Spivak, Vasilakopoulou.