Contents

Idea

Let $\mathcal{C}$ be a closed monoidal category with tensor product and internal hom denoted by

respectively, and consider a monoid internal to $\mathcal{C}$:

Recall that the “$A$-action monad” induced by $A$ – often called the “$A$-writer monad” when considered as a monad in computer science – is the endofunctor of forming the tensor product with $A$

equipped with unit and multiplication structure morphisms induced, under the tensor product, from the unit and multiplication on $A$, respectively.

The analogous construction but with the tensor product replaced by the internal hom

which in computer science/type theory tends to be written

gives a comonad which hence deserves to be called the coaction comonad or cowriter comonad induced by $A$.

Alternatively, one might think to dualize the notion of the writer monad by considering a comonoid-object

and the induced comonad structure on $B \otimes (\text{-})$.

But if $\mathcal{C}$ is in fact a compact closed category, then these two notions agree: In this case the internal hom out of the monoid object $A$ is the tensor product with the dual comonoid object

Finally, if $A$ carries both monoid- and comonoid-structure in a compatible way to make a Frobenius monoid, then the induced (co)writer (co)monad structures are compatible to make a Frobenius monad.

Related concepts

References

The terminology “cowriter comonad” is used for instance in:

• Danel Ahman, Tarmo Uustalu, p. 5 of: Taking updates seriously, Proceedings of the Sixth International Workshop on Bidirectional Transformations (Bx 2017), CEUR Workshop Proceedings 1827 (2017) [pdf]

• Tarmo Uustalu, lecture notes for MGS 2021 (2021):

  p. 21 of: Monads and Interaction Lecture 3 [pdf, pdf]