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

Portability non-portable (GADTs, MPTCs) experimental Edward Kmett Trustworthy

Description

The `Density` `Comonad` for a `Functor` (aka the 'Comonad generated by a `Functor`) The `Density` term dates back to Dubuc''s 1974 thesis. The term `Monad` genererated by a `Functor` dates back to 1972 in Street''s ''Formal Theory of Monads''.

The left Kan extension of a `Functor` along itself (`Lan f f`) forms a `Comonad`. This is that `Comonad`.

Synopsis

# Documentation

data Density k a whereSource

Constructors

 Density :: (k b -> a) -> k b -> Density k a

Instances

 ComonadTrans Density Functor (Density f) Applicative f => Applicative (Density f) Comonad (Density f) Apply f => Apply (Density f) Extend (Density f)

liftDensity :: Comonad w => w a -> Density w aSource

The natural transformation from a `Comonad w` to the `Comonad` generated by `w` (forwards).

This is merely a right-inverse (section) of `lower`, rather than a full inverse.

``` `lower` . `liftDensity` ≡ `id`
```

densityToAdjunction :: Adjunction f g => Density f a -> f (g a)Source

The Density `Comonad` of a left adjoint is isomorphic to the `Comonad` formed by that `Adjunction`.

This isomorphism is witnessed by `densityToAdjunction` and `adjunctionToDensity`.

``` `densityToAdjunction` . `adjunctionToDensity` ≡ `id`
`adjunctionToDensity` . `densityToAdjunction` ≡ `id`
```

lanToDensity :: Lan f f a -> Density f aSource

The `Density` `Comonad` of a `Functor` `f` is obtained by taking the left Kan extension (`Lan`) of `f` along itself. This isomorphism is witnessed by `lanToDensity` and `densityToLan`

``` `lanToDensity` . `densityToLan` ≡ `id`
`densityToLan` . `lanToDensity` ≡ `id`
```