kan-extensions-5.2.6: Kan extensions, Kan lifts, the Yoneda lemma, and (co)density (co)monads
Copyright2008-2016 Edward Kmett
LicenseBSD
MaintainerEdward Kmett <ekmett@gmail.com>
Stabilityexperimental
Portabilityrank 2 types
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Functor.Kan.Lan

Description

Left Kan Extensions

Synopsis

Left Kan Extensions

data Lan (g :: k -> Type) (h :: k -> Type) a where Source #

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

Constructors

Lan :: forall {k} (g :: k -> Type) (b :: k) a (h :: k -> Type). (g b -> a) -> h b -> Lan g h a 

Instances

Instances details
(Functor g, Applicative h) => Applicative (Lan g h) Source # 
Instance details

Defined in Data.Functor.Kan.Lan

Methods

pure :: a -> Lan g h a #

(<*>) :: Lan g h (a -> b) -> Lan g h a -> Lan g h b #

liftA2 :: (a -> b -> c) -> Lan g h a -> Lan g h b -> Lan g h c #

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

(<*) :: Lan g h a -> Lan g h b -> Lan g h a #

Functor (Lan f g) Source # 
Instance details

Defined in Data.Functor.Kan.Lan

Methods

fmap :: (a -> b) -> Lan f g a -> Lan f g b #

(<$) :: a -> Lan f g b -> Lan f g a #

(Functor g, Apply h) => Apply (Lan g h) Source # 
Instance details

Defined in Data.Functor.Kan.Lan

Methods

(<.>) :: Lan g h (a -> b) -> Lan g h a -> Lan g h b #

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

(<.) :: Lan g h a -> Lan g h b -> Lan g h a #

liftF2 :: (a -> b -> c) -> Lan g h a -> Lan g h b -> Lan g h c #

toLan :: forall {k} f h g b. Functor f => (forall (a :: k). h a -> f (g a)) -> Lan g h b -> f b Source #

The universal property of a left Kan extension.

fromLan :: forall {k} g h f (b :: k). (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 :: forall {k} h (a :: k) g. h a -> Lan g h (g a) Source #

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

composeLan :: forall (compose :: (Type -> Type) -> (Type -> Type) -> Type -> Type) (f :: Type -> Type) (g :: Type -> Type) (h :: Type -> Type) a. (Composition compose, Functor f) => Lan f (Lan g h) a -> Lan (compose f g) h a Source #

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

composeLan . decomposeLanid
decomposeLan . composeLanid

decomposeLan :: forall (compose :: (Type -> Type) -> (Type -> Type) -> Type -> Type) (f :: Type -> Type) (g :: Type -> Type) (h :: Type -> Type) a. Composition compose => Lan (compose f g) h a -> Lan f (Lan g h) a Source #

adjointToLan :: forall (f :: Type -> Type) g a. Adjunction f g => g a -> Lan f Identity a Source #

lanToAdjoint :: forall (f :: Type -> Type) g a. Adjunction f g => Lan f Identity a -> g a Source #

composedAdjointToLan :: forall (f :: Type -> Type) g h a. Adjunction f g => h (g a) -> Lan f h a Source #

lanToComposedAdjoint :: forall h (f :: Type -> Type) g a. (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