Representable (Lan f g)

[Icelandjack]

I spotted this on ncatlab

Proposition 4.1. For F:C→D a 𝒱-enriched functor between small 𝒱-enriched categories we have

1. the left Kan extension along F takes representable presheaves C(c,−):C→𝒱 to their image under F:

Lan FC(c,−)≃D(F(c),−)

for all c ∈ C.

An in Haskell this translates (roughly) to a Representableinstance for Lan:

instance (Functor f, Representable g) => Distributive (Lan f g) where
  distribute :: Functor h => h (Lan f g a) -> Lan f g (h a)
  distribute = distributeRep

instance (Functor f, Representable g) => Representable (Lan f g) where
  type Rep (Lan f g) = f (Rep g)

  index :: Lan f g a -> (f (Rep g) -> a)
  index (Lan f g) = f . fmap (index g)

  tabulate :: (f (Rep g) -> a) -> Lan f g a
  tabulate = (`Lan` tabulate id)

I noticed it was missing from the library.

[RyanGlScott]

Those feel like reasonable additions to the library.

Out of curiosity, does the Distributive instance need a full Representable g constraint? Or would Distributive g suffice, assuming that you rewrote the implementation accordingly?

[Icelandjack]

No I wasn't able to come up with it but I fully expect that the constraint can be weakened. I also wasn't able to determine if a dual case exists for Ran.