Contents

### Context

#### Mapping space

internal hom/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$.

In the context of monads in computer science this is called the writer comonad. This is of interest in functional programming languages such as Haskell, where a program for the form $X \longrightarrow W \times Y$ behaves like taking input of type $X$ to output of type $Y$ while in addition producing output (“side effect”) of type $W$.

If here $W$ is equipped with the structure of a monoid, then $W \times (-)$ also canonically inherits the structure of a monad, allowing aggregation of a program’s $W$ outputs, corresponding to a sort of side channel. (See writer monad.)

## 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 \,.$