Proposition (Q is State(D)). Q is isomorphic to State(D).
[[_]]D : | LGraph(Mix(C,P)) | D | |
[[_]]Q : | State(LGraph(Mix(C,P))) | Q |
We will now define an identity-on-objects isomorphism between Q and State(D):
By definition, G : XS YS in LGraph(Mix(C,P)) and so define:
which gives us:
By definition, G : X Y in State(LGraph(Mix(C,P))) and so define:
It is routine to show that st and ts are symmetric premonoidal functors, and that they form an isomorphism.