{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Monoidal.Distributive where

import Data.Bifunctor (bimap)
import Data.Kind (Type)
import Prelude (Either (..), const)
import Prelude qualified as P

import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), lmap, src, (:~>), type (+->))
import Proarrow.Helper.CCC
import Proarrow.Object.BinaryCoproduct (Coprod (..), HasBinaryCoproducts (..), HasCoproducts, copar)
import Proarrow.Object.BinaryProduct (Cartesian, fst', snd', PROD (..), Prod (..), diag)
import Proarrow.Object.Exponential (BiCCC)
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Coproduct ((:+:) (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Product ((:*:) (..))
import Proarrow.Profunctor.Star (Star (..))

class (MonoidalProfunctor p, MonoidalProfunctor (Coprod p)) => DistributiveProfunctor p
instance (MonoidalProfunctor p, MonoidalProfunctor (Coprod p)) => DistributiveProfunctor p

class (Monoidal k, HasCoproducts k, DistributiveProfunctor ((~>) :: CAT k)) => Distributive k where
  distL :: (Ob (a :: k), Ob b, Ob c) => (a ** (b || c)) ~> (a ** b || a ** c)
  distR :: (Ob (a :: k), Ob b, Ob c) => ((a || b) ** c) ~> (a ** c || b ** c)
  distL0 :: (Ob (a :: k)) => (a ** InitialObject) ~> InitialObject
  distR0 :: (Ob (a :: k)) => (InitialObject ** a) ~> InitialObject

instance Distributive Type where
  distL :: forall a b c.
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL (a
a, Either b c
e) = (b -> (a, b))
-> (c -> (a, c)) -> Either b c -> Either (a, b) (a, c)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: PRO Type Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (a
a,) (a
a,) Either b c
e
  distR :: forall a b c.
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR (Either a b
e, c
c) = (a -> (a, c))
-> (b -> (b, c)) -> Either a b -> Either (a, c) (b, c)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: PRO Type Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (,c
c) (,c
c) Either a b
e
  distL0 :: forall a. Ob a => (a ** InitialObject) ~> InitialObject
distL0 = (a ** InitialObject) ~> InitialObject
(a, Void) -> Void
forall a b. (a, b) -> b
P.snd
  distR0 :: forall a. Ob a => (InitialObject ** a) ~> InitialObject
distR0 = (InitialObject ** a) ~> InitialObject
(Void, a) -> Void
forall a b. (a, b) -> a
P.fst

instance Distributive () where
  distL :: forall (a :: ()) (b :: ()) (c :: ()).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL = (a ** (b || c)) ~> ((a ** b) || (a ** c))
Unit '() '()
U.Unit
  distR :: forall (a :: ()) (b :: ()) (c :: ()).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR = ((a || b) ** c) ~> ((a ** c) || (b ** c))
Unit '() '()
U.Unit
  distL0 :: forall (a :: ()). Ob a => (a ** InitialObject) ~> InitialObject
distL0 = (a ** InitialObject) ~> InitialObject
Unit '() '()
U.Unit
  distR0 :: forall (a :: ()). Ob a => (InitialObject ** a) ~> InitialObject
distR0 = (InitialObject ** a) ~> InitialObject
Unit '() '()
U.Unit

instance (BiCCC k) => Distributive (PROD k) where
  distL :: forall (a :: PROD k) (b :: PROD k) (c :: PROD k).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @(PR a) @(PR b) @(PR c) =
    ((UN 'PR a && (UN 'PR b || UN 'PR c))
 ~> ((UN 'PR a && UN 'PR b) || (UN 'PR a && UN 'PR c)))
-> Prod
     (~>)
     ('PR (UN 'PR a && (UN 'PR b || UN 'PR c)))
     ('PR ((UN 'PR a && UN 'PR b) || (UN 'PR a && UN 'PR c)))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod
      ( forall {k} (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
forall (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
toCCC @(F a * (F b + F c)) @((F a * F b) + (F a * F c))
          (((forall (x :: FK k).
  Cast
    x (TermF && ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c)))) =>
  x ~> ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
 -> (TermF && ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
    ~> (('F (UN 'PR a) * 'F (UN 'PR b))
        + ('F (UN 'PR a) * 'F (UN 'PR c))))
-> TermF
   ~> (('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c)))
       ~~> (('F (UN 'PR a) * 'F (UN 'PR b))
            + ('F (UN 'PR a) * 'F (UN 'PR c))))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
~> 'F (UN 'PR a)
a :& (TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
~> ('F (UN 'PR b) + 'F (UN 'PR c))
bc) -> ((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
 ~> ('F (UN 'PR b)
     ~~> ('F (UN 'PR a)
          --> (('F (UN 'PR a) * 'F (UN 'PR b))
               + ('F (UN 'PR a) * 'F (UN 'PR c))))))
