Indexed Lawvere theories for local state

John Power – 27 May 2020

After my most recent seminar, a few of the participants, notably Sophie, Steve and Mike, expressed interest in local state. I wrote two papers about local state after the paper I presented last time. So I thought it might be helpful for me to speak about the last one, despite its being ten years old and not being definitive.

The goal was to understand the algebras for the monad on [Inj,Set] for local state as the models of a kind of Lawvere theory. I could not achieve that, but I made some progress. I introduced the notion of a D-indexed Lawvere theory and its models, with the leading example having D=Inj, thus not having finite products. So the definition is not as one would expect from the perspective of fibrations. Moreover, with the specific goal firmly in mind, I took models in an ordinary category with finite products rather than in a D-indexed category with finite products, thus another strange definition.

That, together with the use of a tensor of theories, allowed me to model lookup and state, but for block, one needs a way of moving from a state with n locations to a state with n+1 locations. Exponentiation with the final comodel of a Lawvere theory allowed me to do that, thus modelling block, but I could not see how to model some block axioms, so I ended with the most elegant hack I could see.