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

Portability GADTs, MPTCs, fundeps provisional Edward Kmett Trustworthy

Data.Functor.Yoneda.Reduction

Description

Yoneda Reduction:

`Yoneda f` is isomorphic to `Lan f Identity`

Synopsis

Documentation

data Yoneda f a whereSource

A form suitable for Yoneda reduction

Constructors

 Yoneda :: (b -> a) -> f b -> Yoneda f a

Instances

liftYoneda :: f a -> Yoneda f aSource

Yoneda expansion

``` `liftYoneda` . `lowerYoneda` ≡ `id`
`lowerYoneda` . `liftYoneda` ≡ `id`
```
``` `lift` = `liftYoneda`
```

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

Yoneda reduction

``` `lower` = `lowerM` = `lowerYoneda`
```

lowerM :: Monad f => Yoneda f a -> f aSource

Yoneda reduction given a `Monad`.

``` `lower` = `lowerM` = `lowerYoneda`
```

as a Left Kan extension

yonedaToLan :: Yoneda f a -> Lan Identity f aSource

`Yoneda f` is the left Kan extension of `f` along the `Identity` functor.

``` `yonedaToLan` . `lanToYoneda` ≡ `id`
`lanToYoneda` . `yonedaToLan` ≡ `id`
```

as a Left Kan lift

yonedaToLift :: Yoneda f a -> Lift Identity f aSource

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

``` `yonedaToLift` . `liftToYoneda` ≡ `id`
`liftToYoneda` . `yonedaToLift` ≡ `id`
```