-> ((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
    ~> ('F (UN 'PR c)
        ~~> ('F (UN 'PR a)
             --> (('F (UN 'PR a) * 'F (UN 'PR b))
                  + ('F (UN 'PR a) * 'F (UN 'PR c))))))
-> (TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
   ~> (('F (UN 'PR b) || 'F (UN 'PR c))
       ~~> ('F (UN 'PR a)
            --> (('F (UN 'PR a) * 'F (UN 'PR b))
                 + ('F (UN 'PR a) * 'F (UN 'PR c)))))
forall {k} (a :: k) (b :: k) (c :: k) (i :: k).
(HasBinaryCoproducts k, CCC k, Ob a, Ob b, Ob c) =>
(i ~> (a ~~> c)) -> (i ~> (b ~~> c)) -> i ~> ((a || b) ~~> c)
either (((forall (x :: FK k).
  Cast
    x
    ((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
     && 'F (UN 'PR b)) =>
  x ~> 'F (UN 'PR b))
 -> ((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
     && 'F (UN 'PR b))
    ~> ('F (UN 'PR a)
        --> (('F (UN 'PR a) * 'F (UN 'PR b))
             + ('F (UN 'PR a) * 'F (UN 'PR c)))))
-> (TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
   ~> ('F (UN 'PR b)
       ~~> ('F (UN 'PR a)
            --> (('F (UN 'PR a) * 'F (UN 'PR b))
                 + ('F (UN 'PR a) * 'F (UN 'PR c)))))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \forall (x :: FK k).
Cast
  x
  ((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
   && 'F (UN 'PR b)) =>
x ~> 'F (UN 'PR b)
b -> ((forall (x :: FK k).
  Cast
    x
    (((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
      * 'F (UN 'PR b))
     && 'F (UN 'PR a)) =>
  x ~> 'F (UN 'PR a))
 -> (((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
      * 'F (UN 'PR b))
     && 'F (UN 'PR a))
    ~> (('F (UN 'PR a) * 'F (UN 'PR b))
        + ('F (UN 'PR a) * 'F (UN 'PR c))))
-> ((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
    * 'F (UN 'PR b))
   ~> ('F (UN 'PR a)
       ~~> (('F (UN 'PR a) * 'F (UN 'PR b))
            + ('F (UN 'PR a) * 'F (UN 'PR c))))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \forall (x :: FK k).
Cast
  x
  (((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
    * 'F (UN 'PR b))
   && 'F (UN 'PR a)) =>
x ~> 'F (UN 'PR a)
a' -> ((((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
   * 'F (UN 'PR b))
  * 'F (UN 'PR a))
 ~> ('F (UN 'PR a) * 'F (UN 'PR b)))
-> (((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
     * 'F (UN 'PR b))
    * 'F (UN 'PR a))
   ~> (('F (UN 'PR a) * 'F (UN 'PR b))
       || ('F (UN 'PR a) * 'F (UN 'PR c)))
forall {k} (a :: k) (b :: k) (i :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(i ~> a) -> i ~> (a || b)
left ((((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
  * 'F (UN 'PR b))
 * 'F (UN 'PR a))
~> 'F (UN 'PR a)
forall (x :: FK k).
Cast
  x
  (((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
    * 'F (UN 'PR b))
   && 'F (UN 'PR a)) =>
x ~> 'F (UN 'PR a)
a' ((((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
   * 'F (UN 'PR b))
  * 'F (UN 'PR a))
 ~> 'F (UN 'PR a))
-> ((((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
      * 'F (UN 'PR b))
     * 'F (UN 'PR a))
    ~> 'F (UN 'PR b))
-> (((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
     * 'F (UN 'PR b))
    * 'F (UN 'PR a))
   ~> ('F (UN 'PR a) && 'F (UN 'PR b))
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob a, Ob b) =>
(i ~> a) -> (i ~> b) -> i ~> (a && b)
:& (((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
  * 'F (UN 'PR b))
 * 'F (UN 'PR a))
~> 'F (UN 'PR b)
forall (x :: FK k).
Cast
  x
  ((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
   && 'F (UN 'PR b)) =>
x ~> 'F (UN 'PR b)
b)) (((forall (x :: FK k).
  Cast
    x
    ((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
     && 'F (UN 'PR c)) =>
  x ~> 'F (UN 'PR c))
 -> ((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
     && 'F (UN 'PR c))
    ~> ('F (UN 'PR a)
        --> (('F (UN 'PR a) * 'F (UN 'PR b))
             + ('F (UN 'PR a) * 'F (UN 'PR c)))))
-> (TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
   ~> ('F (UN 'PR c)
       ~~> ('F (UN 'PR a)
            --> (('F (UN 'PR a) * 'F (UN 'PR b))
                 + ('F (UN 'PR a) * 'F (UN 'PR c)))))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \forall (x :: FK k).
