# Proof that Q is State(D)

Proposition (Q is State(D)). Q is isomorphic to State(D).

Proof. Since the pushout defining Q was taken in the category of strict symmetric premonoidal categories, the following diagram commutes:

[[_]]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):

- For any f : X Y in Q we can find (since [[_]]Q is epi) a graph G : X Y in State(LGraph(Mix(C,P))) such that:

  [[G : X Y]]Q = f : X Y

  By definition, G : XS YS in LGraph(Mix(C,P)) and so define:

  st(f) = [[G : XS YS]]D : X S Y S in D

  which gives us:

  st(f) : X Y in State(D)

- For any f : X Y in State(D), we have f : X S Y S in D. We can find (since [[_]]D is epi) a graph G : XS YS in LGraph(Mix(C,P)) such that:

  [[G : XS YS]]D = f : X S Y S in D

  By definition, G : X Y in State(LGraph(Mix(C,P))) and so define:

  ts(f) = [[G : X Y]]Q : X Y in Q

It is routine to show that st and ts are symmetric premonoidal functors, and that they form an isomorphism.

Back