kan-extensions-5.2.5: Kan extensions, Kan lifts, the Yoneda lemma, and (co)density (co)monads
Copyright (C) 2008-2016 Edward Kmett
License BSD-style (see the file LICENSE)
Maintainer Edward Kmett <ekmett@gmail.com>
Stability experimental
Portability non-portable (GADTs, MPTCs)
Safe Haskell Safe-Inferred
Language Haskell2010

Control.Comonad.Density

Description

The Density Comonad for a Functor (aka the 'Comonad generated by a Functor ) The Density term dates back to Dubuc''s 1974 thesis. The term Monad generated by a Functor dates back to 1972 in Street''s ''Formal Theory of Monads''.

The left Kan extension of a Functor along itself ( Lan f f ) forms a Comonad . This is that Comonad .

Synopsis

Documentation

data Density k a where Source #

Constructors

Density :: (k b -> a) -> k b -> Density k a

Instances

Instances details
ComonadTrans ( Density :: ( Type -> Type ) -> Type -> Type ) Source #
Instance details

Defined in Control.Comonad.Density

Functor ( Density f) Source #
Instance details

Defined in Control.Comonad.Density

Applicative f => Applicative ( Density f) Source #
Instance details

Defined in Control.Comonad.Density

Comonad ( Density f) Source #
Instance details

Defined in Control.Comonad.Density

Apply f => Apply ( Density f) Source #
Instance details

Defined in Control.Comonad.Density

Extend ( Density f) Source #
Instance details

Defined in Control.Comonad.Density

liftDensity :: Comonad w => w a -> Density w a Source #

The natural transformation from a Comonad w to the Comonad generated by w (forwards).

This is merely a right-inverse (section) of lower , rather than a full inverse.

lower . liftDensityid

densityToAdjunction :: Adjunction f g => Density f a -> f (g a) Source #

The Density Comonad of a left adjoint is isomorphic to the Comonad formed by that Adjunction .

This isomorphism is witnessed by densityToAdjunction and adjunctionToDensity .

densityToAdjunction . adjunctionToDensityid
adjunctionToDensity . densityToAdjunctionid

lanToDensity :: Lan f f a -> Density f a Source #

The Density Comonad of a Functor f is obtained by taking the left Kan extension ( Lan ) of f along itself. This isomorphism is witnessed by lanToDensity and densityToLan

lanToDensity . densityToLanid
densityToLan . lanToDensityid