toRan and fromRan witness an adjunction from Compose[G,_,_] to Ran[G,_,_].
This is the natural transformation that defines a right Kan extension.
The universal property of a right Kan extension.
The universal property of a right Kan extension. The functor Ran[G,H,_] and the
natural transformation gran[G,H,_] are couniversal in the sense that for any
functor K and a natural transformation s from K[G[_]] to H, a unique
natural transformation toRan exists from K to Ran[G,H,_] such that
for all k, gran(toRan(k)) = s(k).