In this Agda file, I give an introduction to Lawvere theories and Monads. It’s not exactly a “gentle” introduction because:
- I’m still trying to grok these things myself,
- I’ve to live up to my reputation of writing unfathomable gagaposts.
We’ll start with the State monad and, briefly, a Tick monad. The game is the following: I’ll present them syntactically – through a signature – and semantically – through a collection of equations. I’ll then show how the usual monad is related to this presentation.