Contents

mapping space

# Contents

## Idea

In a cartesian closed category/type theory $\mathcal{C}$, given any object/type $W$ there is a comonad

$W \times (-) \colon \mathcal{C} \to \mathcal{C}$

given by forming the Cartesian product with $W$

If here $W$ is equipped with the structure of a monoid, then $W \times (-)$ also canonically inherits the structure of a monad (see writer monad).

In the context of monads in computer science this is called the writer monad. This is the case of interest in functional programming languages such as Haskell, where a program for the form $X \longrightarrow W \times Y$ behaves like a program taking input of type $X$ to output of type $Y$ while in addition producing output of type $W$, which is aggregated using the the monoid when the functions are composed, creating a sort of side channel.

## Properties

In a cartesian closed category/type theory $\mathcal{C}$, the writer comonad $W\times (-)$ is left adjoint to the reader monad $[W,-]$.

### In terms of dependent type theory

If the type system is even a locally Cartesian closed category/dependent type theory then for each type $W$ there is the base change adjoint triple

$\mathcal{C}_{/W} \stackrel{\overset{\sum_W}{\longrightarrow}}{\stackrel{\overset{W^\ast}{\longleftarrow}}{\underset{\prod_W}{\longrightarrow}}} \mathcal{C}$

In terms of this then the writer comonad is equivalently the composite

$\sum_W W^\ast = W\times (-) \;\colon\; \mathcal{C} \longrightarrow \mathcal{C}$

of context extension followed by dependent sum.

One may also think of this as being the integral transform through the span

$\ast \leftarrow W \rightarrow \ast$

(with trivial kernel) or as the polynomial functor associated with the span

$\ast \leftarrow W \stackrel{id}{\rightarrow} W \rightarrow \ast \,.$