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: applied category theory

Topic: Sy^S vs coalgebras

Nathaniel Virgo (Aug 18 2021 at 13:01):

I'm working my way through the Topos institute polynomial functors course, but only very slowly, so I've just finished day 3.

One thing that struck me is that in that course a Moore machine is defined as a natural transformation $Sy^S\to By^A$. This was kind of surprising to me because for me the more obvious way to define a Moore machine is as a coalgebra of the functor $By^A$. (That is, a set $S$ together with a function $S\to (By^A)(S) = B\times S^A$.) It seemed kind of odd that specifying a functor $Sy^S\to By^A$ would be the same as specifying a coalgebra, and I wondered if it was just a coincidence or if there's something more to it.

After a bit of thought, I realised it's the same for any functor $F\colon \mathbf{Set}\to\mathbf{Set}$. (It doesn't need to be a polynomial functor.) Specifying a natural transformation $Sy^S\to F$ is equivalent to specifying a coalgebra of $F$ whose underlying object is $S$. The proof is similar to the proof of the Yoneda lemma. (Or maybe there's a neat way to use Yoneda to prove it, I'm not sure.)

But this still seems kind of mysterious to me, and I'm wondering if anyone has any insight into what's really going on.

In particular, the coalgebras of a functor form a category, whereas natural transformations between two functors only form a set. So I'm wondering whether there is a natural notion of morphism from a natural transformations $Sy^S\to F$ to a natural transformation $Ty^T\to F$, such that it turns out to be equivalent to a coalgebra homorphism.

Jacques Carette (Aug 18 2021 at 13:06):

The natural notion of morphisms of natural transformations are called modifications. You might be interested in looking at transfors as well. [I don't know the actual answer to the question, only that 'modification' is very likely to be part of the answer.]

Henry Story (Aug 18 2021 at 21:40):

Ah happy to have a place to come to do talk about the topos course on Poly :-)
I was also quite confused or wondering about the relation to coalgebras. So I was really happy when on Day 4.5 @David Jaz gave a talk that really went into that aspect. https://twitter.com/bblfish/status/1424454040985944066

Ah finally! @myers_jaz explains how Poly relates to and differs from Coalgebras! https://www.youtube.com/watch?v=QNuGyjHJtP8&list=PLhgq-BqyZ7i6IjU82EDzCqgERKjjIPlmh&index=6

- The 🐟‍‍ BabelFish (@bblfish)

Henry Story (Aug 18 2021 at 21:42):

In that Tweet thread I also point to an earlier high level Math professional-dan-players-level workshop on Poly where modal logic and coalgebras was discussed and Bart Jacobs gave a talk...

Henry Story (Aug 18 2021 at 21:49):

Are those recorded in Berkley btw? It seems that the quality of recording is not as good as it was at MIT or when people were just presenting from home. Perhaps moving to tablets would be better? Having to watch Nelson and David wear masks, while jumping around from one side of the room to the other drawing diagrams, makes me feel like I am asphyxiating. :mask:

Valeria de Paiva (Aug 18 2021 at 21:59):

@Henry Story well, Berkeley now has regulations about use of masks indoors, so they have to wear masks to comply.

Henry Story (Aug 18 2021 at 22:01):

:-) I guessed that, especially as the last few lectures they were the only two in the room I think. At that point I was thinking it may be healthier to work by drawing the diagrams on a tablet from home.

Henry Story (Aug 18 2021 at 22:14):

At the same time I get the feeling that the physical activity of writing on a white board makes it easier to be enthusiastic about the subject, in a way that is more difficult to get through when sitting at a table.

Valeria de Paiva (Aug 18 2021 at 22:25):

they're writing the book together, so presumably they know what's best for their goal.

Henry Story (Aug 18 2021 at 22:28):

Very helpful book. I was reading it and also Jaz Myers' book.

Nick Smith (Aug 18 2021 at 23:20):

FWIW I very much prefer seeing a real person draw on a real whiteboard than a disembodied head sketching with an invisible hand into a note-taking app. In the latter case, you lose the ability to easily point and gesture at what was already written.

Nick Smith (Aug 18 2021 at 23:25):

