Adjoint Functors Induce Monads and Comonads

It is folklore knowledge that a pair of adjoint functors induces a monad and a comonad. Due to my recent work, I had to load relevant information into my brain cache. However, it turned out to be hard for me to find all the pieces of information I need in one place. Therefore, I am going to summarise here what I know and need, hoping it will be helpful for someone like me.

Deriving Monadic Programs

I started to take an interest in reasoning and derivation of monadic programs around 2016-17. Several years having passed, I collaborated with many nice people, managed to get some results published, failed to publish some stuffs I personally like, and am still working on some interesting tiny problems. This post summaries what was done, and what remains to be done.