kan-extensions-5.2.5: Kan extensions, Kan lifts, the Yoneda lemma, and (co)density (co)monads
Copyright 2008-2016 Edward Kmett
License BSD
Maintainer Edward Kmett <ekmett@gmail.com>
Stability experimental
Portability rank 2 types
Safe Haskell Safe-Inferred
Language Haskell2010

Data.Functor.Kan.Lan

Description

Left Kan Extensions

Synopsis

Left Kan Extensions

data Lan g h a where Source #

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

Constructors

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

Instances

Instances details
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 Source #

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

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

Defined in Data.Functor.Kan.Lan

Methods

pure :: a -> Lan g h a Source #

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

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

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

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

( 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 Source #

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

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

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

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

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 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 :: Composition compose => Lan (compose f g) h a -> Lan f ( Lan g h) a Source #

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