kan-extensions-5.2: Kan extensions, Kan lifts, the Yoneda lemma, and (co)density (co)monads

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
 ComonadTrans (Density :: (Type -> Type) -> Type -> Type) Source # Instance detailsDefined in Control.Comonad.Density Methodslower :: Comonad w => Density w a -> w a # Source # Instance detailsDefined in Control.Comonad.Density Methodsfmap :: (a -> b) -> Density f a -> Density f b #(<\$) :: a -> Density f b -> Density f a # Source # Instance detailsDefined in Control.Comonad.Density Methodspure :: a -> Density f a #(<*>) :: Density f (a -> b) -> Density f a -> Density f b #liftA2 :: (a -> b -> c) -> Density f a -> Density f b -> Density f c #(*>) :: Density f a -> Density f b -> Density f b #(<*) :: Density f a -> Density f b -> Density f a # Source # Instance detailsDefined in Control.Comonad.Density Methodsextract :: Density f a -> a #duplicate :: Density f a -> Density f (Density f a) #extend :: (Density f a -> b) -> Density f a -> Density f b # Apply f => Apply (Density f) Source # Instance detailsDefined in Control.Comonad.Density Methods(<.>) :: Density f (a -> b) -> Density f a -> Density f b #(.>) :: Density f a -> Density f b -> Density f b #(<.) :: Density f a -> Density f b -> Density f a #liftF2 :: (a -> b -> c) -> Density f a -> Density f b -> Density f c # Source # Instance detailsDefined in Control.Comonad.Density Methodsduplicated :: Density f a -> Density f (Density f a) #extended :: (Density f a -> b) -> Density f a -> Density f b #

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 . liftDensity ≡ id


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 . adjunctionToDensity ≡ id
adjunctionToDensity . densityToAdjunction ≡ id


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

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

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 . densityToLan ≡ id
densityToLan . lanToDensity ≡ id