Idris2Doc : Control.Category.Comonad

Control.Category.Comonad

(source)
Definitions
interface CatComonad : Hom obj -> (obj -> obj) -> Type
  A *comonad* `w` is a comonoid object in the category of
  endofunctors in `cat`, where the tensor product is given by
  composition. Generally, `cat` is a category, though this is not
  enforced by the interface.
  
  This is the interface-style definition of a comonad. For the
  record-style definition, see `Control.Category.Records.ComonadR`.
  
  Laws (when `cat` is a category):
  * `counit . cojoin = id`
  * `map counit . cojoin = id`
  * `cojoin . cojoin = map cojoin . cojoin`

  Parameters: cat, w
Constraints: CatFunctor cat cat w
Constructor: 
MkCatComonad

Methods:
  
cojoin : cat (w a) (w (w a))
  The cojoin transformation of the comonad.
  
counit : cat (w a) a
  The counit transformation of the comonad.
cojoin : CatComonad cat w => cat (w a) (w (w a))
  The cojoin transformation of the comonad.

  Totality: total
  Visibility: public export
counit : CatComonad cat w => cat (w a) a
  The counit transformation of the comonad.

  Totality: total
  Visibility: public export
StrongComonad : Hom obj -> (obj -> obj -> obj) -> (obj -> obj) -> Type
  A strong comonad is a comonad that is also a costrong functor,
  with additional compatibility laws.
  
  Laws:
  * `mapr counit . costrongl = counit`
  * `mapl counit . costrongr = counit`
  * `costrongl . map costrongl . cojoin = mapr cojoin . costrongl`
  * `costrongr . map costrongr . cojoin = mapl cojoin . costrongr`

  Totality: total
  Visibility: public export
Id : Category cat => StrongComonad cat ten id
  Totality: total
  Visibility: public export