Let C be a CCC. Let (×) be a product bifunctor in C. Cat is CCC, so we can curry (×):
curry (×) : C→(C⇒C)
curry (×) A = λB. A×B
Functor category C⇒C has usual monoidal structure. A monoid in C⇒C is a monad in C. We consider finite products as monoidal structure on C.
curry (×) 1 ≅ id
∀ A B. curry (×) (A×B) ≅ (curry (×) A) ∘ (curry (×) B)
Therefore (curry (×)) preserves monoidal structure, so it transports a monoid to a monad and a comonoid to a comonad. This is a construction for Coreader and Writer. What about Reader and Cowriter? Intuitively, we should use adjunction in CCC, though I can not understand how it is explained formally.
|canonical comonoid in a category with products||base.Control.Monad.Reader.Reader||Hackage.category-extras.Control.Comonad.R