A more general treatment of the Yoneda lemma than is given in Data.Functor.Yoneda.

Yoneda.hs

{-# LANGUAGE GHC2021, BlockArguments #-}

module Yoneda where

import Prelude hiding (id, (.), map)
import Control.Category


-- Preliminaries
class (Category c, Category d) => ExoFunctor c d f where
  map :: a `c` b -> f a `d` f b

type f  ~> g = forall x.   f x   -> g x
type c ~~> d = forall x y. c x y -> d x y


-- Covariant lemma
newtype Yoneda c f a = Yoneda{ unYoneda :: c a ~> f }

instance Category c => ExoFunctor c (->) (Yoneda c f) where
  map f = \y -> Yoneda \g -> unYoneda y (g . f)

toYoneda :: ExoFunctor c (->) f => f ~> Yoneda c f
toYoneda x = Yoneda (`map` x)

fromYoneda :: Category c => Yoneda c f ~> f
fromYoneda y = unYoneda y id


-- Covariant embedding
newtype Embed c a b = Embed{ unEmbed :: c b ~> c a }

instance Category (Embed c) where
  id = Embed id
  Embed f . Embed g = Embed (g . f)

embed :: Category c => c ~~> Embed c
embed c = Embed (. c)

debed :: Category c => Embed c ~~> c
debed e = unEmbed e id