internalization and categorical algebra
algebra object (associative, Lie, …)
internal category ($\to$ more)
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
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.
(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 |
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):
Last revised on August 11, 2023 at 20:11:11. See the history of this page for a list of all contributions to it.