kan-extensions- Kan extensions, the Yoneda lemma, and (co)density (co)monads

Portabilityrank 2 types
MaintainerEdward Kmett <ekmett@gmail.com>






newtype Ran g h a Source




runRan :: forall b. (a -> g b) -> h b


Functor (Ran g h) 

toRan :: (Composition compose, Functor k) => (forall a. compose k g a -> h a) -> k b -> Ran g h bSource

toRan and fromRan witness a higher kinded adjunction. from (`'Compose'` g) to Ran g

fromRan :: Composition compose => (forall a. k a -> Ran g h a) -> compose k g b -> h bSource

composeRan :: Composition compose => Ran f (Ran g h) a -> Ran (compose f g) h aSource

decomposeRan :: (Composition compose, Functor f) => Ran (compose f g) h a -> Ran f (Ran g h) aSource

ranToComposedAdjoint :: (Composition compose, Adjunction f g) => Ran g h a -> compose h f aSource

composedAdjointToRan :: (Composition compose, Adjunction f g, Functor h) => compose h f a -> Ran g h aSource

data Lan g h a whereSource


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


Functor (Lan f g) 

toLan :: (Composition compose, Functor f) => (forall a. h a -> compose f g a) -> Lan g h b -> f bSource

fromLan :: Composition compose => (forall a. Lan g h a -> f a) -> h b -> compose f g bSource

lanToComposedAdjoint :: (Composition compose, Functor h, Adjunction f g) => Lan f h a -> compose h g aSource

lanToComposedAdjoint and composedAdjointToLan witness the natural isomorphism between Lan f h and Compose h g given f -| g

composedAdjointToLan :: Composition compose => Adjunction f g => compose h g a -> Lan f h aSource

composeLan :: (Composition compose, Functor f) => Lan f (Lan g h) a -> Lan (compose f g) h aSource

composeLan and decomposeLan witness the natural isomorphism from Lan f (Lan g h) and Lan (f o g) h

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