kan-extensions-3.7: Kan extensions, Kan lifts, various forms of the Yoneda lemma, and (co)density (co)monads

PortabilityMPTCs, fundeps
Stabilityprovisional
MaintainerEdward Kmett <ekmett@gmail.com>
Safe HaskellTrustworthy

Data.Functor.Yoneda

Contents

Description

The covariant form of the Yoneda lemma states that f is naturally isomorphic to Yoneda f.

This is described in a rather intuitive fashion by Dan Piponi in

http://blog.sigfpe.com/2006/11/yoneda-lemma.html

Synopsis

Documentation

newtype Yoneda f a Source

Yoneda f a can be viewed as the partial application of fmap to its second argument.

Constructors

Yoneda 

Fields

runYoneda :: forall b. (a -> b) -> f b
 

liftYoneda :: Functor f => f a -> Yoneda f aSource

The natural isomorphism between f and Yoneda f given by the Yoneda lemma is witnessed by liftYoneda and lowerYoneda

 liftYoneda . lowerYonedaid
 lowerYoneda . liftYonedaid
 lowerYoneda (liftYoneda fa) =         -- definition
 lowerYoneda (Yoneda (f -> fmap f a)) -- definition
 (f -> fmap f fa) id                  -- beta reduction
 fmap id fa                            -- functor law
 fa
 lift = liftYoneda

maxF :: (Functor f, Ord (f a)) => Yoneda f a -> Yoneda f a -> Yoneda f aSource

minF :: (Functor f, Ord (f a)) => Yoneda f a -> Yoneda f a -> Yoneda f aSource

maxM :: (Monad m, Ord (m a)) => Yoneda m a -> Yoneda m a -> Yoneda m aSource

minM :: (Monad m, Ord (m a)) => Yoneda m a -> Yoneda m a -> Yoneda m aSource

as a right Kan extension

yonedaToRan :: Yoneda f a -> Ran Identity f aSource

Yoneda f can be viewed as the right Kan extension of f along the Identity functor.

 yonedaToRan . ranToYonedaid
 ranToYoneda . yonedaToRanid

as a right Kan lift

yonedaToRift :: Yoneda f a -> Rift Identity f aSource

Yoneda f can be viewed as the right Kan lift of f along the Identity functor.

 yonedaToRift . riftToYonedaid
 riftToYoneda . yonedaToRiftid