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

Portability rank 2 types experimental Edward Kmett Trustworthy

Data.Functor.Kan.Lan

Contents

Description

Left Kan Extensions

Synopsis

Left Kan Extensions

data Lan g h a whereSource

The left Kan extension of a `Functor` `h` along a `Functor` `g`.

Constructors

 Lan :: (g b -> a) -> h b -> Lan g h a

Instances

 Functor (Lan f g) (Functor g, Applicative h) => Applicative (Lan g h) (Functor g, Apply h) => Apply (Lan g h)

toLan :: Functor f => (forall a. h a -> f (g a)) -> Lan g h b -> f bSource

The universal property of a left Kan extension.

fromLan :: (forall a. Lan g h a -> f a) -> h b -> f (g b)Source

`fromLan` and `toLan` witness a (higher kinded) adjunction between `Lan g` and `(Compose g)`

``` `toLan` . `fromLan` ≡ `id`
`fromLan` . `toLan` ≡ `id`
```

glan :: h a -> Lan g h (g a)Source

This is the natural transformation that defines a Left Kan extension.

composeLan :: (Composition compose, Functor f) => Lan f (Lan g h) a -> Lan (compose f g) h aSource

`composeLan` and `decomposeLan` witness the natural isomorphism from `Lan f (Lan g h)` and `Lan (f o g) h`

``` `composeLan` . `decomposeLan` ≡ `id`
`decomposeLan` . `composeLan` ≡ `id`
```

decomposeLan :: Composition compose => Lan (compose f g) h a -> Lan f (Lan g h) aSource

adjointToLan :: Adjunction f g => g a -> Lan f Identity aSource

``` `adjointToLan` . `lanToAdjoint` ≡ `id`
`lanToAdjoint` . `adjointToLan` ≡ `id`
```

composedAdjointToLan :: Adjunction f g => h (g a) -> Lan f h aSource

lanToComposedAdjoint :: (Functor h, Adjunction f g) => Lan f h a -> h (g a)Source

`lanToComposedAdjoint` and `composedAdjointToLan` witness the natural isomorphism between `Lan f h` and `Compose h g` given `f -| g`

``` `composedAdjointToLan` . `lanToComposedAdjoint` ≡ `id`
`lanToComposedAdjoint` . `composedAdjointToLan` ≡ `id`
```