Cast
  x
  ((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
   && 'F (UN 'PR c)) =>
x ~> 'F (UN 'PR c)
c -> ((forall (x :: FK k).
  Cast
    x
    (((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
      * 'F (UN 'PR c))
     && 'F (UN 'PR a)) =>
  x ~> 'F (UN 'PR a))
 -> (((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
      * 'F (UN 'PR c))
     && 'F (UN 'PR a))
    ~> (('F (UN 'PR a) * 'F (UN 'PR b))
        + ('F (UN 'PR a) * 'F (UN 'PR c))))
-> ((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
    * 'F (UN 'PR c))
   ~> ('F (UN 'PR a)
       ~~> (('F (UN 'PR a) * 'F (UN 'PR b))
            + ('F (UN 'PR a) * 'F (UN 'PR c))))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \forall (x :: FK k).
Cast
  x
  (((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
    * 'F (UN 'PR c))
   && 'F (UN 'PR a)) =>
x ~> 'F (UN 'PR a)
a' -> ((((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
   * 'F (UN 'PR c))
  * 'F (UN 'PR a))
 ~> ('F (UN 'PR a) * 'F (UN 'PR c)))
-> (((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
     * 'F (UN 'PR c))
    * 'F (UN 'PR a))
   ~> (('F (UN 'PR a) * 'F (UN 'PR b))
       || ('F (UN 'PR a) * 'F (UN 'PR c)))
forall {k} (a :: k) (b :: k) (i :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(i ~> b) -> i ~> (a || b)
right ((((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
  * 'F (UN 'PR c))
 * 'F (UN 'PR a))
~> 'F (UN 'PR a)
forall (x :: FK k).
Cast
  x
  (((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
    * 'F (UN 'PR c))
   && 'F (UN 'PR a)) =>
x ~> 'F (UN 'PR a)
a' ((((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
   * 'F (UN 'PR c))
  * 'F (UN 'PR a))
 ~> 'F (UN 'PR a))
-> ((((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
      * 'F (UN 'PR c))
     * 'F (UN 'PR a))
    ~> 'F (UN 'PR c))
-> (((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
     * 'F (UN 'PR c))
    * 'F (UN 'PR a))
   ~> ('F (UN 'PR a) && 'F (UN 'PR c))
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob a, Ob b) =>
(i ~> a) -> (i ~> b) -> i ~> (a && b)
:& (((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
  * 'F (UN 'PR c))
 * 'F (UN 'PR a))
~> 'F (UN 'PR c)
forall (x :: FK k).
Cast
  x
  ((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
   && 'F (UN 'PR c)) =>
x ~> 'F (UN 'PR c)
c)) ((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
 ~> (('F (UN 'PR b) + 'F (UN 'PR c))
     ~~> ('F (UN 'PR a)
          --> (('F (UN 'PR a) * 'F (UN 'PR b))
               + ('F (UN 'PR a) * 'F (UN 'PR c))))))
-> ((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
    ~> ('F (UN 'PR b) + 'F (UN 'PR c)))
-> (TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
   ~> ('F (UN 'PR a)
       --> (('F (UN 'PR a) * 'F (UN 'PR b))
            + ('F (UN 'PR a) * 'F (UN 'PR c))))
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob b) =>
(i ~> (a ~~> b)) -> (i ~> a) -> i ~> b
$ (TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
~> ('F (UN 'PR b) + 'F (UN 'PR c))
bc ((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
 ~> ('F (UN 'PR a)
     ~~> (('F (UN 'PR a) * 'F (UN 'PR b))
          + ('F (UN 'PR a) * 'F (UN 'PR c)))))
-> ((TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
    ~> 'F (UN 'PR a))
-> (TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
   ~> (('F (UN 'PR a) * 'F (UN 'PR b))
       + ('F (UN 'PR a) * 'F (UN 'PR c)))
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob b) =>
(i ~> (a ~~> b)) -> (i ~> a) -> i ~> b
$ (TermF * ('F (UN 'PR a) * ('F (UN 'PR b) + 'F (UN 'PR c))))
~> 'F (UN 'PR a)
a)
      )
  distR :: forall (a :: PROD k) (b :: PROD k) (c :: PROD k).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @(PR a) @(PR b) @(PR c) =
    (((UN 'PR a || UN 'PR b) && UN 'PR c)
 ~> ((UN 'PR a && UN 'PR c) || (UN 'PR b && UN 'PR c)))
-> Prod
     (~>)
     ('PR ((UN 'PR a || UN 'PR b) && UN 'PR c))
     ('PR ((UN 'PR a && UN 'PR c) || (UN 'PR b && UN 'PR c)))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod
      ( forall {k} (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
forall (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
toCCC @((F a + F b) * F c) @((F a * F c) + (F b * F c))
          (((forall (x :: FK k).
  Cast
    x (TermF && (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c))) =>
  x ~> (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
 -> (TermF && (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
    ~> (('F (UN 'PR a) * 'F (UN 'PR c))
        + ('F (UN 'PR b) * 'F (UN 'PR c))))
-> TermF
   ~> ((('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c))
       ~~> (('F (UN 'PR a) * 'F (UN 'PR c))
            + ('F (UN 'PR b) * 'F (UN 'PR c))))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
~> ('F (UN 'PR a) + 'F (UN 'PR b))
ab :& (TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
~> 'F (UN 'PR c)
c) -> ((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
 ~> ('F (UN 'PR a)
     ~~> ('F (UN 'PR c)
          --> (('F (UN 'PR a) * 'F (UN 'PR c))
               + ('F (UN 'PR b) * 'F (UN 'PR c))))))
