In the field of algebraic computational effects, there is a Lawvere theory for global binary state (taking value either $0$ or $1$) which is generated by three operations
- $get: 2 \to 1$
- $put_0: 1 \to 1$
- $put_1: 1 \to 1$
subject to three natural equations which are specified in Notions of Computation Determine Monads. (I am only considering one store location and a binary variable, so my equations are fewer and simpler than in that paper.) The equations are more conveniently drawn than written:
It is more natural to interpret the equations from bottom to top. Respectively, they specify that
- putting $b$ and then putting $a$ is the same as just putting $a$
- getting the state, then putting $0$ if it was $0$, and $1$ if it was $1$ (before continuing along a joint path) is the same as doing nothing
- getting the state, and then getting the state again, is the same as just getting the state (and you can't get $0$ followed by $1$ or vice versa).
I can prove some simple and natural properties of this Lawvere theory, such as "getting the state, then putting $0$ if it was $0$, and $1$ if it was $1$ before continuing along a separate paths is the same as just getting the state". However I cannot prove equality between the two following diagrams:
This is roughy interpreted as "putting $0$ (resp. $1$) followed by getting" is the same as just "putting $0$ (resp. $1$) and following the left path (resp. right path)".
This seems to me an obvious relation in the theory for state, but I cannot manage to prove it! One of the following must hold
- I have misinterpreted the equations for state
- I have misinterpreted the true meaning of the equation I am trying to prove
- I am missing a simple trick for proving the equation from the state axioms
Can someone help me out? Thanks!