Modulekan-extensions-5.2.7Haskell2010

Data.Functor.Kan.Lan

Left Kan Extensions

Left Kan Extensions

10 declarations

datadata Lan (g :: k -> Type) (h :: k -> Type) a where

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

Instances3Functor, Applicative, Apply

Functor (Lan f g)Defined in kan-extensions-5.2.7 · Data.Functor.Kan.Lan
(Functor g, Applicative h) => Applicative (Lan g h)Defined in kan-extensions-5.2.7 · Data.Functor.Kan.Lan
(Functor g, Apply h) => Apply (Lan g h)Defined in kan-extensions-5.2.7 · Data.Functor.Kan.Lan

valuetoLan :: Functor f => (forall (a :: k). h a -> f (g a)) -> Lan g h b -> f b

The universal property of a left Kan extension.

valuefromLan :: (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

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

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

valuecomposeLan

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

valuedecomposeLan

valueadjointToLan :: Adjunction f g => g a -> Lan f Identity a

adjointToLan . lanToAdjoint ≡ id
lanToAdjoint . adjointToLan ≡ id

valuelanToAdjoint :: Adjunction f g => Lan f Identity a -> g a

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

valuelanToComposedAdjoint :: (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