    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE UndecidableInstances #-}
    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Profunctor.Composition
    -- Copyright   :  (C) 2014-2015 Edward Kmett
    -- License     :  BSD-style (see the file LICENSE)
    --
    -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
    -- Stability   :  experimental
    -- Portability :  GADTs, TFs, MPTCs, RankN
    --
    ----------------------------------------------------------------------------
    module Data.Profunctor.Composition
      (
      -- * Profunctor Composition
        Procompose(..)
      , procomposed
      -- * Unitors and Associator
      , idl
      , idr
      , assoc
      -- * Categories as monoid objects
      , eta
      , mu
      -- * Generalized Composition
      , stars, kleislis
      , costars, cokleislis
      -- * Right Kan Lift
      , Rift(..)
      , decomposeRift
      ) where

    import Control.Arrow
    import Control.Category
    import Control.Comonad
    import Control.Monad (liftM)
    import Data.Functor.Compose
    import Data.Profunctor
    import Data.Profunctor.Adjunction
    import Data.Profunctor.Monad
    import Data.Profunctor.Rep
    import Data.Profunctor.Sieve
    import Data.Profunctor.Traversing
    import Data.Profunctor.Unsafe
    import Prelude hiding ((.),id)

    type Iso s t a b = forall p f. (Profunctor p, Functor f) => p a (f b) -> p s (f t)

    -- * Profunctor Composition

    -- | @'Procompose' p q@ is the 'Profunctor' composition of the
    -- 'Profunctor's @p@ and @q@.
    --
    -- For a good explanation of 'Profunctor' composition in Haskell
    -- see Dan Piponi's article:
    --
    -- <http://blog.sigfpe.com/2011/07/profunctors-in-haskell.html>
    data Procompose p q d c where
      Procompose :: p x c -> q d x -> Procompose p q d c

    instance ProfunctorFunctor (Procompose p) where
      promap :: (p :-> q) -> Procompose p p :-> Procompose p q
    promap f :: p :-> q
    f (Procompose p :: p x b
    p q :: p a x
    q) = p x b -> q a x -> Procompose p q a b
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose p x b
    p (p a x -> q a x
    p :-> q
    f p a x
    q)

    instance Category p => ProfunctorMonad (Procompose p) where
      proreturn :: p :-> Procompose p p
    proreturn = p b b -> p a b -> Procompose p p a b
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose p b b
    forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id
      projoin :: Procompose p (Procompose p p) :-> Procompose p p
    projoin (Procompose p :: p x b
    p (Procompose q :: p x x
    q r :: p a x
    r)) = p x b -> p a x -> Procompose p p a b
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose (p x b
    p p x b -> p x x -> p x b
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . p x x
    q) p a x
    r

    procomposed :: Category p => Procompose p p a b -> p a b
    procomposed :: Procompose p p a b -> p a b
    procomposed (Procompose pxc :: p x b
    pxc pdx :: p a x
    pdx) = p x b
    pxc p x b -> p a x -> p a b
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . p a x
    pdx
    {-# INLINE procomposed #-}

    instance (Profunctor p, Profunctor q) => Profunctor (Procompose p q) where
      dimap :: (a -> b) -> (c -> d) -> Procompose p q b c -> Procompose p q a d
    dimap l :: a -> b
    l r :: c -> d
    r (Procompose f :: p x c
    f g :: q b x
    g) = p x d -> q a x -> Procompose p q a d
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose ((c -> d) -> p x c -> p x d
    forall (p :: * -> * -> *) b c a.
    Profunctor p =>
    (b -> c) -> p a b -> p a c
    rmap c -> d
    r p x c
    f) ((a -> b) -> q b x -> q a x
    forall (p :: * -> * -> *) a b c.
    Profunctor p =>
    (a -> b) -> p b c -> p a c
    lmap a -> b
    l q b x
    g)
      {-# INLINE dimap #-}
      lmap :: (a -> b) -> Procompose p q b c -> Procompose p q a c
    lmap k :: a -> b
    k (Procompose f :: p x c
    f g :: q b x
    g) = p x c -> q a x -> Procompose p q a c
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose p x c
    f ((a -> b) -> q b x -> q a x
    forall (p :: * -> * -> *) a b c.
    Profunctor p =>
    (a -> b) -> p b c -> p a c
    lmap a -> b
    k q b x
    g)
      {-# INLINE rmap #-}
      rmap :: (b -> c) -> Procompose p q a b -> Procompose p q a c
    rmap k :: b -> c
    k (Procompose f :: p x b
    f g :: q a x
    g) = p x c -> q a x -> Procompose p q a c
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose ((b -> c) -> p x b -> p x c
    forall (p :: * -> * -> *) b c a.
    Profunctor p =>
    (b -> c) -> p a b -> p a c
    rmap b -> c
    k p x b
    f) q a x
    g
      {-# INLINE lmap #-}
      k :: q b c
    k #. :: q b c -> Procompose p q a b -> Procompose p q a c
    #. Procompose f :: p x b
    f g :: q a x
    g     = p x c -> q a x -> Procompose p q a c
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose (q b c
    k q b c -> p x b -> p x c
    forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
    (Profunctor p, Coercible c b) =>
    q b c -> p a b -> p a c
    #. p x b
    f) q a x
    g
      {-# INLINE (#.) #-}
      Procompose f :: p x c
    f g :: q b x
    g .# :: Procompose p q b c -> q a b -> Procompose p q a c
    .# k :: q a b
    k     = p x c -> q a x -> Procompose p q a c
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose p x c
    f (q b x
    g q b x -> q a b -> q a x
    forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
    (Profunctor p, Coercible b a) =>
    p b c -> q a b -> p a c
    .# q a b
    k)
      {-# INLINE (.#) #-}

    instance Profunctor p => Functor (Procompose p q a) where
      fmap :: (a -> b) -> Procompose p q a a -> Procompose p q a b
    fmap k :: a -> b
    k (Procompose f :: p x a
    f g :: q a x
    g) = p x b -> q a x -> Procompose p q a b
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose ((a -> b) -> p x a -> p x b
    forall (p :: * -> * -> *) b c a.
    Profunctor p =>
    (b -> c) -> p a b -> p a c
    rmap a -> b
    k p x a
    f) q a x
    g
      {-# INLINE fmap #-}

    instance (Sieve p f, Sieve q g) => Sieve (Procompose p q) (Compose g f) where
      sieve :: Procompose p q a b -> a -> Compose g f b
    sieve (Procompose g :: p x b
    g f :: q a x
    f) d :: a
    d = g (f b) -> Compose g f b
    forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
    f (g a) -> Compose f g a
    Compose (g (f b) -> Compose g f b) -> g (f b) -> Compose g f b
    forall a b. (a -> b) -> a -> b
    $ p x b -> x -> f b
    forall (p :: * -> * -> *) (f :: * -> *) a b.
    Sieve p f =>
    p a b -> a -> f b
    sieve p x b
    g (x -> f b) -> g x -> g (f b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> q a x -> a -> g x
    forall (p :: * -> * -> *) (f :: * -> *) a b.
    Sieve p f =>
    p a b -> a -> f b
    sieve q a x
    f a
    d
      {-# INLINE sieve #-}

    -- | The composition of two 'Representable' 'Profunctor's is 'Representable' by
    -- the composition of their representations.
    instance (Representable p, Representable q) => Representable (Procompose p q) where
      type Rep (Procompose p q) = Compose (Rep q) (Rep p)
      tabulate :: (d -> Rep (Procompose p q) c) -> Procompose p q d c
    tabulate f :: d -> Rep (Procompose p q) c
    f = p (Rep p c) c -> q d (Rep p c) -> Procompose p q d c
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose ((Rep p c -> Rep p c) -> p (Rep p c) c
    forall (p :: * -> * -> *) d c.
    Representable p =>
    (d -> Rep p c) -> p d c
    tabulate Rep p c -> Rep p c
    forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id) ((d -> Rep q (Rep p c)) -> q d (Rep p c)
    forall (p :: * -> * -> *) d c.
    Representable p =>
    (d -> Rep p c) -> p d c
    tabulate (Compose (Rep q) (Rep p) c -> Rep q (Rep p c)
    forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
    Compose f g a -> f (g a)
    getCompose (Compose (Rep q) (Rep p) c -> Rep q (Rep p c))
    -> (d -> Compose (Rep q) (Rep p) c) -> d -> Rep q (Rep p c)
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . d -> Compose (Rep q) (Rep p) c
    d -> Rep (Procompose p q) c
    f))
      {-# INLINE tabulate #-}

    instance (Cosieve p f, Cosieve q g) => Cosieve (Procompose p q) (Compose f g) where
      cosieve :: Procompose p q a b -> Compose f g a -> b
    cosieve (Procompose g :: p x b
    g f :: q a x
    f) (Compose d :: f (g a)
    d) = p x b -> f x -> b
    forall (p :: * -> * -> *) (f :: * -> *) a b.
    Cosieve p f =>
    p a b -> f a -> b
    cosieve p x b
    g (f x -> b) -> f x -> b
    forall a b. (a -> b) -> a -> b
    $ q a x -> g a -> x
    forall (p :: * -> * -> *) (f :: * -> *) a b.
    Cosieve p f =>
    p a b -> f a -> b
    cosieve q a x
    f (g a -> x) -> f (g a) -> f x
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f (g a)
    d
      {-# INLINE cosieve #-}

    instance (Corepresentable p, Corepresentable q) => Corepresentable (Procompose p q) where
      type Corep (Procompose p q) = Compose (Corep p) (Corep q)
      cotabulate :: (Corep (Procompose p q) d -> c) -> Procompose p q d c
    cotabulate f :: Corep (Procompose p q) d -> c
    f = p (Corep q d) c -> q d (Corep q d) -> Procompose p q d c
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose ((Corep p (Corep q d) -> c) -> p (Corep q d) c
    forall (p :: * -> * -> *) d c.
    Corepresentable p =>
    (Corep p d -> c) -> p d c
    cotabulate (Compose (Corep p) (Corep q) d -> c
    Corep (Procompose p q) d -> c
    f (Compose (Corep p) (Corep q) d -> c)
    -> (Corep p (Corep q d) -> Compose (Corep p) (Corep q) d)
    -> Corep p (Corep q d)
    -> c
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . Corep p (Corep q d) -> Compose (Corep p) (Corep q) d
    forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
    f (g a) -> Compose f g a
    Compose)) ((Corep q d -> Corep q d) -> q d (Corep q d)
    forall (p :: * -> * -> *) d c.
    Corepresentable p =>
    (Corep p d -> c) -> p d c
    cotabulate Corep q d -> Corep q d
    forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id)
      {-# INLINE cotabulate #-}

    instance (Strong p, Strong q) => Strong (Procompose p q) where
      first' :: Procompose p q a b -> Procompose p q (a, c) (b, c)
    first' (Procompose x :: p x b
    x y :: q a x
    y) = p (x, c) (b, c) -> q (a, c) (x, c) -> Procompose p q (a, c) (b, c)
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose (p x b -> p (x, c) (b, c)
    forall (p :: * -> * -> *) a b c.
    Strong p =>
    p a b -> p (a, c) (b, c)
    first' p x b
    x) (q a x -> q (a, c) (x, c)
    forall (p :: * -> * -> *) a b c.
    Strong p =>
    p a b -> p (a, c) (b, c)
    first' q a x
    y)
      {-# INLINE first' #-}
      second' :: Procompose p q a b -> Procompose p q (c, a) (c, b)
    second' (Procompose x :: p x b
    x y :: q a x
    y) = p (c, x) (c, b) -> q (c, a) (c, x) -> Procompose p q (c, a) (c, b)
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose (p x b -> p (c, x) (c, b)
    forall (p :: * -> * -> *) a b c.
    Strong p =>
    p a b -> p (c, a) (c, b)
    second' p x b
    x) (q a x -> q (c, a) (c, x)
    forall (p :: * -> * -> *) a b c.
    Strong p =>
    p a b -> p (c, a) (c, b)
    second' q a x
    y)
      {-# INLINE second' #-}

    instance (Choice p, Choice q) => Choice (Procompose p q) where
      left' :: Procompose p q a b -> Procompose p q (Either a c) (Either b c)
    left' (Procompose x :: p x b
    x y :: q a x
    y) = p (Either x c) (Either b c)
    -> q (Either a c) (Either x c)
    -> Procompose p q (Either a c) (Either b c)
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose (p x b -> p (Either x c) (Either b c)
    forall (p :: * -> * -> *) a b c.
    Choice p =>
    p a b -> p (Either a c) (Either b c)
    left' p x b
    x) (q a x -> q (Either a c) (Either x c)
    forall (p :: * -> * -> *) a b c.
    Choice p =>
    p a b -> p (Either a c) (Either b c)
    left' q a x
    y)
      {-# INLINE left' #-}
      right' :: Procompose p q a b -> Procompose p q (Either c a) (Either c b)
    right' (Procompose x :: p x b
    x y :: q a x
    y) = p (Either c x) (Either c b)
    -> q (Either c a) (Either c x)
    -> Procompose p q (Either c a) (Either c b)
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose (p x b -> p (Either c x) (Either c b)
    forall (p :: * -> * -> *) a b c.
    Choice p =>
    p a b -> p (Either c a) (Either c b)
    right' p x b
    x) (q a x -> q (Either c a) (Either c x)
    forall (p :: * -> * -> *) a b c.
    Choice p =>
    p a b -> p (Either c a) (Either c b)
    right' q a x
    y)
      {-# INLINE right' #-}

    instance (Closed p, Closed q) => Closed (Procompose p q) where
      closed :: Procompose p q a b -> Procompose p q (x -> a) (x -> b)
    closed (Procompose x :: p x b
    x y :: q a x
    y) = p (x -> x) (x -> b)
    -> q (x -> a) (x -> x) -> Procompose p q (x -> a) (x -> b)
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose (p x b -> p (x -> x) (x -> b)
    forall (p :: * -> * -> *) a b x.
    Closed p =>
    p a b -> p (x -> a) (x -> b)
    closed p x b
    x) (q a x -> q (x -> a) (x -> x)
    forall (p :: * -> * -> *) a b x.
    Closed p =>
    p a b -> p (x -> a) (x -> b)
    closed q a x
    y)
      {-# INLINE closed #-}

    instance (Traversing p, Traversing q) => Traversing (Procompose p q) where
      traverse' :: Procompose p q a b -> Procompose p q (f a) (f b)
    traverse' (Procompose p :: p x b
    p q :: q a x
    q) = p (f x) (f b) -> q (f a) (f x) -> Procompose p q (f a) (f b)
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose (p x b -> p (f x) (f b)
    forall (p :: * -> * -> *) (f :: * -> *) a b.
    (Traversing p, Traversable f) =>
    p a b -> p (f a) (f b)
    traverse' p x b
    p) (q a x -> q (f a) (f x)
    forall (p :: * -> * -> *) (f :: * -> *) a b.
    (Traversing p, Traversable f) =>
    p a b -> p (f a) (f b)
    traverse' q a x
    q)
      {-# INLINE traverse' #-}

    instance (Mapping p, Mapping q) => Mapping (Procompose p q) where
      map' :: Procompose p q a b -> Procompose p q (f a) (f b)
    map' (Procompose p :: p x b
    p q :: q a x
    q) = p (f x) (f b) -> q (f a) (f x) -> Procompose p q (f a) (f b)
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose (p x b -> p (f x) (f b)
    forall (p :: * -> * -> *) (f :: * -> *) a b.
    (Mapping p, Functor f) =>
    p a b -> p (f a) (f b)
    map' p x b
    p) (q a x -> q (f a) (f x)
    forall (p :: * -> * -> *) (f :: * -> *) a b.
    (Mapping p, Functor f) =>
    p a b -> p (f a) (f b)
    map' q a x
    q)
      {-# INLINE map' #-}

    instance (Corepresentable p, Corepresentable q) => Costrong (Procompose p q) where
      unfirst :: Procompose p q (a, d) (b, d) -> Procompose p q a b
    unfirst = Procompose p q (a, d) (b, d) -> Procompose p q a b
    forall (p :: * -> * -> *) a d b.
    Corepresentable p =>
    p (a, d) (b, d) -> p a b
    unfirstCorep
      {-# INLINE unfirst #-}
      unsecond :: Procompose p q (d, a) (d, b) -> Procompose p q a b
    unsecond = Procompose p q (d, a) (d, b) -> Procompose p q a b
    forall (p :: * -> * -> *) d a b.
    Corepresentable p =>
    p (d, a) (d, b) -> p a b
    unsecondCorep
      {-# INLINE unsecond #-}

    -- * Lax identity

    -- | @(->)@ functions as a lax identity for 'Profunctor' composition.
    --
    -- This provides an 'Iso' for the @lens@ package that witnesses the
    -- isomorphism between @'Procompose' (->) q d c@ and @q d c@, which
    -- is the left identity law.
    --
    -- @
    -- 'idl' :: 'Profunctor' q => Iso' ('Procompose' (->) q d c) (q d c)
    -- @
    idl :: Profunctor q => Iso (Procompose (->) q d c) (Procompose (->) r d' c') (q d c) (r d' c')
    idl :: Iso
      (Procompose (->) q d c) (Procompose (->) r d' c') (q d c) (r d' c')
    idl = (Procompose (->) q d c -> q d c)
    -> (f (r d' c') -> f (Procompose (->) r d' c'))
    -> p (q d c) (f (r d' c'))
    -> p (Procompose (->) q d c) (f (Procompose (->) r d' c'))
    forall (p :: * -> * -> *) a b c d.
    Profunctor p =>
    (a -> b) -> (c -> d) -> p b c -> p a d
    dimap (\(Procompose g :: x -> c
    g f :: q d x
    f) -> (x -> c) -> q d x -> q d c
    forall (p :: * -> * -> *) b c a.
    Profunctor p =>
    (b -> c) -> p a b -> p a c
    rmap x -> c
    g q d x
    f) ((r d' c' -> Procompose (->) r d' c')
    -> f (r d' c') -> f (Procompose (->) r d' c')
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((c' -> c') -> r d' c' -> Procompose (->) r d' c'
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose c' -> c'
    forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id))

    -- | @(->)@ functions as a lax identity for 'Profunctor' composition.
    --
    -- This provides an 'Iso' for the @lens@ package that witnesses the
    -- isomorphism between @'Procompose' q (->) d c@ and @q d c@, which
    -- is the right identity law.
    --
    -- @
    -- 'idr' :: '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')
    idr :: Iso
      (Procompose q (->) d c) (Procompose r (->) d' c') (q d c) (r d' c')
    idr = (Procompose q (->) d c -> q d c)
    -> (f (r d' c') -> f (Procompose r (->) d' c'))
    -> p (q d c) (f (r d' c'))
    -> p (Procompose q (->) d c) (f (Procompose r (->) d' c'))
    forall (p :: * -> * -> *) a b c d.
    Profunctor p =>
    (a -> b) -> (c -> d) -> p b c -> p a d
    dimap (\(Procompose g :: q x c
    g f :: d -> x
    f) -> (d -> x) -> q x c -> q d c
    forall (p :: * -> * -> *) a b c.
    Profunctor p =>
    (a -> b) -> p b c -> p a c
    lmap d -> x
    f q x c
    g) ((r d' c' -> Procompose r (->) d' c')
    -> f (r d' c') -> f (Procompose r (->) d' c')
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (r d' c' -> (d' -> d') -> Procompose r (->) d' c'
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    `Procompose` d' -> d'
    forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id))

    -- | The associator for 'Profunctor' composition.
    --
    -- This provides an 'Iso' for the @lens@ package that witnesses the
    -- isomorphism between @'Procompose' p ('Procompose' q r) a b@ and
    -- @'Procompose' ('Procompose' p q) r a b@, which arises because
    -- @Prof@ is only a bicategory, rather than a strict 2-category.
    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)
    assoc :: p (Procompose (Procompose p q) r a b)
      (f (Procompose (Procompose x y) z a b))
    -> p (Procompose p (Procompose q r) a b)
         (f (Procompose x (Procompose y z) a b))
    assoc = (Procompose p (Procompose q r) a b
     -> Procompose (Procompose p q) r a b)
    -> (f (Procompose (Procompose x y) z a b)
        -> f (Procompose x (Procompose y z) a b))
    -> p (Procompose (Procompose p q) r a b)
         (f (Procompose (Procompose x y) z a b))
    -> p (Procompose p (Procompose q r) a b)
         (f (Procompose x (Procompose y z) a b))
    forall (p :: * -> * -> *) a b c d.
    Profunctor p =>
    (a -> b) -> (c -> d) -> p b c -> p a d
    dimap (\(Procompose f :: p x b
    f (Procompose g h)) -> Procompose p q x b -> r a x -> Procompose (Procompose p q) r a b
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose (p x b -> q x x -> Procompose p q x b
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose p x b
    f q x x
    g) r a x
    h)
                  ((Procompose (Procompose x y) z a b
     -> Procompose x (Procompose y z) a b)
    -> f (Procompose (Procompose x y) z a b)
    -> f (Procompose x (Procompose y z) a b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\(Procompose (Procompose f g) h :: z a x
    h) -> x x b -> Procompose y z a x -> Procompose x (Procompose y z) a b
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose x x b
    f (y x x -> z a x -> Procompose y z a x
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose y x x
    g z a x
    h)))

    -- | '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)@.
    --
    -- @'stars' :: 'Functor' f => Iso' ('Procompose' ('Star' f) ('Star' g) d c) ('Star' ('Compose' f g) d c)@
    stars :: Functor g
            => Iso (Procompose (Star f ) (Star g ) d  c )
                   (Procompose (Star f') (Star g') d' c')
                   (Star (Compose g  f ) d  c )
                   (Star (Compose g' f') d' c')
    stars :: Iso
      (Procompose (Star f) (Star g) d c)
      (Procompose (Star f') (Star g') d' c')
      (Star (Compose g f) d c)
      (Star (Compose g' f') d' c')
    stars = (Procompose (Star f) (Star g) d c -> Star (Compose g f) d c)
    -> (f (Star (Compose g' f') d' c')
        -> f (Procompose (Star f') (Star g') d' c'))
    -> p (Star (Compose g f) d c) (f (Star (Compose g' f') d' c'))
    -> p (Procompose (Star f) (Star g) d c)
         (f (Procompose (Star f') (Star g') d' c'))
    forall (p :: * -> * -> *) a b c d.
    Profunctor p =>
    (a -> b) -> (c -> d) -> p b c -> p a d
    dimap Procompose (Star f) (Star g) d c -> Star (Compose g f) d c
    forall (f :: * -> *) (g :: * -> *) d c.
    Functor f =>
    Procompose (Star g) (Star f) d c -> Star (Compose f g) d c
    hither ((Star (Compose g' f') d' c'
     -> Procompose (Star f') (Star g') d' c')
    -> f (Star (Compose g' f') d' c')
    -> f (Procompose (Star f') (Star g') d' c')
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Star (Compose g' f') d' c' -> Procompose (Star f') (Star g') d' c'
    forall (f :: * -> *) (f :: * -> *) d c.
    Star (Compose f f) d c -> Procompose (Star f) (Star f) d c
    yon) where
      hither :: Procompose (Star g) (Star f) d c -> Star (Compose f g) d c
    hither (Procompose (Star xgc) (Star dfx)) = (d -> Compose f g c) -> Star (Compose f g) d c
    forall (f :: * -> *) d c. (d -> f c) -> Star f d c
    Star (f (g c) -> Compose f g c
    forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
    f (g a) -> Compose f g a
    Compose (f (g c) -> Compose f g c) -> (d -> f (g c)) -> d -> Compose f g c
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . (x -> g c) -> f x -> f (g c)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap x -> g c
    xgc (f x -> f (g c)) -> (d -> f x) -> d -> f (g c)
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . d -> f x
    dfx)
      yon :: Star (Compose f f) d c -> Procompose (Star f) (Star f) d c
    yon (Star dfgc :: d -> Compose f f c
    dfgc) = Star f (f c) c
    -> Star f d (f c) -> Procompose (Star f) (Star f) d c
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose ((f c -> f c) -> Star f (f c) c
    forall (f :: * -> *) d c. (d -> f c) -> Star f d c
    Star f c -> f c
    forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id) ((d -> f (f c)) -> Star f d (f c)
    forall (f :: * -> *) d c. (d -> f c) -> Star f d c
    Star (Compose f f c -> f (f c)
    forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
    Compose f g a -> f (g a)
    getCompose (Compose f f c -> f (f c)) -> (d -> Compose f f c) -> d -> f (f c)
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . d -> Compose f f c
    dfgc))

    -- | '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@.
    --
    -- @'costars' :: 'Functor' f => Iso' ('Procompose' ('Costar' f) ('Costar' g) d c) ('Costar' ('Compose' g f) d c)@
    costars :: Functor f
              => Iso (Procompose (Costar f ) (Costar g ) d  c )
                     (Procompose (Costar f') (Costar g') d' c')
                     (Costar (Compose f  g ) d  c )
                     (Costar (Compose f' g') d' c')
    costars :: Iso
      (Procompose (Costar f) (Costar g) d c)
      (Procompose (Costar f') (Costar g') d' c')
      (Costar (Compose f g) d c)
      (Costar (Compose f' g') d' c')
    costars = (Procompose (Costar f) (Costar g) d c -> Costar (Compose f g) d c)
    -> (f (Costar (Compose f' g') d' c')
        -> f (Procompose (Costar f') (Costar g') d' c'))
    -> p (Costar (Compose f g) d c) (f (Costar (Compose f' g') d' c'))
    -> p (Procompose (Costar f) (Costar g) d c)
         (f (Procompose (Costar f') (Costar g') d' c'))
    forall (p :: * -> * -> *) a b c d.
    Profunctor p =>
    (a -> b) -> (c -> d) -> p b c -> p a d
    dimap Procompose (Costar f) (Costar g) d c -> Costar (Compose f g) d c
    forall (f :: * -> *) (f :: * -> *) d c.
    Functor f =>
    Procompose (Costar f) (Costar f) d c -> Costar (Compose f f) d c
    hither ((Costar (Compose f' g') d' c'
     -> Procompose (Costar f') (Costar g') d' c')
    -> f (Costar (Compose f' g') d' c')
    -> f (Procompose (Costar f') (Costar g') d' c')
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Costar (Compose f' g') d' c'
    -> Procompose (Costar f') (Costar g') d' c'
    forall (f :: * -> *) (f :: * -> *) d c.
    Costar (Compose f f) d c -> Procompose (Costar f) (Costar f) d c
    yon) where
      hither :: Procompose (Costar f) (Costar f) d c -> Costar (Compose f f) d c
    hither (Procompose (Costar gxc) (Costar fdx)) = (Compose f f d -> c) -> Costar (Compose f f) d c
    forall (f :: * -> *) d c. (f d -> c) -> Costar f d c
    Costar (f x -> c
    gxc (f x -> c) -> (Compose f f d -> f x) -> Compose f f d -> c
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . (f d -> x) -> f (f d) -> f x
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap f d -> x
    fdx (f (f d) -> f x)
    -> (Compose f f d -> f (f d)) -> Compose f f d -> f x
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . Compose f f d -> f (f d)
    forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
    Compose f g a -> f (g a)
    getCompose)
      yon :: Costar (Compose f f) d c -> Procompose (Costar f) (Costar f) d c
    yon (Costar dgfc :: Compose f f d -> c
    dgfc) = Costar f (f d) c
    -> Costar f d (f d) -> Procompose (Costar f) (Costar f) d c
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose ((f (f d) -> c) -> Costar f (f d) c
    forall (f :: * -> *) d c. (f d -> c) -> Costar f d c
    Costar (Compose f f d -> c
    dgfc (Compose f f d -> c) -> (f (f d) -> Compose f f d) -> f (f d) -> c
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . f (f d) -> Compose f f d
    forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
    f (g a) -> Compose f g a
    Compose)) ((f d -> f d) -> Costar f d (f d)
    forall (f :: * -> *) d c. (f d -> c) -> Costar f d c
    Costar f d -> f d
    forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id)

    -- | This is a variant on 'stars' that uses 'Kleisli' instead of 'Star'.
    --
    -- @'kleislis' :: 'Monad' f => Iso' ('Procompose' ('Kleisli' f) ('Kleisli' g) d c) ('Kleisli' ('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')
    kleislis :: 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')
    kleislis = (Procompose (Kleisli f) (Kleisli g) d c
     -> Kleisli (Compose g f) d c)
    -> (f (Kleisli (Compose g' f') d' c')
        -> f (Procompose (Kleisli f') (Kleisli g') d' c'))
    -> p (Kleisli (Compose g f) d c)
         (f (Kleisli (Compose g' f') d' c'))
    -> p (Procompose (Kleisli f) (Kleisli g) d c)
         (f (Procompose (Kleisli f') (Kleisli g') d' c'))
    forall (p :: * -> * -> *) a b c d.
    Profunctor p =>
    (a -> b) -> (c -> d) -> p b c -> p a d
    dimap Procompose (Kleisli f) (Kleisli g) d c -> Kleisli (Compose g f) d c
    forall (f :: * -> *) (g :: * -> *) d c.
    Monad f =>
    Procompose (Kleisli g) (Kleisli f) d c -> Kleisli (Compose f g) d c
    hither ((Kleisli (Compose g' f') d' c'
     -> Procompose (Kleisli f') (Kleisli g') d' c')
    -> f (Kleisli (Compose g' f') d' c')
    -> f (Procompose (Kleisli f') (Kleisli g') d' c')
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Kleisli (Compose g' f') d' c'
    -> Procompose (Kleisli f') (Kleisli g') d' c'
    forall (m :: * -> *) (m :: * -> *) d c.
    Kleisli (Compose m m) d c -> Procompose (Kleisli m) (Kleisli m) d c
    yon) where
      hither :: Procompose (Kleisli g) (Kleisli f) d c -> Kleisli (Compose f g) d c
    hither (Procompose (Kleisli xgc) (Kleisli dfx)) = (d -> Compose f g c) -> Kleisli (Compose f g) d c
    forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
    Kleisli (f (g c) -> Compose f g c
    forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
    f (g a) -> Compose f g a
    Compose (f (g c) -> Compose f g c) -> (d -> f (g c)) -> d -> Compose f g c
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . (x -> g c) -> f x -> f (g c)
    forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
    liftM x -> g c
    xgc (f x -> f (g c)) -> (d -> f x) -> d -> f (g c)
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . d -> f x
    dfx)
      yon :: Kleisli (Compose m m) d c -> Procompose (Kleisli m) (Kleisli m) d c
    yon (Kleisli dfgc :: d -> Compose m m c
    dfgc) = Kleisli m (m c) c
    -> Kleisli m d (m c) -> Procompose (Kleisli m) (Kleisli m) d c
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose ((m c -> m c) -> Kleisli m (m c) c
    forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
    Kleisli m c -> m c
    forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id) ((d -> m (m c)) -> Kleisli m d (m c)
    forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
    Kleisli (Compose m m c -> m (m c)
    forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
    Compose f g a -> f (g a)
    getCompose (Compose m m c -> m (m c)) -> (d -> Compose m m c) -> d -> m (m c)
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . d -> Compose m m c
    dfgc))

    -- | This is a variant on 'costars' that uses 'Cokleisli' instead
    -- of 'Costar'.
    --
    -- @'cokleislis' :: 'Functor' f => Iso' ('Procompose' ('Cokleisli' f) ('Cokleisli' g) d c) ('Cokleisli' ('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')
    cokleislis :: 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')
    cokleislis = (Procompose (Cokleisli f) (Cokleisli g) d c
     -> Cokleisli (Compose f g) d c)
    -> (f (Cokleisli (Compose f' g') d' c')
        -> f (Procompose (Cokleisli f') (Cokleisli g') d' c'))
    -> p (Cokleisli (Compose f g) d c)
         (f (Cokleisli (Compose f' g') d' c'))
    -> p (Procompose (Cokleisli f) (Cokleisli g) d c)
         (f (Procompose (Cokleisli f') (Cokleisli g') d' c'))
    forall (p :: * -> * -> *) a b c d.
    Profunctor p =>
    (a -> b) -> (c -> d) -> p b c -> p a d
    dimap Procompose (Cokleisli f) (Cokleisli g) d c
    -> Cokleisli (Compose f g) d c
    forall (w :: * -> *) (w :: * -> *) d c.
    Functor w =>
    Procompose (Cokleisli w) (Cokleisli w) d c
    -> Cokleisli (Compose w w) d c
    hither ((Cokleisli (Compose f' g') d' c'
     -> Procompose (Cokleisli f') (Cokleisli g') d' c')
    -> f (Cokleisli (Compose f' g') d' c')
    -> f (Procompose (Cokleisli f') (Cokleisli g') d' c')
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Cokleisli (Compose f' g') d' c'
    -> Procompose (Cokleisli f') (Cokleisli g') d' c'
    forall (w :: * -> *) (w :: * -> *) d c.
    Cokleisli (Compose w w) d c
    -> Procompose (Cokleisli w) (Cokleisli w) d c
    yon) where
      hither :: Procompose (Cokleisli w) (Cokleisli w) d c
    -> Cokleisli (Compose w w) d c
    hither (Procompose (Cokleisli gxc) (Cokleisli fdx)) = (Compose w w d -> c) -> Cokleisli (Compose w w) d c
    forall k (w :: k -> *) (a :: k) b. (w a -> b) -> Cokleisli w a b
    Cokleisli (w x -> c
    gxc (w x -> c) -> (Compose w w d -> w x) -> Compose w w d -> c
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . (w d -> x) -> w (w d) -> w x
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap w d -> x
    fdx (w (w d) -> w x)
    -> (Compose w w d -> w (w d)) -> Compose w w d -> w x
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . Compose w w d -> w (w d)
    forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
    Compose f g a -> f (g a)
    getCompose)
      yon :: Cokleisli (Compose w w) d c
    -> Procompose (Cokleisli w) (Cokleisli w) d c
    yon (Cokleisli dgfc :: Compose w w d -> c
    dgfc) = Cokleisli w (w d) c
    -> Cokleisli w d (w d)
    -> Procompose (Cokleisli w) (Cokleisli w) d c
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose ((w (w d) -> c) -> Cokleisli w (w d) c
    forall k (w :: k -> *) (a :: k) b. (w a -> b) -> Cokleisli w a b
    Cokleisli (Compose w w d -> c
    dgfc (Compose w w d -> c) -> (w (w d) -> Compose w w d) -> w (w d) -> c
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . w (w d) -> Compose w w d
    forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
    f (g a) -> Compose f g a
    Compose)) ((w d -> w d) -> Cokleisli w d (w d)
    forall k (w :: k -> *) (a :: k) b. (w a -> b) -> Cokleisli w a b
    Cokleisli w d -> w d
    forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id)

    ----------------------------------------------------------------------------
    -- * Rift
    ----------------------------------------------------------------------------

    -- | This represents the right Kan lift of a 'Profunctor' @q@ along a 'Profunctor' @p@ in a limited version of the 2-category of Profunctors where the only object is the category Hask, 1-morphisms are profunctors composed and compose with Profunctor composition, and 2-morphisms are just natural transformations.
    newtype Rift p q a b = Rift { Rift p q a b -> forall x. p b x -> q a x
    runRift :: forall x. p b x -> q a x }

    instance ProfunctorFunctor (Rift p) where
      promap :: (p :-> q) -> Rift p p :-> Rift p q
    promap f :: p :-> q
    f (Rift g :: forall x. p b x -> p a x
    g) = (forall x. p b x -> q a x) -> Rift p q a b
    forall (p :: * -> * -> *) (q :: * -> * -> *) a b.
    (forall x. p b x -> q a x) -> Rift p q a b
    Rift (p a x -> q a x
    p :-> q
    f (p a x -> q a x) -> (p b x -> p a x) -> p b x -> q a x
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . p b x -> p a x
    forall x. p b x -> p a x
    g)

    instance Category p => ProfunctorComonad (Rift p) where
      proextract :: Rift p p :-> p
    proextract (Rift f :: forall x. p b x -> p a x
    f) = p b b -> p a b
    forall x. p b x -> p a x
    f p b b
    forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id
      produplicate :: Rift p p :-> Rift p (Rift p p)
    produplicate (Rift f :: forall x. p b x -> p a x
    f) = (forall x. p b x -> Rift p p a x) -> Rift p (Rift p p) a b
    forall (p :: * -> * -> *) (q :: * -> * -> *) a b.
    (forall x. p b x -> q a x) -> Rift p q a b
    Rift ((forall x. p b x -> Rift p p a x) -> Rift p (Rift p p) a b)
    -> (forall x. p b x -> Rift p p a x) -> Rift p (Rift p p) a b
    forall a b. (a -> b) -> a -> b
    $ \p :: p b x
    p -> (forall x. p x x -> p a x) -> Rift p p a x
    forall (p :: * -> * -> *) (q :: * -> * -> *) a b.
    (forall x. p b x -> q a x) -> Rift p q a b
    Rift ((forall x. p x x -> p a x) -> Rift p p a x)
    -> (forall x. p x x -> p a x) -> Rift p p a x
    forall a b. (a -> b) -> a -> b
    $ \q :: p x x
    q -> p b x -> p a x
    forall x. p b x -> p a x
    f (p x x
    q p x x -> p b x -> p b x
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . p b x
    p)

    instance (Profunctor p, Profunctor q) => Profunctor (Rift p q) where
      dimap :: (a -> b) -> (c -> d) -> Rift p q b c -> Rift p q a d
    dimap ca :: a -> b
    ca bd :: c -> d
    bd f :: Rift p q b c
    f = (forall x. p d x -> q a x) -> Rift p q a d
    forall (p :: * -> * -> *) (q :: * -> * -> *) a b.
    (forall x. p b x -> q a x) -> Rift p q a b
    Rift ((a -> b) -> q b x -> q a x
    forall (p :: * -> * -> *) a b c.
    Profunctor p =>
    (a -> b) -> p b c -> p a c
    lmap a -> b
    ca (q b x -> q a x) -> (p d x -> q b x) -> p d x -> q a x
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . Rift p q b c -> forall x. p c x -> q b x
    forall (p :: * -> * -> *) (q :: * -> * -> *) a b.
    Rift p q a b -> forall x. p b x -> q a x
    runRift Rift p q b c
    f (p c x -> q b x) -> (p d x -> p c x) -> p d x -> q b x
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . (c -> d) -> p d x -> p c x
    forall (p :: * -> * -> *) a b c.
    Profunctor p =>
    (a -> b) -> p b c -> p a c
    lmap c -> d
    bd)
      {-# INLINE dimap #-}
      lmap :: (a -> b) -> Rift p q b c -> Rift p q a c
    lmap ca :: a -> b
    ca f :: Rift p q b c
    f = (forall x. p c x -> q a x) -> Rift p q a c
    forall (p :: * -> * -> *) (q :: * -> * -> *) a b.
    (forall x. p b x -> q a x) -> Rift p q a b
    Rift ((a -> b) -> q b x -> q a x
    forall (p :: * -> * -> *) a b c.
    Profunctor p =>
    (a -> b) -> p b c -> p a c
    lmap a -> b
    ca (q b x -> q a x) -> (p c x -> q b x) -> p c x -> q a x
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . Rift p q b c -> forall x. p c x -> q b x
    forall (p :: * -> * -> *) (q :: * -> * -> *) a b.
    Rift p q a b -> forall x. p b x -> q a x
    runRift Rift p q b c
    f)
      {-# INLINE lmap #-}
      rmap :: (b -> c) -> Rift p q a b -> Rift p q a c
    rmap bd :: b -> c
    bd f :: Rift p q a b
    f = (forall x. p c x -> q a x) -> Rift p q a c
    forall (p :: * -> * -> *) (q :: * -> * -> *) a b.
    (forall x. p b x -> q a x) -> Rift p q a b
    Rift (Rift p q a b -> forall x. p b x -> q a x
    forall (p :: * -> * -> *) (q :: * -> * -> *) a b.
    Rift p q a b -> forall x. p b x -> q a x
    runRift Rift p q a b
    f (p b x -> q a x) -> (p c x -> p b x) -> p c x -> q a x
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . (b -> c) -> p c x -> p b x
    forall (p :: * -> * -> *) a b c.
    Profunctor p =>
    (a -> b) -> p b c -> p a c
    lmap b -> c
    bd)
      {-# INLINE rmap #-}
      bd :: q b c
    bd #. :: q b c -> Rift p q a b -> Rift p q a c
    #. f :: Rift p q a b
    f = (forall x. p c x -> q a x) -> Rift p q a c
    forall (p :: * -> * -> *) (q :: * -> * -> *) a b.
    (forall x. p b x -> q a x) -> Rift p q a b
    Rift (\p :: p c x
    p -> Rift p q a b -> p b x -> q a x
    forall (p :: * -> * -> *) (q :: * -> * -> *) a b.
    Rift p q a b -> forall x. p b x -> q a x
    runRift Rift p q a b
    f (p c x
    p p c x -> q b c -> p b x
    forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
    (Profunctor p, Coercible b a) =>
    p b c -> q a b -> p a c
    .# q b c
    bd))
      {-# INLINE (#.) #-}
      f :: Rift p q b c
    f .# :: Rift p q b c -> q a b -> Rift p q a c
    .# ca :: q a b
    ca = (forall x. p c x -> q a x) -> Rift p q a c
    forall (p :: * -> * -> *) (q :: * -> * -> *) a b.
    (forall x. p b x -> q a x) -> Rift p q a b
    Rift (\p :: p c x
    p -> Rift p q b c -> p c x -> q b x
    forall (p :: * -> * -> *) (q :: * -> * -> *) a b.
    Rift p q a b -> forall x. p b x -> q a x
    runRift Rift p q b c
    f p c x
    p q b x -> q a b -> q a x
    forall (p :: * -> * -> *) a b c (q :: * -> * -> *).
    (Profunctor p, Coercible b a) =>
    p b c -> q a b -> p a c
    .# q a b
    ca)
      {-# INLINE (.#) #-}

    instance Profunctor p => Functor (Rift p q a) where
      fmap :: (a -> b) -> Rift p q a a -> Rift p q a b
    fmap bd :: a -> b
    bd f :: Rift p q a a
    f = (forall x. p b x -> q a x) -> Rift p q a b
    forall (p :: * -> * -> *) (q :: * -> * -> *) a b.
    (forall x. p b x -> q a x) -> Rift p q a b
    Rift (Rift p q a a -> forall x. p a x -> q a x
    forall (p :: * -> * -> *) (q :: * -> * -> *) a b.
    Rift p q a b -> forall x. p b x -> q a x
    runRift Rift p q a a
    f (p a x -> q a x) -> (p b x -> p a x) -> p b x -> q a x
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . (a -> b) -> p b x -> p a x
    forall (p :: * -> * -> *) a b c.
    Profunctor p =>
    (a -> b) -> p b c -> p a c
    lmap a -> b
    bd)
      {-# INLINE fmap #-}

    -- | @'Rift' p p@ forms a 'Monad' in the 'Profunctor' 2-category, which is isomorphic to a Haskell 'Category' instance.
    instance p ~ q => Category (Rift p q) where
      id :: Rift p q a a
    id = (forall x. p a x -> q a x) -> Rift p q a a
    forall (p :: * -> * -> *) (q :: * -> * -> *) a b.
    (forall x. p b x -> q a x) -> Rift p q a b
    Rift forall x. p a x -> q a x
    forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id
      {-# INLINE id #-}
      Rift f :: forall x. p c x -> q b x
    f . :: Rift p q b c -> Rift p q a b -> Rift p q a c
    . Rift g :: forall x. p b x -> q a x
    g = (forall x. p c x -> q a x) -> Rift p q a c
    forall (p :: * -> * -> *) (q :: * -> * -> *) a b.
    (forall x. p b x -> q a x) -> Rift p q a b
    Rift (q b x -> q a x
    forall x. p b x -> q a x
    g (q b x -> q a x) -> (q c x -> q b x) -> q c x -> q a x
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . q c x -> q b x
    forall x. p c x -> q b x
    f)
      {-# INLINE (.) #-}

    -- | The 2-morphism that defines a left Kan lift.
    --
    -- Note: When @p@ is right adjoint to @'Rift' p (->)@ then 'decomposeRift' is the 'counit' of the adjunction.
    decomposeRift :: Procompose p (Rift p q) :-> q
    decomposeRift :: Procompose p (Rift p q) a b -> q a b
    decomposeRift (Procompose p :: p x b
    p (Rift pq :: forall x. p x x -> q a x
    pq)) = p x b -> q a b
    forall x. p x x -> q a x
    pq p x b
    p
    {-# INLINE decomposeRift #-}

    instance ProfunctorAdjunction (Procompose p) (Rift p) where
      counit :: Procompose p (Rift p p) :-> p
    counit (Procompose p :: p x b
    p (Rift pq :: forall x. p x x -> p a x
    pq)) = p x b -> p a b
    forall x. p x x -> p a x
    pq p x b
    p
      unit :: p :-> Rift p (Procompose p p)
    unit q :: p a b
    q = (forall x. p b x -> Procompose p p a x)
    -> Rift p (Procompose p p) a b
    forall (p :: * -> * -> *) (q :: * -> * -> *) a b.
    (forall x. p b x -> q a x) -> Rift p q a b
    Rift ((forall x. p b x -> Procompose p p a x)
     -> Rift p (Procompose p p) a b)
    -> (forall x. p b x -> Procompose p p a x)
    -> Rift p (Procompose p p) a b
    forall a b. (a -> b) -> a -> b
    $ \p :: p b x
    p -> p b x -> p a b -> Procompose p p a x
    forall (p :: * -> * -> *) x c (q :: * -> * -> *) d.
    p x c -> q d x -> Procompose p q d c
    Procompose p b x
    p p a b
    q

    --instance (ProfunctorAdjunction f g, ProfunctorAdjunction f' g') => ProfunctorAdjunction (ProfunctorCompose f' f) (ProfunctorCompose g g') where

    ----------------------------------------------------------------------------
    -- * Monoids
    ----------------------------------------------------------------------------

    -- | a 'Category' that is also a 'Profunctor' is a 'Monoid' in @Prof@

    eta :: (Profunctor p, Category p) => (->) :-> p
    eta :: (->) :-> p
    eta f :: a -> b
    f = (a -> b) -> p a a -> p a b
    forall (p :: * -> * -> *) b c a.
    Profunctor p =>
    (b -> c) -> p a b -> p a c
    rmap a -> b
    f p a a
    forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id

    mu :: Category p => Procompose p p :-> p
    mu :: Procompose p p :-> p
    mu (Procompose f :: p x b
    f g :: p a x
    g) = p x b
    f p x b -> p a x -> p a b
    forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . p a x
    g