Copyright  (C) 2014 Edward Kmett 

License  BSDstyle (see the file LICENSE) 
Maintainer  Edward Kmett <ekmett@gmail.com> 
Stability  experimental 
Portability  GADTs, TFs, MPTCs, RankN 
Safe Haskell  Trustworthy 
Language  Haskell2010 
 data Procompose p q d c where
 Procompose :: p x c > q d x > Procompose p q d c
 procomposed :: Category p => Procompose p p a b > p a b
 idl :: Profunctor q => Iso (Procompose (>) q d c) (Procompose (>) r d' c') (q d c) (r d' c')
 idr :: Profunctor q => Iso (Procompose q (>) d c) (Procompose r (>) d' c') (q d c) (r d' c')
 assoc :: Iso (Procompose p (Procompose q r) a b) (Procompose x (Procompose y z) a b) (Procompose (Procompose p q) r a b) (Procompose (Procompose x y) z a b)
 upstars :: Functor g => Iso (Procompose (UpStar f) (UpStar g) d c) (Procompose (UpStar f') (UpStar g') d' c') (UpStar (Compose g f) d c) (UpStar (Compose g' f') d' c')
 kleislis :: Monad g => Iso (Procompose (Kleisli f) (Kleisli g) d c) (Procompose (Kleisli f') (Kleisli g') d' c') (Kleisli (Compose g f) d c) (Kleisli (Compose g' f') d' c')
 downstars :: Functor f => Iso (Procompose (DownStar f) (DownStar g) d c) (Procompose (DownStar f') (DownStar g') d' c') (DownStar (Compose f g) d c) (DownStar (Compose f' g') d' c')
 cokleislis :: Functor f => Iso (Procompose (Cokleisli f) (Cokleisli g) d c) (Procompose (Cokleisli f') (Cokleisli g') d' c') (Cokleisli (Compose f g) d c) (Cokleisli (Compose f' g') d' c')
 newtype Rift p q a b = Rift {
 runRift :: forall x. p b x > q a x
 decomposeRift :: Procompose p (Rift p q) :> q
Profunctor Composition
data Procompose p q d c where Source
is the Procompose
p qProfunctor
composition of the
Profunctor
s p
and q
.
For a good explanation of Profunctor
composition in Haskell
see Dan Piponi's article:
Procompose :: p x c > q d x > Procompose p q d c 
Category * p => ProfunctorMonad (Procompose p)  
ProfunctorFunctor (Procompose p)  
ProfunctorAdjunction (Procompose p) (Rift p)  
(Profunctor p, Profunctor q) => Profunctor (Procompose p q)  
(Choice p, Choice q) => Choice (Procompose p q)  
(Strong p, Strong q) => Strong (Procompose p q)  
(Closed p, Closed q) => Closed (Procompose p q)  
(Corepresentable p, Corepresentable q) => Corepresentable (Procompose p q)  
(Representable p, Representable q) => Representable (Procompose p q)  The composition of two 
Profunctor p => Functor (Procompose p q a)  
type Corep (Procompose p q) = Compose (Corep p) (Corep q)  
type Rep (Procompose p q) = Compose (Rep q) (Rep p) 
procomposed :: Category p => Procompose p p a b > p a b Source
Unitors and Associator
idl :: Profunctor q => Iso (Procompose (>) q d c) (Procompose (>) r d' c') (q d c) (r d' c') Source
(>)
functions as a lax identity for Profunctor
composition.
This provides an Iso
for the lens
package that witnesses the
isomorphism between
and Procompose
(>) q d cq d c
, which
is the left identity law.
idl
::Profunctor
q => Iso' (Procompose
(>) q d c) (q d c)
idr :: Profunctor q => Iso (Procompose q (>) d c) (Procompose r (>) d' c') (q d c) (r d' c') Source
(>)
functions as a lax identity for Profunctor
composition.
This provides an Iso
for the lens
package that witnesses the
isomorphism between
and Procompose
q (>) d cq d c
, which
is the right identity law.
idr
::Profunctor
q => Iso' (Procompose
q (>) d c) (q d c)
assoc :: Iso (Procompose p (Procompose q r) a b) (Procompose x (Procompose y z) a b) (Procompose (Procompose p q) r a b) (Procompose (Procompose x y) z a b) Source
The associator for Profunctor
composition.
This provides an Iso
for the lens
package that witnesses the
isomorphism between
and
Procompose
p (Procompose
q r) a b
, which arises because
Procompose
(Procompose
p q) r a bProf
is only a bicategory, rather than a strict 2category.
Generalized Composition
upstars :: Functor g => Iso (Procompose (UpStar f) (UpStar g) d c) (Procompose (UpStar f') (UpStar g') d' c') (UpStar (Compose g f) d c) (UpStar (Compose g' f') d' c') Source
Profunctor
composition generalizes Functor
composition in two ways.
This is the first, which shows that exists b. (a > f b, b > g c)
is
isomorphic to a > f (g c)
.
upstars
::Functor
f => Iso' (Procompose
(UpStar
f) (UpStar
g) d c) (UpStar
(Compose
f g) d c)
kleislis :: Monad g => Iso (Procompose (Kleisli f) (Kleisli g) d c) (Procompose (Kleisli f') (Kleisli g') d' c') (Kleisli (Compose g f) d c) (Kleisli (Compose g' f') d' c') Source
downstars :: Functor f => Iso (Procompose (DownStar f) (DownStar g) d c) (Procompose (DownStar f') (DownStar g') d' c') (DownStar (Compose f g) d c) (DownStar (Compose f' g') d' c') Source
Profunctor
composition generalizes Functor
composition in two ways.
This is the second, which shows that exists b. (f a > b, g b > c)
is
isomorphic to g (f a) > c
.
downstars
::Functor
f => Iso' (Procompose
(DownStar
f) (DownStar
g) d c) (DownStar
(Compose
g f) d c)
cokleislis :: Functor f => Iso (Procompose (Cokleisli f) (Cokleisli g) d c) (Procompose (Cokleisli f') (Cokleisli g') d' c') (Cokleisli (Compose f g) d c) (Cokleisli (Compose f' g') d' c') Source
This is a variant on downstars
that uses Cokleisli
instead
of DownStar
.
cokleislis
::Functor
f => Iso' (Procompose
(Cokleisli
f) (Cokleisli
g) d c) (Cokleisli
(Compose
g f) d c)
Right Kan Lift
This represents the right Kan lift of a Profunctor
q
along a Profunctor
p
in a limited version of the 2category of Profunctors where the only object is the category Hask, 1morphisms are profunctors composed and compose with Profunctor composition, and 2morphisms are just natural transformations.
(~) (* > * > *) p q => Category * (Rift p q) 

Category * p => ProfunctorComonad (Rift p)  
ProfunctorFunctor (Rift p)  
ProfunctorAdjunction (Procompose p) (Rift p)  
(Profunctor p, Profunctor q) => Profunctor (Rift p q)  
Profunctor p => Functor (Rift p q a) 
decomposeRift :: Procompose p (Rift p q) :> q Source
The 2morphism that defines a left Kan lift.
Note: When p
is right adjoint to
then Rift
p (>)decomposeRift
is the counit
of the adjunction.