kan-extensions-4.0.1: 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.Coyoneda

Description

The co-Yoneda lemma for a covariant `Functor` `f` states that `Coyoneda f` is naturally isomorphic to `f`.

Synopsis

# Documentation

data Coyoneda f a whereSource

A covariant `Functor` suitable for Yoneda reduction

Constructors

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

Instances

liftCoyoneda :: f a -> Coyoneda f aSource

Yoneda expansion

``` `liftCoyoneda` . `lowerCoyoneda` ≡ `id`
`lowerCoyoneda` . `liftCoyoneda` ≡ `id`
```
``` lowerCoyoneda (liftCoyoneda fa) = -- by definition
lowerCoyoneda (Coyoneda id fa)  = -- by definition
fmap id fa                      = -- functor law
fa
```
``` `lift` = `liftCoyoneda`
```

lowerCoyoneda :: Functor f => Coyoneda f a -> f aSource

Yoneda reduction lets us walk under the existential and apply `fmap`.

Mnemonically, "Yoneda reduction" sounds like and works a bit like β-reduction.

You can view `Coyoneda` as just the arguments to `fmap` tupled up.

``` `lower` = `lowerM` = `lowerCoyoneda`
```

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

Yoneda reduction given a `Monad` lets us walk under the existential and apply `liftM`.

You can view `Coyoneda` as just the arguments to `liftM` tupled up.

``` `lower` = `lowerM` = `lowerCoyoneda`
```

# as a Left Kan extension

coyonedaToLan :: Coyoneda f a -> Lan Identity f aSource

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

``` `coyonedaToLan` . `lanToCoyoneda` ≡ `id`
`lanToCoyoneda` . `coyonedaToLan` ≡ `id`
```

# as a Left Kan lift

coyonedaToLift :: Coyoneda f a -> Lift Identity f aSource

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

``` `coyonedaToLift` . `liftToCoyoneda` ≡ `id`
`liftToCoyoneda` . `coyonedaToLift` ≡ `id`
```