Portability | GADTs, MPTCs, fundeps |
---|---|

Stability | provisional |

Maintainer | Edward Kmett <ekmett@gmail.com> |

Safe Haskell | Trustworthy |

Yoneda Reduction:

- data Yoneda f a where
- liftYoneda :: f a -> Yoneda f a
- lowerYoneda :: Functor f => Yoneda f a -> f a
- lowerM :: Monad f => Yoneda f a -> f a
- yonedaToLan :: Yoneda f a -> Lan Identity f a
- lanToYoneda :: Lan Identity f a -> Yoneda f a
- yonedaToLift :: Yoneda f a -> Lift Identity f a
- liftToYoneda :: Functor f => Lift Identity f a -> Yoneda f a

# Documentation

A form suitable for Yoneda reduction

liftYoneda :: f a -> Yoneda f aSource

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`

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

# 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`