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

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 where Source

A covariant `Functor` suitable for Yoneda reduction

Constructors

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

Instances

liftCoyoneda :: f a -> Coyoneda f a Source

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 a Source

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

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

http://ncatlab.org/nlab/show/Yoneda+reduction

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

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

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

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 a Source

`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 a Source

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

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