-> ((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
    ~> ('F (UN 'PR b)
        ~~> ('F (UN 'PR c)
             --> (('F (UN 'PR a) * 'F (UN 'PR c))
                  + ('F (UN 'PR b) * 'F (UN 'PR c))))))
-> (TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
   ~> (('F (UN 'PR a) || 'F (UN 'PR b))
       ~~> ('F (UN 'PR c)
            --> (('F (UN 'PR a) * 'F (UN 'PR c))
                 + ('F (UN 'PR b) * 'F (UN 'PR c)))))
forall {k} (a :: k) (b :: k) (c :: k) (i :: k).
(HasBinaryCoproducts k, CCC k, Ob a, Ob b, Ob c) =>
(i ~> (a ~~> c)) -> (i ~> (b ~~> c)) -> i ~> ((a || b) ~~> c)
either (((forall (x :: FK k).
  Cast
    x
    ((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
     && 'F (UN 'PR a)) =>
  x ~> 'F (UN 'PR a))
 -> ((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
     && 'F (UN 'PR a))
    ~> ('F (UN 'PR c)
        --> (('F (UN 'PR a) * 'F (UN 'PR c))
             + ('F (UN 'PR b) * 'F (UN 'PR c)))))
-> (TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
   ~> ('F (UN 'PR a)
       ~~> ('F (UN 'PR c)
            --> (('F (UN 'PR a) * 'F (UN 'PR c))
                 + ('F (UN 'PR b) * 'F (UN 'PR c)))))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \forall (x :: FK k).
Cast
  x
  ((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
   && 'F (UN 'PR a)) =>
x ~> 'F (UN 'PR a)
a -> ((forall (x :: FK k).
  Cast
    x
    (((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
      * 'F (UN 'PR a))
     && 'F (UN 'PR c)) =>
  x ~> 'F (UN 'PR c))
 -> (((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
      * 'F (UN 'PR a))
     && 'F (UN 'PR c))
    ~> (('F (UN 'PR a) * 'F (UN 'PR c))
        + ('F (UN 'PR b) * 'F (UN 'PR c))))
-> ((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
    * 'F (UN 'PR a))
   ~> ('F (UN 'PR c)
       ~~> (('F (UN 'PR a) * 'F (UN 'PR c))
            + ('F (UN 'PR b) * 'F (UN 'PR c))))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \forall (x :: FK k).
Cast
  x
  (((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
    * 'F (UN 'PR a))
   && 'F (UN 'PR c)) =>
x ~> 'F (UN 'PR c)
c' -> ((((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
   * 'F (UN 'PR a))
  * 'F (UN 'PR c))
 ~> ('F (UN 'PR a) * 'F (UN 'PR c)))
-> (((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
     * 'F (UN 'PR a))
    * 'F (UN 'PR c))
   ~> (('F (UN 'PR a) * 'F (UN 'PR c))
       || ('F (UN 'PR b) * 'F (UN 'PR c)))
forall {k} (a :: k) (b :: k) (i :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(i ~> a) -> i ~> (a || b)
left ((((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
  * 'F (UN 'PR a))
 * 'F (UN 'PR c))
~> 'F (UN 'PR a)
forall (x :: FK k).
Cast
  x
  ((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
   && 'F (UN 'PR a)) =>
x ~> 'F (UN 'PR a)
a ((((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
   * 'F (UN 'PR a))
  * 'F (UN 'PR c))
 ~> 'F (UN 'PR a))
-> ((((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
      * 'F (UN 'PR a))
     * 'F (UN 'PR c))
    ~> 'F (UN 'PR c))
-> (((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
     * 'F (UN 'PR a))
    * 'F (UN 'PR c))
   ~> ('F (UN 'PR a) && 'F (UN 'PR c))
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob a, Ob b) =>
(i ~> a) -> (i ~> b) -> i ~> (a && b)
:& (((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
  * 'F (UN 'PR a))
 * 'F (UN 'PR c))
