The monad and examples from Haskell: A computer-checked library for Category Theory in Lean

Category Theory is a widely used field of Mathematics.<br/>Some concepts from it are often used in functional programming.<br/>This paper will focus on the Monad and a few implementations of it from Haskell.<br/>We will also present the computer-checked library we have written to help us in this task.