λ-Files: Writer comonad in Coq

λ-Files: Writer comonad in Coq: In the last post , we reviewed Writer comonad in Haskell. In this post we will implement it in Coq. Since monads are not the part of standa...