~> 'F (UN 'PR c)
forall (x :: FK k).
Cast
  x
  (((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
    * 'F (UN 'PR a))
   && 'F (UN 'PR c)) =>
x ~> 'F (UN 'PR c)
c')) (((forall (x :: FK k).
  Cast
    x
    ((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
     && 'F (UN 'PR b)) =>
  x ~> 'F (UN 'PR b))
 -> ((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
     && 'F (UN 'PR b))
    ~> ('F (UN 'PR c)
        --> (('F (UN 'PR a) * 'F (UN 'PR c))
             + ('F (UN 'PR b) * 'F (UN 'PR c)))))
-> (TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
   ~> ('F (UN 'PR b)
       ~~> ('F (UN 'PR c)
            --> (('F (UN 'PR a) * 'F (UN 'PR c))
                 + ('F (UN 'PR b) * 'F (UN 'PR c)))))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \forall (x :: FK k).
Cast
  x
  ((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
   && 'F (UN 'PR b)) =>
x ~> 'F (UN 'PR b)
b -> ((forall (x :: FK k).
  Cast
    x
    (((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
      * 'F (UN 'PR b))
     && 'F (UN 'PR c)) =>
  x ~> 'F (UN 'PR c))
 -> (((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
      * 'F (UN 'PR b))
     && 'F (UN 'PR c))
    ~> (('F (UN 'PR a) * 'F (UN 'PR c))
        + ('F (UN 'PR b) * 'F (UN 'PR c))))
-> ((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
    * 'F (UN 'PR b))
   ~> ('F (UN 'PR c)
       ~~> (('F (UN 'PR a) * 'F (UN 'PR c))
            + ('F (UN 'PR b) * 'F (UN 'PR c))))
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \forall (x :: FK k).
Cast
  x
  (((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
    * 'F (UN 'PR b))
   && 'F (UN 'PR c)) =>
x ~> 'F (UN 'PR c)
c' -> ((((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
   * 'F (UN 'PR b))
  * 'F (UN 'PR c))
 ~> ('F (UN 'PR b) * 'F (UN 'PR c)))
-> (((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
     * 'F (UN 'PR b))
    * 'F (UN 'PR c))
   ~> (('F (UN 'PR a) * 'F (UN 'PR c))
       || ('F (UN 'PR b) * 'F (UN 'PR c)))
forall {k} (a :: k) (b :: k) (i :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(i ~> b) -> i ~> (a || b)
right ((((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
  * 'F (UN 'PR b))
 * 'F (UN 'PR c))
~> 'F (UN 'PR b)
forall (x :: FK k).
Cast
  x
  ((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
   && 'F (UN 'PR b)) =>
x ~> 'F (UN 'PR b)
b ((((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
   * 'F (UN 'PR b))
  * 'F (UN 'PR c))
 ~> 'F (UN 'PR b))
-> ((((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
      * 'F (UN 'PR b))
     * 'F (UN 'PR c))
    ~> 'F (UN 'PR c))
-> (((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
     * 'F (UN 'PR b))
    * 'F (UN 'PR c))
   ~> ('F (UN 'PR b) && 'F (UN 'PR c))
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob a, Ob b) =>
(i ~> a) -> (i ~> b) -> i ~> (a && b)
:& (((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
  * 'F (UN 'PR b))
 * 'F (UN 'PR c))
~> 'F (UN 'PR c)
forall (x :: FK k).
Cast
  x
  (((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
    * 'F (UN 'PR b))
   && 'F (UN 'PR c)) =>
x ~> 'F (UN 'PR c)
c')) ((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
 ~> (('F (UN 'PR a) + 'F (UN 'PR b))
     ~~> ('F (UN 'PR c)
          --> (('F (UN 'PR a) * 'F (UN 'PR c))
               + ('F (UN 'PR b) * 'F (UN 'PR c))))))
-> ((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
    ~> ('F (UN 'PR a) + 'F (UN 'PR b)))
-> (TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
   ~> ('F (UN 'PR c)
       --> (('F (UN 'PR a) * 'F (UN 'PR c))
            + ('F (UN 'PR b) * 'F (UN 'PR c))))
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob b) =>
(i ~> (a ~~> b)) -> (i ~> a) -> i ~> b
$ (TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
~> ('F (UN 'PR a) + 'F (UN 'PR b))
ab ((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
 ~> ('F (UN 'PR c)
     ~~> (('F (UN 'PR a) * 'F (UN 'PR c))
          + ('F (UN 'PR b) * 'F (UN 'PR c)))))
-> ((TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
    ~> 'F (UN 'PR c))
