nLab cowriter comonad

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}$:

$$A \,\in\, Mon\big(\mathcal{C}\big) \,.$$

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$

$$A \otimes (\text{-}) \;\colon\; \mathcal{C} \to \mathcal{C}$$

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

$$[A,\, \text{-}] \;\colon\; \mathcal{C} \to \mathcal{C}$$

which in computer science/type theory tends to be written

$$(A \to \text{-}) \;\colon\; \mathcal{C} \to \mathcal{C} \,,$$

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

$$B \,\in\, CoMon(\mathcal{C})$$

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

$$[A,\,\text{-}] \;\simeq\; A^\ast \otimes (\text{-}) \,.$$

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

(co)monad name	underlying endofunctor	(co)monad structure induced by
reader monad	$W \to (\text{-})$ on cartesian types	unique comonoid structure on $W$
coreader comonad	$W \times (\text{-})$ on cartesian types	unique comonoid structure on $W$
writer monad	$A \otimes (\text{-})$ on monoidal types	chosen monoid structure on $A$
cowriter comonad	$\array{A \to (\text{-}) \\ \\ A \otimes (\text{-})}$ on monoidal types	chosen monoid structure on $A$ chosen comonoid structure on $A$
Frobenius (co)writer	$\array{A \to (\text{-}) \\ A \otimes (\text{-})}$ on monoidal types	chosen Frobenius monoid structure

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]