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
hom-set, hom-object, internal hom, exponential object, derived hom-space
loop space object, free loop space object, derived loop space
Given an object $W$ in a category $\mathcal{C}$, if all binary cartesian products with $W$ exist, then taking the cartesian product with $W$ assembles into a comonad
whose comultiplication is induced by the diagonal map on $W$ and whose counit is induced by the terminal map $W \to \ast$.
When $W$ is furthermore equipped with the structure of a monoid, then $W \times (-)$ also canonically inherits the structure of a monad. (Regarded as a monad in computer science this models the aggregation of a programβs $W$-typed outputs, corresponding to a sort of side channel.) Equipped with this monad-structure, the operation $W \times (-)$ is known as the writer monad, see there for more.
On the other hand, if $W$ is further exponentiable then $W \times (-)$ is left adjoint to the reader monad $W \to -$, so that it is known as the reader comonad (eg. in the Haskell documentation for Control.Comonad.Reader) or coreader comonad (e.g. Ahman & Uustalu (2019)). It is also known as the product comonad (e.g. Uustalu & Vene 2008, p. 270) and the environment comonad (eg. in the Haskell documentation for Control.Comonad.Env).
If all binary cartesian products in $C$ exist, then the coreader comonad extends to a $C$-indexed comonad on $C$, i.e. a functor $C \to Comonad$. If $C$ has a terminal object $1$, then the environment comonad $1 \times -$ is isomorphic to the identity comonad.
If $C$ is a monoidal category rather than having all binary products, then tensoring with an object $\Gamma \otimes -$ can be given an analogous comonad structure when $\Gamma$ has a comonoid structure. In a cartesian monoidal category every object has a unique comonoid structure, which is what induces the coreader comonad. Even without assuming objects carry comonoid structures, the action sending $\Gamma$ to the functor $\Gamma \otimes -$ defines a strong monoidal functor from $C$ to the monoidal category of endofunctors $[C,C]$, a degenerate kind of graded comonad.
In a cartesian closed category/type theory $\mathcal{C}$, the coreader comonad $W\times (-)$ is left adjoint to the reader monad $[W,-]$.
The composite of coreader comonad followed by reader monad is the state monad.
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
In terms of this then the coreader comonad is equivalently the composite
of context extension followed by dependent sum.
One may also think of this as being the integral transform through the span
(with trivial kernel) or as the polynomial functor associated with the span
A coalgebra of the coreader comonad $W \times -$ is equivalent to simply a morphism $A \to W$ for $A$ the carrier of the co-algebra. Furthermore, the category of coalgebras is the isomorphic to the slice category over $W$. This shows that if all cartesian products with $W$ exist, then the forgetful functor $\Sigma_W \colon C / W \to C$ is comonadic.
Eg.
Danel Ahman, Tarmo Uustalu, p. 3 of: Decomposing Comonad Morphisms, CALCO 2019, Leibniz International Proceedings in Informatics (LIPIcs) 139 (2019) [doi:10.4230/LIPIcs.CALCO.2019.14]
Tarmo Uustalu, p. 13 of: Monads and Interaction Lecture 3, lecture notes for MGS 2021 (2021) [pdf, pdf]
Tarmo Uustalu, Varmo Vene, Comonadic Notions of Computation, Electronic Notes in Theoretical Computer Science 203 5 (2008) 263-284 [doi:10.1016/j.entcs.2008.05.029]
In Haskell:
See also:
Last revised on June 8, 2023 at 16:03:47. See the history of this page for a list of all contributions to it.