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

Portability MPTCs, fundeps provisional Edward Kmett Trustworthy

Data.Functor.Yoneda

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

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 FieldsrunYoneda :: forall b. (a -> b) -> f b

Instances

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