Lan

trait Lan[G[_], H[_], A]

The left Kan extension of H along G

Companion
object
class Object
trait Matchable
class Any
Lan[G, H, A]

Type members

Types

type I

Value members

Abstract methods

def f(gi: G[I]): A
def v: H[I]

Concrete methods

def map[B](g: A => B): Lan[G, H, B]
def toAdjoint[F[_]](implicit H: Functor[H], A: Adjunction[G, F]): H[F[A]]

If G is left adjoint to F, there is a natural isomorphism between Lan[G,H,_] and H[F[_]]

If G is left adjoint to F, there is a natural isomorphism between Lan[G,H,_] and H[F[_]]

def toLan[F[_] : Functor](s: NaturalTransformation[H, [α] =>> F[G[α]]]): F[A]

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 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).