search

ekmett / kan-extensions

Kan extensions, Kan lifts, the Yoneda lemma, and (co)monads generated by a functor
Other
78 stars 33 forks source link

Representable (Lan f g) #80

Open Icelandjack opened 6 months ago

Icelandjack commented 6 months ago

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 commented 6 months ago

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 commented 6 months ago

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.