module Data.Category.Yoneda where
import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
import Data.Category.CartesianClosed
type YonedaEmbedding k = Postcompose (Hom k) (Op k) :.: ToTuple2 k (Op k)
yonedaEmbedding :: Category k => YonedaEmbedding k
yonedaEmbedding = Postcompose Hom :.: ToTuple2
data Yoneda (k :: * -> * -> *) f = Yoneda
type instance Dom (Yoneda k f) = Op k
type instance Cod (Yoneda k f) = (->)
type instance Yoneda k f :% a = Nat (Op k) (->) (k :-*: a) f
instance (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => Functor (Yoneda k f) where
Yoneda % Op ab = \n -> n . yonedaEmbedding % ab
fromYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Yoneda k f :~> f
fromYoneda f = Nat Yoneda f (\(Op a) n -> (n ! Op a) a)
toYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> f :~> Yoneda k f
toYoneda f = Nat f Yoneda (\(Op a) fa -> Nat (hom_X a) f (\_ h -> (f % Op h) fa))