kan-extensions-3.6.2: 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 co-Yoneda lemma states that

`f a` is isomorphic to `(forall r. (a -> r) -> f a)`

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

Synopsis

# Documentation

newtype Yoneda f a Source

Constructors

 Yoneda FieldsrunYoneda :: forall b. (a -> b) -> f b

Instances

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

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` is the right Kan extension of `f` along the `Identity` functor.

``` `yonedaToRan` . `ranToYoneda` ≡ `id`
`ranToYoneda` . `yonedaToRan` ≡ `id`
```

# as a right Kan lift

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

`Yoneda f` is the right Kan lift of `f` along the `Identity` functor.

``` `yonedaToRift` . `riftToYoneda` ≡ `id`
`riftToYoneda` . `yonedaToRift` ≡ `id`
```