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