-> (TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
   ~> (('F (UN 'PR a) * 'F (UN 'PR c))
       + ('F (UN 'PR b) * 'F (UN 'PR c)))
forall {k} (i :: k) (a :: k) (b :: k).
(CCC k, Ob b) =>
(i ~> (a ~~> b)) -> (i ~> a) -> i ~> b
$ (TermF * (('F (UN 'PR a) + 'F (UN 'PR b)) * 'F (UN 'PR c)))
~> 'F (UN 'PR c)
c)
      )
  distL0 :: forall (a :: PROD k). Ob a => (a ** InitialObject) ~> InitialObject
distL0 @(PR a) = ((UN 'PR a && InitialObject) ~> InitialObject)
-> Prod (~>) ('PR (UN 'PR a && InitialObject)) ('PR InitialObject)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod (forall {k} (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
forall (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
toCCC @(F a * InitF) @InitF (((forall (x :: FK k).
  Cast x (TermF && ('F (UN 'PR a) * InitF)) =>
  x ~> ('F (UN 'PR a) * InitF))
 -> (TermF && ('F (UN 'PR a) * InitF)) ~> InitF)
-> TermF ~> (('F (UN 'PR a) * InitF) ~~> InitF)
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \((TermF * ('F (UN 'PR a) * InitF)) ~> 'F (UN 'PR a)
_ :& (TermF * ('F (UN 'PR a) * InitF)) ~> InitF
v) -> (TermF && ('F (UN 'PR a) * InitF)) ~> InitF
(TermF * ('F (UN 'PR a) * InitF)) ~> InitF
v))
  distR0 :: forall (a :: PROD k). Ob a => (InitialObject ** a) ~> InitialObject
distR0 @(PR a) = ((InitialObject && UN 'PR a) ~> InitialObject)
-> Prod (~>) ('PR (InitialObject && UN 'PR a)) ('PR InitialObject)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod (forall {k} (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
forall (a :: FK k) (b :: FK k).
(BiCCC k, Ob a, Ob b) =>
(TermF ~> (a --> b)) -> FromFree a ~> FromFree b
toCCC @(InitF * F a) @InitF (((forall (x :: FK k).
  Cast x (TermF && (InitF * 'F (UN 'PR a))) =>
  x ~> (InitF * 'F (UN 'PR a)))
 -> (TermF && (InitF * 'F (UN 'PR a))) ~> InitF)
-> TermF ~> ((InitF * 'F (UN 'PR a)) ~~> InitF)
forall {k} (a :: k) (b :: k) (i :: k).
(CCC k, Ob i, Ob a, Ob b) =>
((forall (x :: k). Cast x (i && a) => x ~> a) -> (i && a) ~> b)
-> i ~> (a ~~> b)
lam \((TermF * (InitF * 'F (UN 'PR a))) ~> InitF
v :& (TermF * (InitF * 'F (UN 'PR a))) ~> 'F (UN 'PR a)
_) -> (TermF && (InitF * 'F (UN 'PR a))) ~> InitF
(TermF * (InitF * 'F (UN 'PR a))) ~> InitF
v))

class (Profunctor t) => Traversable t where
  traverse :: (DistributiveProfunctor p) => t :.: p :~> p :.: t

instance (CategoryOf k) => Traversable (Id :: k +-> k) where
  traverse :: forall (p :: k +-> k).
DistributiveProfunctor p =>
(Id :.: p) :~> (p :.: Id)
traverse (Id a ~> b
f :.: p b b
p) = (a ~> b) -> p b b -> p a b
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> b
f p b b
p p a b -> Id b b -> (:.:) p Id a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (b ~> b) -> Id b b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id ((Ob b, Ob b) => (:.:) p Id a b) -> p b b -> (:.:) p Id a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p b b
p

instance Traversable (->) where
  traverse :: forall (p :: PRO Type Type).
DistributiveProfunctor p =>
((->) :.: p) :~> (p :.: (->))
traverse (a -> b
f :.: p b b
p) = (a ~> b) -> p b b -> p a b
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> b
a -> b
f p b b
p p a b -> (b -> b) -> (:.:) p (->) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: b -> b
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id

instance (Traversable p, Traversable q) => Traversable (p :.: q) where
  traverse :: forall (p :: j +-> j).
DistributiveProfunctor p =>
((p :.: q) :.: p) :~> (p :.: (p :.: q))
traverse ((p a b
p :.: q b b
q) :.: p b b
r) = case (:.:) q p b b -> (:.:) p q b b
(q :.: p) :~> (p :.: q)
forall {j} (t :: PRO j j) (p :: PRO j j).
(Traversable t, DistributiveProfunctor p) =>
(t :.: p) :~> (p :.: t)
forall (p :: j +-> j).
DistributiveProfunctor p =>
(q :.: p) :~> (p :.: q)
traverse (q b b
q q b b -> p b b -> (:.:) q p b b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p b b
r) of
    p b b
