Modulekan-extensions-5.2.7Haskell2010

Data.Functor.Contravariant.Coyoneda

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

datadata Coyoneda (f :: Type -> Type) a where

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

Instances4Contravariant, Representable, Adjunction, Rep

Contravariant (Coyoneda f)Defined in kan-extensions-5.2.7 · Data.Functor.Contravariant.Coyoneda
Representable f => Representable (Coyoneda f)Defined in kan-extensions-5.2.7 · Data.Functor.Contravariant.Coyoneda
Adjunction f g => Adjunction (Coyoneda f) (Coyoneda g)Defined in kan-extensions-5.2.7 · Data.Functor.Contravariant.Coyoneda
type Rep (Coyoneda f) = Rep fDefined in kan-extensions-5.2.7 · Data.Functor.Contravariant.Coyoneda

valueliftCoyoneda :: f a -> Coyoneda f a

Coyoneda "expansion" of a presheaf

liftCoyoneda . lowerCoyoneda ≡ id
lowerCoyoneda . liftCoyoneda ≡ id

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

Coyoneda reduction on a presheaf

valuehoistCoyoneda :: (forall a. f a -> g a) -> Coyoneda f b -> Coyoneda g b

Lift a natural transformation from f to g to a natural transformation from Coyoneda f to Coyoneda g.