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

Portabilityrank 2 types
Stabilityexperimental
MaintainerEdward Kmett <ekmett@gmail.com>
Safe HaskellTrustworthy

Data.Functor.Kan.Lan

Contents

Description

Left Kan Extensions

Synopsis

Left Kan Extensions

data Lan g h a whereSource

The left Kan extension of a Functor h along a Functor g.

Constructors

Lan :: (g b -> a) -> h b -> Lan g h a 

Instances

Functor (Lan f g) 
(Functor g, Applicative h) => Applicative (Lan g h) 
(Functor g, Apply h) => Apply (Lan g h) 

toLan :: Functor f => (forall a. h a -> f (g a)) -> Lan g h b -> f bSource

The universal property of a left Kan extension.

fromLan :: (forall a. Lan g h a -> f a) -> h b -> f (g b)Source

fromLan and toLan witness a (higher kinded) adjunction between Lan g and (Compose g)

 toLan . fromLanid
 fromLan . toLanid

glan :: h a -> Lan g h (g a)Source

This is the natural transformation that defines a Left Kan extension.

composeLan :: (Composition compose, Functor f) => Lan f (Lan g h) a -> Lan (compose f g) h aSource

composeLan and decomposeLan witness the natural isomorphism from Lan f (Lan g h) and Lan (f o g) h

 composeLan . decomposeLanid
 decomposeLan . composeLanid

decomposeLan :: Composition compose => Lan (compose f g) h a -> Lan f (Lan g h) aSource

composedAdjointToLan :: Adjunction f g => h (g a) -> Lan f h aSource

lanToComposedAdjoint :: (Functor h, Adjunction f g) => Lan f h a -> h (g a)Source

lanToComposedAdjoint and composedAdjointToLan witness the natural isomorphism between Lan f h and Compose h g given f -| g

 composedAdjointToLan . lanToComposedAdjointid
 lanToComposedAdjoint . composedAdjointToLanid