Data.Functor.Contravariant.Coyoneda

The co-Yoneda lemma for presheafs states that f is naturally isomorphic to Coyoneda f.

Documentation

data Coyoneda f a where

A Contravariant functor (aka presheaf) suitable for Yoneda reduction.

http://ncatlab.org/nlab/show/Yoneda+reduction

Constructors

Coyoneda :: (a -> b) -> f b -> Coyoneda f a

Instances

Contravariant (Coyoneda f)

Representable f => Representable (Coyoneda f)

Adjunction f g => Adjunction (Coyoneda f) (Coyoneda g)

liftCoyoneda :: f a -> Coyoneda f a

Coyoneda expansion of a presheaf

 liftCoyoneda . lowerCoyoneda ≡ id
 lowerCoyoneda . liftCoyoneda ≡ id

lowerCoyoneda :: Contravariant f => Coyoneda f a -> f a

Coyoneda reduction on a presheaf