Control.Functor.KanExtension
 Portability non-portable (rank-2 polymorphism) Stability experimental Maintainer Edward Kmett
 Contents Right Kan Extensions Left Kan Extensions
Description

Left and right Kan extensions, expressed as higher order functors

NB: Yoneda, CoYoneda, Density, Codensity have been factored out into separate modules.

Synopsis
newtype Ran g h a = Ran {
 runRan :: forall b. (a -> g b) -> h b
}
toRan :: (Composition o, Functor k) => ((k `o` g) :~> h) -> k :~> Ran g h
fromRan :: Composition o => (k :~> Ran g h) -> (k `o` g) :~> h
ranToComposedAdjoint :: (Composition o, Adjunction f g) => Ran g h :~> (h `o` f)
composedAdjointToRan :: (Functor h, Composition o, Adjunction f g) => (h `o` f) :~> Ran g h
composeRan :: Composition o => Ran f (Ran g h) :~> Ran (f `o` g) h
decomposeRan :: (Functor f, Composition o) => Ran (f `o` g) h :~> Ran f (Ran g h)
data Lan g h a = forall b . Lan (g b -> a) (h b)
toLan :: (Composition o, Functor f) => (h :~> (f `o` g)) -> Lan g h :~> f
fromLan :: Composition o => (Lan g h :~> f) -> h :~> (f `o` g)
composeLan :: (Functor f, Composition o) => Lan f (Lan g h) :~> Lan (f `o` g) h
decomposeLan :: Composition o => Lan (f `o` g) h :~> Lan f (Lan g h)
lanToComposedAdjoint :: (Functor h, Composition o, Adjunction f g) => Lan f h :~> (h `o` g)
composedAdjointToLan :: (Composition o, Adjunction f g) => (h `o` g) :~> Lan f h
Right Kan Extensions
newtype Ran g h a

The right Kan Extension of h along g. An alternative definition in terms of Ends.

`newtype RanT g h a b b' { (a -> g b) -> h b' }`
`type Ran g h a = End (RanT g h a)`
Constructors
Ran
 runRan :: forall b. (a -> g b) -> h b Instances
 HFunctor (Ran g) Functor (Ran g h)
toRan :: (Composition o, Functor k) => ((k `o` g) :~> h) -> k :~> Ran g h
Nat(k o g, h) is isomorphic to Nat(k, Ran g h) (forwards)
fromRan :: Composition o => (k :~> Ran g h) -> (k `o` g) :~> h
Nat(k o g, h) is isomorphic to Nat(k, Ran g h) (backwards)
f -| g iff Ran g Identity exists (forward)
f -| g iff Ran g Identity exists (backwards)
ranToComposedAdjoint :: (Composition o, Adjunction f g) => Ran g h :~> (h `o` f)
composedAdjointToRan :: (Functor h, Composition o, Adjunction f g) => (h `o` f) :~> Ran g h
composeRan :: Composition o => Ran f (Ran g h) :~> Ran (f `o` g) h
The natural isomorphism from Ran f (Ran g h) to Ran (f o g) h (forwards)
decomposeRan :: (Functor f, Composition o) => Ran (f `o` g) h :~> Ran f (Ran g h)
The natural isomorphism from Ran f (Ran g h) to Ran (f o g) h (backwards)
Left Kan Extensions
data Lan g h a

Left Kan Extension

`newtype LanT g h a b b' { (g b -> a, h b') }`
`type Lan g h a = Coend (LanT g h a)`
Constructors
 forall b . Lan (g b -> a) (h b) Instances
 Functor g => HFunctor (Lan g) Functor (Lan f g)
toLan :: (Composition o, Functor f) => (h :~> (f `o` g)) -> Lan g h :~> f
Nat(h, f.g) is isomorphic to Nat (Lan g h, f) (forwards)
fromLan :: Composition o => (Lan g h :~> f) -> h :~> (f `o` g)
Nat(h, f.g) is isomorphic to Nat (Lan g h, f) (backwards)