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

Data.Functor.Coyoneda

Contents

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.

`Coyoneda f` is always a functor, even if `f` is not. In this case, it is called the free functor over `f`. Note the following categorical fine print: If `f` is not a functor, `Coyoneda f` is actually not the left Kan extension of `f` along the `Identity` functor, but along the inclusion functor from the discrete subcategory of Hask which contains only identity functions as morphisms to the full category Hask. (This is because `f`, not being a proper functor, can only be interpreted as a categorical functor by restricting the source category to only contain identities.)

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