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

Copyright 2013 Edward Kmett and Dan Doel BSD Edward Kmett experimental rank N types Trustworthy Haskell98

Data.Functor.Kan.Lift

Contents

Description

Left Kan lifts for functors over Hask, wherever they exist.

http://ncatlab.org/nlab/show/Kan+lift

Synopsis

# Left Kan lifts

newtype Lift g f a Source

```f => g . Lift g f
(forall z. f => g . z) -> Lift g f => z -- couniversal```

Here we use the universal property directly as how we extract from our definition of `Lift`.

Constructors

 Lift FieldsrunLift :: forall z. Functor z => (forall x. f x -> g (z x)) -> z a

Instances

 Functor (Lift g h)

toLift :: Functor z => (forall a. f a -> g (z a)) -> Lift g f b -> z b Source

The universal property of `Lift`

fromLift :: Adjunction l u => (forall a. Lift u f a -> z a) -> f b -> u (z b) Source

When the adjunction exists

````fromLift` . `toLift` ≡ `id`
`toLift` . `fromLift` ≡ `id`
```

glift :: Adjunction l g => k a -> g (Lift g k a) Source

`f => g (`Lift` g f a)`

composeLift :: (Composition compose, Functor f, Functor g) => Lift f (Lift g h) a -> Lift (compose g f) h a Source

````composeLift` . `decomposeLift` = `id`
`decomposeLift` . `composeLift` = `id`
```

decomposeLift :: (Composition compose, Adjunction l g) => Lift (compose g f) h a -> Lift f (Lift g h) a Source

adjointToLift :: Adjunction f u => f a -> Lift u Identity a Source

`Lift u Identity a` is isomorphic to the left adjoint to `u` if one exists.

````adjointToLift` . `liftToAdjoint` ≡ `id`
`liftToAdjoint` . `adjointToLift` ≡ `id`
```

liftToAdjoint :: Adjunction f u => Lift u Identity a -> f a Source

`Lift u Identity a` is isomorphic to the left adjoint to `u` if one exists.

liftToComposedAdjoint :: (Adjunction f u, Functor h) => Lift u h a -> f (h a) Source

`Lift u h a` is isomorphic to the post-composition of the left adjoint of `u` onto `h` if such a left adjoint exists.

````liftToComposedAdjoint` . `composedAdjointToLift` ≡ `id`
`composedAdjointToLift` . `liftToComposedAdjoint` ≡ `id`
```

composedAdjointToLift :: Adjunction f u => f (h a) -> Lift u h a Source

`Lift u h a` is isomorphic to the post-composition of the left adjoint of `u` onto `h` if such a left adjoint exists.

repToLift :: Representable u => Rep u -> a -> Lift u Identity a Source

````repToLift` . `liftToRep` ≡ `id`
`liftToRep` . `repToLift` ≡ `id`
```

liftToComposedRep :: (Functor h, Representable u) => Lift u h a -> (Rep u, h a) Source

````liftToComposedRep` . `composedRepToLift` ≡ `id`
`composedRepToLift` . `liftToComposedRep` ≡ `id`
```

composedRepToLift :: Representable u => Rep u -> h a -> Lift u h a Source