kan-extensions-3.6.2: Kan extensions, Kan lifts, various forms of the Yoneda lemma, and (co)density (co)monads

Portabilitynon-portable (GADTs, MPTCs)
MaintainerEdward Kmett <ekmett@gmail.com>
Safe HaskellTrustworthy



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' genererated 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.



data Density k a whereSource


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

liftDensity :: Comonad w => w a -> Density w aSource

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 aSource

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