@Nathaniel Virgo During the Day 8 lecture David Spivak explains how Poly is "co-closed" with respect to $\lhd$, and this yields the equivalence between $Sy^S \to p$ and $S \to p(S)$. Perhaps this is what you are looking for?

Nick Smith (Aug 18 2021 at 23:34):

As for coalgebra homomorphisms, it's possible these are the 2-cells in the double category $\mathbb{P}$ (briefly discussed in the unfinished Part III of the book), but I'm not sure.

Matteo Capucci (he/him) (Aug 19 2021 at 09:01):

Nathaniel Virgo said:

In particular, the coalgebras of a functor form a category, whereas natural transformations between two functors only form a set. So I'm wondering whether there is a natural notion of morphism from a natural transformations $Sy^S\to F$ to a natural transformation $Ty^T\to F$, such that it turns out to be equivalent to a coalgebra homorphism.

These morphisms between coalgebras should be embodied by charts (see Myers' book on dynamical systems, or his paper on double categories of systems). More precisely, such coalgebra morphisms form a 'triangle' in the double category of arenas, i.e. a square whose bottom side is the identity. The two vertical sides are the coalgebras, and the top horizontal side is a chart.
What I want to say is that once we identify what a chart in Poly is (a question that @Jérémy Ledent asked some time ago), then we'd answer what a coalgebra morphism is

Nathaniel Virgo (Aug 19 2021 at 14:17):

That sounds promising. I think I see it. Below I post the diagrams I used to help me understand it, as I think they might be helpful.

One wrinkle is that the correspondence between natural transformations $Sy^S \to F$ and coalgebras of $F$ seems to hold not only for polynomial functors, but for any endofunctor on Set. So it seems like maybe we should be seeking a generalisation of this picture to aribitrary functors somehow, rather than just polynomial ones?

Here's what I think a square looks like in that double category, in a sort of weird combination between string diagrams and a commutative diagram. (A unique square exists if and only if the diagram commutes.)

image.png

The horizontal morphisms are charts (all arrows point left to right) and the vertical ones are lenses (some arrows point up, others point down). Then the triangle you describe sounds like this

image.png

But I think we have to simplify it to this special case (or is that forced on us somehow)?

image.png

then I think that is the same as a coalgrabra morphism between coalgebras of $By^A$, though it's not completely obvious to me.

Matteo Capucci (he/him) (Aug 19 2021 at 15:10):

I think the special case is forced since $A^-$ is functorially determined by $A^+$ for systems (that's the $T$ part of a doctrine of dynamical systems). In this doctrine, $T$ is the identity on objects and promotes a morphism $f$ to the chart $(f, \pi_2 ; f)$, which recovers the special case

Matteo Capucci (he/him) (Aug 19 2021 at 15:10):

I really love these diagrams btw!!

Matteo Capucci (he/him) (Aug 19 2021 at 15:14):

What I have no clue about is what charts ought to be in Poly... Ofc you can 'artifically' add them following the usual double Grothendieck construction that creates doctrines of dyn systems, but I'd like to see them pop out in another way. I mean, lenses pop out in Poly as natural transformations, i.e. the canonical notion of morphism between functors. There should be another notion of morphism that gives charts, apparently

Matteo Capucci (he/him) (Aug 19 2021 at 15:21):

Mmmh this is interesting: instead of polynomials, consider Dirichlet polynomials, i.e. consider $SS^y$ instead of $Sy^S$. Then nat transformations $SS^y \to TT^y$ are given by charts! In fact:

$$[SS^y, TT^y] = \big[\sum_{s \in S} \mathrm{Set}(-,S), \sum_{t \in T} \mathrm{Set}(-,T)\big] = \prod_{s \in S} \sum_{t \in T} \mathrm{Set}(S, T) = (S \to T) \times (S \times S \to T)$$

Matteo Capucci (he/him) (Aug 19 2021 at 15:23):

I don't know what to do with this fact: we have the right morphisms, but in the wrong category!

John Baez (Aug 19 2021 at 17:34):

Henry Story said:

Are those recorded in Berkeley btw?

Yes, on the 6th floor of the Wells Fargo building.

It seems that the quality of recording is not as good as it was at MIT or when people were just presenting from home.

That's true.

Perhaps moving to tablets would be better.

I'm not sure what that means.

John Baez (Aug 19 2021 at 17:51):

Anyway, you should send your comments to David Spivak if you want someone to do something about this.

Henry Story (Aug 19 2021 at 18:29):

John Baez said:

Anyway, you should send your comments to David Spivak if you want someone to do something about this.

Oh, I think he's aware of that. They have been having problems with video quality and sound breaking up since the beginning of the course, where they did not have this problem at MIT and the whole of last year when courses were online.
By a Tablet, I mean the way @Thorsten Altenkirch did his presentation on "Containers and Inductive Types" in the Workshop on Polynomials earlier this year referring to work by @Conor McBride . (His talk is important as it gives the CS terminology for the subject, which clashes with the new one.) https://www.youtube.com/watch?v=hBC2seNe3YE

Henry Story (Aug 19 2021 at 18:41):

Ah, I just found that there was a thread here on Zulip, regarding Thorsten's Topos talk on Containers (Polynomials functors) and inductive types.

Henry Story (Aug 19 2021 at 18:55):

I became especially interested in Poly as it seems that as a model of dynamical systems they could provide insight into Actor Systems such as Erlang or Akka.
Those actor Systems were thought up in the 1970s and are quite easy to conceptualise by thinking of Actors as people sending each other messages to mailboxes on which they act one at a time. The model goes beyond Object Oriented Programming, because Actors can deal very well with highly concurrent and dynamic systems. E.g. PayPal was using Akka on 8 servers to process 1-10 billion transactions a day a couple of years ago.
So since Bart Jacobs presented OO as coalgebras, and these appear in polynomials as lenses, but polynomials are apparently also very good for dynamic systems that can change behavior this is very intruiging. I started a thread on Poly and Actors, in case people have ideas there. It also ties in a bit with the recent discussion on Optics (also Lenses) and Web Servers, which I was trying to understand, but before knowing about Poly.

Note that Actors can also change behavior. I guess that would map to Polys being Sums of representable functors. Each element of the Sum corresponding to a different behavioral state.

dusko (Aug 25 2021 at 14:11):

Nathaniel Virgo said:

I'm working my way through the Topos institute polynomial functors course, but only very slowly, so I've just finished day 3.

One thing that struck me is that in that course a Moore machine is defined as a natural transformation $Sy^S\to By^A$. This was kind of surprising to me because for me the more obvious way to define a Moore machine is as a coalgebra of the functor $By^A$. (That is, a set $S$ together with a function $S\to (By^A)(S) = B\times S^A$.) It seemed kind of odd that specifying a functor $Sy^S\to By^A$ would be the same as specifying a coalgebra, and I wondered if it was just a coincidence or if there's something more to it.

After a bit of thought, I realised it's the same for any functor $F\colon \mathbf{Set}\to\mathbf{Set}$. (It doesn't need to be a polynomial functor.) Specifying a natural transformation $Sy^S\to F$ is equivalent to specifying a coalgebra of $F$ whose underlying object is $S$. The proof is similar to the proof of the Yoneda lemma. (Or maybe there's a neat way to use Yoneda to prove it, I'm not sure.)

But this still seems kind of mysterious to me, and I'm wondering if anyone has any insight into what's really going on.

In particular, the coalgebras of a functor form a category, whereas natural transformations between two functors only form a set. So I'm wondering whether there is a natural notion of morphism from a natural transformations $Sy^S\to F$ to a natural transformation $Ty^T\to F$, such that it turns out to be equivalent to a coalgebra homorphism.

yoneda gives a bijection between $\mathsf{Nat}(\mathbf{C}(S,-), G)$ and $GS$ for any $G:\mathbf{C}\to \mathbf{Set}$. Taking $\mathbf{C} = \mathbf{Set}$ and $G = \mathbf{Set}(S,F-)$ for an arbitrary $F:\mathbf{Set}\to \mathbf{Set}$ gives the bijection between $\mathsf{Nat}(\mathbf{Set}(S,-), \mathbf{Set}(S,F-))$ and $\mathbf{Set}(S,FS)$. writing the homs internally and transposing the $S$ brings the nats into the form $\mathsf{Nat}(S\times (-)^S, F-)$. and the elements of the other hom are the coalgebras $S\to FS$. so it is the yoneda lemma for coalgebras: there is a bijection between the $F$-coalgebras over $S$ and the $$S$-indexed $X$-natural families of $F$-coalgebras $X^S \to FX^S$. well spotted!

Henry Story (Aug 26 2021 at 12:43):

I am wondering what Sy^S and coalgebras can tell us about access control modes.
Essentially lenses come with 2 interaction patterns:

* get
* set
(corresponding to JavaBeans™ getters and setters).

For access control on web resources we have found the need for Read and Write modes for sure, which fit very nicely those getters and setters.
But there are good arguments in favor of Append, Delete, Create, too...
Anyone have any thoughts of how those modes of interactions also appear in Sy^S?

Henry Story (Aug 26 2021 at 13:03):

In the thread Optics and Servers I thought that the HTTP POST which is behind the need for Created on a collection, could be modelled in a Lens as an update to a collection. Append would work for adding data to a collection. So it seems like both of these modes appear when one has a lens fixed on a collection, but one does not want to replace the whole collection, but just alter it in monotonic ways.
Delete is problematic as one does not want to delete an element and all contained elements too...
It would be nice to have a mathematical foundation for this.

Spencer Breiner (Aug 26 2021 at 19:02):

Henry Story said:

But there are good arguments in favor of Append, Delete, Create, too...
Anyone have any thoughts of how those modes of interactions also appear in Sy^S?

It looks to me like there are two different ways to do this, depending on your assumptions. Suppose our system is represented as a map $Sy^S\to Oy^I$.

The question is whether we "append" $I$ to (i) the state $S$ or (ii) the output $O$. For (i) we have $ap:S\times I\to S$, and we can just use this to replace the original $put:S\times I\to S$. Most likely $ap$ is a monoid action, and you could maybe use this to get a section of the projection $get:\mathbf{Poly}(Sy^S,Oy^I)\to\mathbf{Set}(S,O)$ (natural in ???).

Alternatively, and probably closer to your case of interest, you might want to let $O$ act on $I$ ($ap':O\times I\to I$), and update $S$ using the original $put$. This would define a new system with $get'=get$ and $put'(s,i) = put(s,ap'(get(s),i)$. A bit more abstractly, we think of this as a map $(id,ap'):Oy^I\to Oy^I$ and post-compose .

Henry Story (Aug 27 2021 at 08:58):

Thanks @Spencer Breiner , those ideas will give me a running example to think of as I go through the Poly courses more carefully.

I wrote a very simple test implementation using Scala's Monocle Lens library last month. The data structure is a nested set of maps. But I think a Tree with data at the leaves would be better. Elements of the tree are accessible by paths which are list of Strings. An example path is ["blog","2021","07","jump-monads-from-conjugation-to-dependent-types"] in a url such as https://topos.site/blog/2021/07/jump-monads-from-conjugation-to-dependent-types/.

• A GET fetches the state at that path location
• A PUT would change the state at the given path.
• A POST to a non-leaf tree, creates a new branch in the tree.
• a POST to a leaf can append the content to the resource, if that is a monoid like data structure (I like that idea).
• DELETE is currently only defined (/allowed) on leaves.

I think that describes a web server (without access control) quite well.
Now I need to find the Poly that goes with that. I think there were examples of trees in the course... If I remember correctly those would be nested polys, so represented as boxes within boxes, or directions of directions, ...

Henry Story (Sep 01 2021 at 12:57):

I have opened a web-cats issue on lenses and the web and have worked on a implementation of a fantasy lens-based web server that I hope can show that we are in the right mathematical space. It's going to take more time to get this translated to Poly, but is is already helpful for helping answer some basic questions on web access control.

Henry Story (Sep 08 2021 at 16:50):

There is evidently a relation between Lenses and CRUD: Create, Read, Update, Delete - Is that nicely written out somewhere? (Or is that just too obvious?)
The insert and update is demonstrated here in Monocle for a Map