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
The store comonad (also costate comonad) is a comonad (in computer science) used to implement computational storage and retrieval of data in functional programming.
As a comonadic triple it is given by an endofunctor,
with natural transformations the counit,
usually called extract and comultiplication,
simply called duplicate.
In a locally Cartesian closed category/dependent type theory , then to every type is associated its base change adjoint triple
In terms of this the store comonad is the composite
of context extension, followed by dependent product , followed by context extension, followed by dependent sum.
Here is called the function monad or reader monad and is the writer comonad.
Jeremy Gibbons, Lenses are the coalgebras for the costate comonad
function monad (reader monad)
Last revised on August 24, 2018 at 11:13:47. See the history of this page for a list of all contributions to it.