“A monad is a monoid in the category of endofunctors, what’s the problem?”
- Philip Wadler, allegedly
Actually, there is a problem. That statement isn’t true for Lean monads due to subtle universe reasons. Oh no!
Since I swear this isn’t a monad tutorial, I recommend you first read FPIL’s monad chapter for some background knowledge.
The main content of this post is in an interactive Lean file, so I recommend cloning the repo (just git clone that URL) and opening Main.lean in any text editor with a Lean plugin. Alternatively, you can copy-and-paste it into live.lean-lang.org. I wrote that file as notes for a category theory class that I’m helping teaching right now, so it’s relatively light on commentary right now.