Data.Functor.Kan.Lift

Left Kan lifts for functors over Hask, wherever they exist.

http://ncatlab.org/nlab/show/Kan+lift

Left Kan lifts

newtype Lift g f a

 f => g . Lift g f
 (forall z. f => g . z) -> Lift g f => z -- couniversal

Here we use the universal property directly as how we extract from our definition of Lift.

Constructors

Lift

Fields

runLift :: forall z. Functor z => (forall x. f x -> g (z x)) -> z a

Instances

Functor (Lift g h)

(Functor g, ~ (* -> *) g h) => Copointed (Lift g h)

toLift :: Functor z => (forall a. f a -> g (z a)) -> Lift g f b -> z b

The universal property of Lift

fromLift :: Adjunction l u => (forall a. Lift u f a -> z a) -> f b -> u (z b)

When the adjunction exists

 fromLift . toLift ≡ id
 toLift . fromLift ≡ id

glift :: Adjunction l g => k a -> g (Lift g k a)

f => g (Lift g f a)

composeLift :: (Composition compose, Functor f, Functor g) => Lift f (Lift g h) a -> Lift (compose g f) h a

 composeLift . decomposeLift = id
 decomposeLift . composeLift = id

decomposeLift :: (Composition compose, Adjunction l g) => Lift (compose g f) h a -> Lift f (Lift g h) a

adjointToLift :: Adjunction f u => f a -> Lift u Identity a

Lift u Identity a is isomorphic to the left adjoint to u if one exists.

 adjointToLift . liftToAdjoint ≡ id
 liftToAdjoint . adjointToLift ≡ id

liftToAdjoint :: Adjunction f u => Lift u Identity a -> f a

Lift u Identity a is isomorphic to the left adjoint to u if one exists.

liftToComposedAdjoint :: (Adjunction f u, Functor h) => Lift u h a -> f (h a)

Lift u h a is isomorphic to the post-composition of the left adjoint of u onto h if such a left adjoint exists.

 liftToComposedAdjoint . composedAdjointToLift ≡ id
 composedAdjointToLift . liftToComposedAdjoint ≡ id

composedAdjointToLift :: Adjunction f u => f (h a) -> Lift u h a

Lift u h a is isomorphic to the post-composition of the left adjoint of u onto h if such a left adjoint exists.

repToLift :: Representable u => Key u -> a -> Lift u Identity a

 repToLift . liftToRep ≡ id
 liftToRep . repToLift ≡ id

liftToRep :: Representable u => Lift u Identity a -> (Key u, a)

liftToComposedRep :: (Functor h, Representable u) => Lift u h a -> (Key u, h a)

 liftToComposedRep . composedRepToLift ≡ id
 composedRepToLift . liftToComposedRep ≡ id

composedRepToLift :: Representable u => Key u -> h a -> Lift u h a