Copyright | 2008-2016 Edward Kmett |
---|---|
License | BSD |
Maintainer | Edward Kmett <ekmett@gmail.com> |
Stability | experimental |
Portability | rank 2 types |
Safe Haskell | Safe |
Language | Haskell98 |
Left Kan Extensions
- data Lan g h a where
- toLan :: Functor f => (forall a. h a -> f (g a)) -> Lan g h b -> f b
- fromLan :: (forall a. Lan g h a -> f a) -> h b -> f (g b)
- glan :: h a -> Lan g h (g a)
- composeLan :: (Composition compose, Functor f) => Lan f (Lan g h) a -> Lan (compose f g) h a
- 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
- 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)
Left Kan Extensions
toLan :: Functor f => (forall a. h a -> f (g a)) -> Lan g h b -> f b #
The universal property of 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