Contents

### Context

#### Categorical algebra

internalization and categorical algebra

universal algebra

categorical semantics

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

$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.

reader monad$W \to (\text{-})$ on cartesian typesunique comonoid structure on $W$
coreader comonad$W \times (\text{-})$ on cartesian typesunique comonoid structure on $W$
writer monad$A \otimes (\text{-})$ on monoidal typeschosen monoid structure on $A$
cowriter comonad$\array{A \to (\text{-}) \\ \\ A \otimes (\text{-})}$ on monoidal typeschosen monoid structure on $A$
chosen comonoid structure on $A$
Frobenius (co)writer$\array{A \to (\text{-}) \\ A \otimes (\text{-})}$ on monoidal typeschosen Frobenius monoid structure