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.
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?