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

Copyright 2008-2013 Edward Kmett BSD Edward Kmett experimental rank 2 types Trustworthy Haskell98

Data.Functor.Kan.Lan

Contents

Description

Left Kan Extensions

Synopsis

# Left Kan Extensions

data Lan g h a where Source

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

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

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

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

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

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

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