It seems like there has to be some kind of relationship between lollipop and the sub-agent relation, right? Like, they’re both about one ‘agent’ sending info to another to combine to send something to the environment. But I’m not quite sure what the relationship is going to be: presumably it’s going to be that if C ◃ D, then C ⊸ D is {equal, isomorphic, biextensionally equivalent} to some special object, but IDK what that object would be.
So, I’d have thought there would be a morphism from C ⊸ ⊥ to (C ⊸ D) ⊗ (D ⊸ ⊥). You get a function from hom(C,⊥) to hom(C,D) x hom(D,⊥) from C being a subagent of D. But you also need a convenient function from hom(C ⊸ D, dual(D ⊸ ⊥)) to env(C). Now, dual(D ⊸ ⊥) is just D, so it’s really a function from hom(C ⊸ D, D) to env(C). But I have no idea what that function would be.
This thread is mostly me trying to work something out and reporting the results. To the extent there’s a question, it’s this: if C ◃ D, is there something interesting to say about C ⊸ D?
I am not sure, but I think that the answer is that you can’t say anything interesting with just ◃, but can maybe say interesting things with ◃+ and ◃×, which I am about to introduce. In the post that just went up, ◃+ is the relationship between one of the components and a sub-sum, and ◃× is the relationship between one of the components and a sub-tensor.◃ is the transitive closure of ◃+ and ◃×.
I think that if C◃+D, then there is a nice morphism from C to D, and if C◃×D, there is a set of nice morphisms from C to D, but in some degenerate cases that set is empty, which is how I constructed a counter example in my other comment.
I guess one version of this is that if C ◃ D, then for all e in the environment of C, there’s some (g,h) in agent(C ⊸ D) and (a,f) in env(C ⊸ D) such that e = h(f). So for all (a,e) in agent(C) x env(C), there’s (a’, e’) in agent(C ⊸ D) x env(C ⊸ D) so that a ⋅ e = a’ ⋄ e’. Which I guess is something.
It seems like there has to be some kind of relationship between lollipop and the sub-agent relation, right? Like, they’re both about one ‘agent’ sending info to another to combine to send something to the environment. But I’m not quite sure what the relationship is going to be: presumably it’s going to be that if C ◃ D, then C ⊸ D is {equal, isomorphic, biextensionally equivalent} to some special object, but IDK what that object would be.
So, I’d have thought there would be a morphism from C ⊸ ⊥ to (C ⊸ D) ⊗ (D ⊸ ⊥). You get a function from hom(C,⊥) to hom(C,D) x hom(D,⊥) from C being a subagent of D. But you also need a convenient function from hom(C ⊸ D, dual(D ⊸ ⊥)) to env(C). Now, dual(D ⊸ ⊥) is just D, so it’s really a function from hom(C ⊸ D, D) to env(C). But I have no idea what that function would be.
I believe, if C=⊤ and D=null, then C◃D, C⊸⊥≅0, C⊸D≅null and D⊸⊥≅null. Thus (C⊸D)⊗(D⊸⊥)≅null⊗null≅⊤, but there is no morphism from 0 to ⊤
Reader’s note: I wish there were somewhere I could look to see the definitions of 0, 1, null, top, and bottom, all in the same place.
For my personal use when I was helping review Scott’s drafts, I made some mnemonics (complete with silly emojis to keep track of the small Cartesian frames and operations) here: https://docs.google.com/drawings/d/1bveBk5Pta_tml_4ezJ0oWiq-qudzgnsRlfbGJgZ1qv4/.
(Also includes my crude visualizations of morphism composition and homotopy equivalence to help those concepts stick better in my brain.)
Thanks!
And now I’ve made a LW post collecting most of the definitions in the sequence so far, so they’re easier to find: https://www.lesswrong.com/posts/kLLu387fiwbis3otQ/cartesian-frames-definitions
You can prove there’s a morphism the other way, but that doesn’t rely on any subagency relationship.
Actually, you can get a morphism from (C ⊸ D) ⊗ (D ⊸ E) to C ⊸ E for any C, D, and E.
I haven’t put time into thinking about most of your comments yet, but I’m pretty sure the answer to this is yes.
EDIT: Oh, I just realized it wasn’t a question.
This thread is mostly me trying to work something out and reporting the results. To the extent there’s a question, it’s this: if C ◃ D, is there something interesting to say about C ⊸ D?
I am not sure, but I think that the answer is that you can’t say anything interesting with just ◃, but can maybe say interesting things with ◃+ and ◃×, which I am about to introduce. In the post that just went up, ◃+ is the relationship between one of the components and a sub-sum, and ◃× is the relationship between one of the components and a sub-tensor.◃ is the transitive closure of ◃+ and ◃×.
I think that if C◃+D, then there is a nice morphism from C to D, and if C◃×D, there is a set of nice morphisms from C to D, but in some degenerate cases that set is empty, which is how I constructed a counter example in my other comment.
And in my proof the morphism isn’t bijective.
I think it would have to involve some fixed point?
I guess one version of this is that if C ◃ D, then for all e in the environment of C, there’s some (g,h) in agent(C ⊸ D) and (a,f) in env(C ⊸ D) such that e = h(f). So for all (a,e) in agent(C) x env(C), there’s (a’, e’) in agent(C ⊸ D) x env(C ⊸ D) so that a ⋅ e = a’ ⋄ e’. Which I guess is something.