If G is left adjoint to F, there is a natural isomorphism between
Lan[G,H,_] and H[F[_]]
The universal property of a left Kan extension.
The universal property of a left Kan extension. The functor Lan[G,H,_] and the
natural transformation glan[G,H,_] are universal in the sense that for any
functor F and a natural transformation s from H to F[G[_]], a unique
natural transformation toLan exists from Lan[G,H,_] to F such that
for all h, glan(h).toLan = s(h).
The left Kan extension of
HalongG