| Copyright | 2013 Edward Kmett and Dan Doel |
|---|---|
| License | BSD |
| Maintainer | Edward Kmett <ekmett@gmail.com> |
| Stability | experimental |
| Portability | rank N types |
| Safe Haskell | Trustworthy |
| Language | Haskell98 |
Data.Functor.Kan.Lift
Contents
Description
Left Kan lifts for functors over Hask, wherever they exist.
- newtype Lift g f a = Lift {}
- toLift :: Functor z => (forall a. f a -> g (z a)) -> Lift g f b -> z b
- fromLift :: Adjunction l u => (forall a. Lift u f a -> z a) -> f b -> u (z b)
- glift :: Adjunction l g => k a -> g (Lift g k a)
- composeLift :: (Composition compose, Functor f, Functor g) => Lift f (Lift g h) a -> Lift (compose g f) h a
- 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
- liftToAdjoint :: Adjunction f u => Lift u Identity a -> f a
- liftToComposedAdjoint :: (Adjunction f u, Functor h) => Lift u h a -> f (h a)
- composedAdjointToLift :: Adjunction f u => f (h a) -> Lift u h a
- repToLift :: Representable u => Rep u -> a -> Lift u Identity a
- liftToRep :: Representable u => Lift u Identity a -> (Rep u, a)
- liftToComposedRep :: (Functor h, Representable u) => Lift u h a -> (Rep u, h a)
- composedRepToLift :: Representable u => Rep u -> h a -> Lift u h a
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.
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)
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=iddecomposeLift.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≡idliftToAdjoint.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≡idcomposedAdjointToLift.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 => Rep u -> a -> Lift u Identity a
liftToRep :: Representable u => Lift u Identity a -> (Rep u, a)
liftToComposedRep :: (Functor h, Representable u) => Lift u h a -> (Rep u, h a)
composedRepToLift :: Representable u => Rep u -> h a -> Lift u h a