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

Copyright 2008-2016 Edward Kmett BSD Edward Kmett experimental rank 2 types Safe Haskell98

Data.Functor.Kan.Lan

Contents

Description

Left Kan Extensions

Synopsis

# Left Kan Extensions

data Lan g h a where #

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) # Instance detailsDefined in Data.Functor.Kan.Lan Methodsfmap :: (a -> b) -> Lan f g a -> Lan f g b #(<\$) :: a -> Lan f g b -> Lan f g a # (Functor g, Applicative h) => Applicative (Lan g h) # Instance detailsDefined in Data.Functor.Kan.Lan Methodspure :: 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 g, Apply h) => Apply (Lan g h) # Instance detailsDefined 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 :: Functor f => (forall a. h a -> f (g a)) -> Lan g h b -> f b #

The universal property of a left Kan extension.

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

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

toLan . fromLan ≡ id
fromLan . toLan ≡ id


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

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 a #

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

composeLan . decomposeLan ≡ id
decomposeLan . composeLan ≡ id


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

adjointToLan :: Adjunction f g => g a -> Lan f Identity a #

adjointToLan . lanToAdjoint ≡ id
lanToAdjoint . adjointToLan ≡ id


lanToAdjoint :: Adjunction f g => Lan f Identity a -> g a #

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

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

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

composedAdjointToLan . lanToComposedAdjoint ≡ id
lanToComposedAdjoint . composedAdjointToLan ≡ id