kan-extensions-4.0.3: 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` . `lowerYoneda` ≡ `id`
`lowerYoneda` . `liftYoneda` ≡ `id`
```
``` 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` . `ranToYoneda` ≡ `id`
`ranToYoneda` . `yonedaToRan` ≡ `id`
```

# 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` . `riftToYoneda` ≡ `id`
`riftToYoneda` . `yonedaToRift` ≡ `id`
```