data-category-0.4.1: Category theory

Portabilitynon-portable
Stabilityexperimental
Maintainersjoerd@w3future.com

Data.Category.Yoneda

Description

 

Synopsis

Documentation

type YonedaEmbedding (~>) = Postcompose (Hom ~>) (Op ~>) :.: ToTuple2 ~> (Op ~>)Source

yonedaEmbedding :: Category ~> => YonedaEmbedding ~>Source

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

data Yoneda (~>) f Source

Constructors

Yoneda 

Instances

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

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

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

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

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