kan-extensions-5.2.5: Kan extensions, Kan lifts, the Yoneda lemma, and (co)density (co)monads
Copyright 2008-2016 Edward Kmett
License BSD
Maintainer Edward Kmett <ekmett@gmail.com>
Stability experimental
Portability rank 2 types
Safe Haskell Trustworthy
Language Haskell2010

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 extend h back along g to give Ran g h : C' -> D , 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    /
Hask -'

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

That is to say given any K : C' -> D 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

Fields

Instances

Instances details
Functor ( Ran g h) Source #
Instance details

Defined in Data.Functor.Kan.Ran

Methods

fmap :: (a -> b) -> Ran g h a -> Ran g h b Source #

(<$) :: a -> Ran g h b -> Ran g h a Source #

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 . fromRanid
fromRan . toRanid

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

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

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