Data.Category.Yoneda

Documentation

type YonedaEmbedding k = Postcompose (Hom k) (Op k) :.: (Postcompose (Swap k (Op k)) (Op k) :.: Tuple k (Op k))

yonedaEmbedding :: Category k => YonedaEmbedding k

The Yoneda embedding functor, C -> Set^(C^op).

data Yoneda k f

Constructors

Yoneda

Instances

(Category k, Functor f, ~ (* -> * -> *) (Dom f) (Op k), ~ (* -> * -> *) (Cod f) (->)) => Functor (Yoneda k f)

Yoneda converts a functor f into a natural transformation from the hom functor to f.

fromYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Yoneda k f :~> f

fromYoneda and toYoneda are together the isomophism from the Yoneda lemma.

toYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> f :~> Yoneda k f