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 Source

The universal property of a left Kan extension.

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`

.`decomposeLan`

≡`id`

`decomposeLan`

.`composeLan`

≡`id`

decomposeLan :: Composition compose => Lan (compose f g) h a -> Lan f (Lan g h) a Source

adjointToLan :: Adjunction f g => g a -> Lan f Identity a Source

`adjointToLan`

.`lanToAdjoint`

≡`id`

`lanToAdjoint`

.`adjointToLan`

≡`id`

lanToAdjoint :: Adjunction f g => Lan f Identity a -> g a Source

composedAdjointToLan :: Adjunction f g => h (g a) -> Lan f 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`

.`lanToComposedAdjoint`

≡`id`

`lanToComposedAdjoint`

.`composedAdjointToLan`

≡`id`