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.Ran

Description

• Right Kan Extensions

Synopsis

# Documentation

newtype Ran g h a Source

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

We can define a right Kan extension in several ways. The definition here is obtained by reading off the definition in of a right Kan extension in terms of an End, but we can derive an equivalent definition from the universal property.

Given a `Functor` `h : C -> D` and a `Functor` `g : C -> C'`, we want to find extend `h` back along `g` to give `Ran g h : C' -> C`, such that the natural transformation `gran :: Ran g h (g a) -> h a` exists.

In some sense this is trying to approximate the inverse of `g` by using one of its adjoints, because if the adjoint and the inverse both exist, they match!

```Hask -h-> Hask
|       +
g      /
|    Ran g h
v    /

The Right Kan extension is unique (up to isomorphism) by taking this as its universal property.

That is to say given any `K : C' -> C` such that we have a natural transformation from `k.g` to `h` `(forall x. k (g x) -> h x)` there exists a canonical natural transformation from `k` to `Ran g h`. `(forall x. k x -> Ran g h x)`.

We could literally read this off as a valid Rank-3 definition for `Ran`:

```data Ran' g h a = forall z. `Functor` z => Ran' (forall x. z (g x) -> h x) (z a)
```

This definition is isomorphic the simpler Rank-2 definition we use below as witnessed by the

```ranIso1 :: Ran g f x -> Ran' g f x
ranIso1 (Ran e) = Ran' e id
```
```ranIso2 :: Ran' g f x -> Ran g f x
ranIso2 (Ran' h z) = Ran \$ \k -> h (k <\$> z)
```
```ranIso2 (ranIso1 (Ran e)) ≡ -- by definition
ranIso2 (Ran' e id) ≡       -- by definition
Ran \$ \k -> e (k <\$> id)    -- by definition
Ran \$ \k -> e (k . id)      -- f . id = f
Ran \$ \k -> e k             -- eta reduction
Ran e
```

The other direction is left as an exercise for the reader.

Constructors

 Ran FieldsrunRan :: forall b. (a -> g b) -> h b

Instances

 Functor (Ran g h)

toRan :: Functor k => (forall a. k (g a) -> h a) -> k b -> Ran g h b Source

The universal property of a right Kan extension.

fromRan :: (forall a. k a -> Ran g h a) -> k (g b) -> h b Source

`toRan` and `fromRan` witness a higher kinded adjunction. from `(`'Compose'` g)` to `Ran g`

````toRan` . `fromRan` ≡ `id`
`fromRan` . `toRan` ≡ `id`
```

gran :: Ran g h (g a) -> h a Source

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

composeRan :: Composition compose => Ran f (Ran g h) a -> Ran (compose f g) h a Source

````composeRan` . `decomposeRan` ≡ `id`
`decomposeRan` . `composeRan` ≡ `id`
```

decomposeRan :: (Composition compose, Functor f) => Ran (compose f g) h a -> Ran f (Ran g h) a Source

adjointToRan :: Adjunction f g => f a -> Ran g Identity a Source

````adjointToRan` . `ranToAdjoint` ≡ `id`
`ranToAdjoint` . `adjointToRan` ≡ `id`
```

composedAdjointToRan :: (Adjunction f g, Functor h) => h (f a) -> Ran g h a Source

ranToComposedAdjoint :: Adjunction f g => Ran g h a -> h (f a) Source

````composedAdjointToRan` . `ranToComposedAdjoint` ≡ `id`
`ranToComposedAdjoint` . `composedAdjointToRan` ≡ `id`
```

composedRepToRan :: (Representable u, Functor h) => h (Rep u, a) -> Ran u h a Source

ranToComposedRep :: Representable u => Ran u h a -> h (Rep u, a) Source