r' :.: q b b
q' -> case (:.:) p p a b -> (:.:) p p a b
(p :.: p) :~> (p :.: p)
forall {j} (t :: PRO j j) (p :: PRO j j).
(Traversable t, DistributiveProfunctor p) =>
(t :.: p) :~> (p :.: t)
forall (p :: j +-> j).
DistributiveProfunctor p =>
(p :.: p) :~> (p :.: p)
traverse (p a b
p p a b -> p b b -> (:.:) p p a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p b b
r') of
      p a b
r'' :.: p b b
p' -> p a b
r'' p a b -> (:.:) p q b b -> (:.:) p (p :.: q) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (p b b
p' p b b -> q b b -> (:.:) p q b b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: q b b
q')

instance (Cartesian k, Traversable p, Traversable q) => Traversable ((p :: k +-> k) :*: q) where
  traverse :: forall (p :: k +-> k).
DistributiveProfunctor p =>
((p :*: q) :.: p) :~> (p :.: (p :*: q))
traverse ((p a b
p :*: q a b
q) :.: p b b
r) = case ((:.:) p p a b -> (:.:) p p a b
(p :.: p) :~> (p :.: p)
forall {j} (t :: PRO j j) (p :: PRO j j).
(Traversable t, DistributiveProfunctor p) =>
(t :.: p) :~> (p :.: t)
forall (p :: k +-> k).
DistributiveProfunctor p =>
(p :.: p) :~> (p :.: p)
traverse (p a b
p p a b -> p b b -> (:.:) p p a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p b b
r), (:.:) q p a b -> (:.:) p q a b
(q :.: p) :~> (p :.: q)
forall {j} (t :: PRO j j) (p :: PRO j j).
(Traversable t, DistributiveProfunctor p) =>
(t :.: p) :~> (p :.: t)
forall (p :: k +-> k).
DistributiveProfunctor p =>
(q :.: p) :~> (p :.: q)
traverse (q a b
q q a b -> p b b -> (:.:) q p a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p b b
r)) of
    (p a b
r' :.: p b b
p', p a b
r'' :.: q b b
q') -> (a ~> (a && a)) -> p (a && a) (b ** b) -> p a (b ** b)
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> (a && a)
forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
diag (p a b
r' p a b -> p a b -> p (a ** a) (b ** b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` p a b
r'') p a (b ** b) -> (:*:) p q (b ** b) b -> (:.:) p (p :*: q) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (((b ** b) ~> b) -> p b b -> p (b ** b) b
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap ((b ~> b) -> Obj b -> (b && b) ~> b
forall {k} (a :: k) (a' :: k) (b :: k).
HasBinaryProducts k =>
(a ~> a') -> Obj b -> (a && b) ~> a'
fst' (p b b -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src p b b
p') (q b b -> Obj b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src q b b
q')) p b b
p' p (b ** b) b -> q (b ** b) b -> (:*:) p q (b ** b) b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (q :: PRO j k).
p a b -> q a b -> (:*:) p q a b
:*: ((b ** b) ~> b) -> q b b -> q (b ** b) b
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap ((b ~> b) -> Obj b -> (b && b) ~> b
forall {k} (a :: k) (b :: k) (b' :: k).
HasBinaryProducts k =>
Obj a -> (b ~> b') -> (a && b) ~> b'
snd' (p b b -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src p b b
p') (q b b -> Obj b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src q b b
q')) q b b
q') ((Ob a, Ob b) => (:.:) p (p :*: q) a b)
-> p a b -> (:.:) p (p :*: q) a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

instance (Traversable p, Traversable q) => Traversable (p :+: q) where
  traverse :: forall (p :: j +-> j).
DistributiveProfunctor p =>
((p :+: q) :.: p) :~> (p :.: (p :+: q))
traverse (InjL p a b
p :.: p b b
r) = case (:.:) p p a b -> (:.:) p p a b
(p :.: p) :~> (p :.: p)
forall {j} (t :: PRO j j) (p :: PRO j j).
(Traversable t, DistributiveProfunctor p) =>
(t :.: p) :~> (p :.: t)
forall (p :: j +-> j).
DistributiveProfunctor p =>
(p :.: p) :~> (p :.: p)
traverse (p a b
p p a b -> p b b -> (:.:) p p a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p b b
r) of p a b
r' :.: p b b
p' -> p a b
r' p a b -> (:+:) p q b b -> (:.:) p (p :+: q) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p b b -> (:+:) p q b b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (q :: PRO j k).
p a b -> (:+:) p q a b
InjL p b b
p'
  traverse (InjR q a b
q :.: p b b
r) = case (:.:) q p a b -> (:.:) p q a b
(q :.: p) :~> (p :.: q)
forall {j} (t :: PRO j j) (p :: PRO j j).
(Traversable t, DistributiveProfunctor p) =>
(t :.: p) :~> (p :.: t)
forall (p :: j +-> j).
DistributiveProfunctor p =>
(q :.: p) :~> (p :.: q)
traverse (q a b
q q a b -> p b b -> (:.:) q p a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p b b
r) of p a b
r' :.: q b b
q' -> p a b
r' p a b -> (:+:) p q b b -> (:.:) p (p :+: q) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: q b b -> (:+:) p q b b
forall {j} {k} (q :: PRO j k) (a :: j) (b :: k) (p :: PRO j k).
q a b -> (:+:) p q a b
InjR q b b
q'

instance Traversable (Star P.Maybe) where
  traverse :: forall (p :: PRO Type Type).
DistributiveProfunctor p =>
(Star Maybe :.: p) :~> (p :.: Star Maybe)
traverse (Star a ~> Maybe b
a2mb :.: p b b
p) = (a ~> Maybe b) -> p (Maybe b) (Maybe b) -> p a (Maybe b)
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> Maybe b
a2mb p (Maybe b) (Maybe b)
go p a (Maybe b) -> Star Maybe (Maybe b) b -> (:.:) p (Star Maybe) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (Maybe b ~> Maybe b) -> Star Maybe (Maybe b) b
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star Maybe b ~> Maybe b
Maybe b -> Maybe b
forall a. a -> a
P.id
    where
      go :: p (Maybe b) (Maybe b)
go =
        (Maybe b ~> Either () b)
-> (Either () b ~> Maybe b)
-> p (Either () b) (Either () b)
-> p (Maybe b) (Maybe b)
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap
          (Either () b -> (b -> Either () b) -> Maybe b -> Either () b
forall b a. b -> (a -> b) -> Maybe a -> b
P.maybe (() -> Either () b
forall a b. a -> Either a b
Left ()) b -> Either () b
forall a b. b -> Either a b
Right)
          (Maybe b -> () -> Maybe b
forall a b. a -> b -> a
const Maybe b
forall a. Maybe a
P.Nothing (() ~> Maybe b) -> (b ~> Maybe b) -> (() || b) ~> Maybe b
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall x a y. (x ~> a) -> (y ~> a) -> (x || y) ~> a
||| b ~> Maybe b
b -> Maybe b
forall a. a -> Maybe a
P.Just)
          (p () ()
p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0 p () () -> p b b -> p (() || b) (() || b)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) (c :: k2)
       (d :: k1).
MonoidalProfunctor (Coprod p) =>
p a b -> p c d -> p (a || c) (b || d)
`copar` p b b
p)

instance Traversable (Star []) where
  traverse :: forall (p :: PRO Type Type).
DistributiveProfunctor p =>
(Star [] :.: p) :~> (p :.: Star [])
traverse (Star a ~> [b]
a2bs :.: p b b
p) = (a ~> [b]) -> p [b] [b] -> p a [b]
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> [b]
a2bs p [b] [b]
go p a [b] -> Star [] [b] b -> (:.:) p (Star []) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: ([b] ~> [b]) -> Star [] [b] b
forall {k1} {k2} (b :: k1) (a :: k2) (f :: k1 -> k2).
Ob b =>
(a ~> f b) -> Star f a b
Star [b] ~> [b]
[b] -> [b]
forall a. a -> a
P.id
    where
      go :: p [b] [b]
go =
        ([b] ~> Either () (b, [b]))
-> (Either () (b, [b]) ~> [b])
-> p (Either () (b, [b])) (Either () (b, [b]))
-> p [b] [b]
forall c a b d. (c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap
          (\[b]
l -> case [b]
l of [] -> () -> Either () (b, [b])
forall a b. a -> Either a b
Left (); (b
x : [b]
xs) -> (b, [b]) -> Either () (b, [b])
forall a b. b -> Either a b
Right (b
x, [b]
xs))
          ([b] -> () -> [b]
forall a b. a -> b -> a
const [] (() ~> [b]) -> ((b, [b]) ~> [b]) -> (() || (b, [b])) ~> [b]
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall x a y. (x ~> a) -> (y ~> a) -> (x || y) ~> a
||| \(b
x, [b]
xs) -> b
x b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b]
xs)
          (p () ()
p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0 p () ()
-> p (b, [b]) (b, [b]) -> p (() || (b, [b])) (() || (b, [b]))
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) (c :: k2)
       (d :: k1).
MonoidalProfunctor (Coprod p) =>
p a b -> p c d -> p (a || c) (b || d)
`copar` (p b b
p p b b -> p [b] [b] -> p (b ** [b]) (b ** [b])
forall x1 x2 y1 y2. p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` p [b] [b]
go))