Gagallium

In this Agda file, I give an introduction to Lawvere theories and Monads. It’s not exactly a “gentle” introduction because:

1. I’m still trying to grok these things myself,
2. 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.