{-# 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 (..))
import Proarrow.Object.BinaryCoproduct (Coprod (..), HasBinaryCoproducts (..), HasCoproducts)
import Proarrow.Object.BinaryProduct (PROD (..), Prod (..))
import Proarrow.Object.Exponential (BiCCC)
import Proarrow.Helper.CCC
import Proarrow.Object.Initial (HasInitialObject (..))

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

copar0 :: (DistributiveProfunctor p) => p InitialObject InitialObject
copar0 :: forall {j} {k} (p :: j +-> k).
DistributiveProfunctor p =>
p InitialObject InitialObject
copar0 = Coprod p ('COPR InitialObject) ('COPR InitialObject)
-> p InitialObject InitialObject
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Coprod p ('COPR a) ('COPR b) -> p a b
unCoprod Coprod p Unit Unit
Coprod p ('COPR InitialObject) ('COPR InitialObject)
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0

copar :: (DistributiveProfunctor p) => p a b -> p c d -> p (a || c) (b || d)
copar :: forall {k} {k} (p :: k +-> k) (a :: k) (b :: k) (c :: k) (d :: k).
DistributiveProfunctor p =>
p a b -> p c d -> p (a || c) (b || d)
copar p a b
p p c d
q = Coprod p ('COPR (a || c)) ('COPR (b || d)) -> p (a || c) (b || d)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Coprod p ('COPR a) ('COPR b) -> p a b
unCoprod (p a b -> Coprod p ('COPR a) ('COPR b)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod p a b
p Coprod p ('COPR a) ('COPR b)
-> Coprod p ('COPR c) ('COPR d)
-> Coprod p ('COPR a ** 'COPR c) ('COPR b ** 'COPR d)
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)
forall (x1 :: COPROD k) (x2 :: COPROD k) (y1 :: COPROD k)
       (y2 :: COPROD k).
Coprod p x1 x2 -> Coprod p y1 y2 -> Coprod p (x1 ** y1) (x2 ** y2)
`par` p c d -> Coprod p ('COPR c) ('COPR d)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Coprod p ('COPR a1) ('COPR b1)
Coprod p c d
q)

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))

travList :: (DistributiveProfunctor p) => p a b -> p [a] [b]
travList :: forall (p :: PRO Type Type) a b.
DistributiveProfunctor p =>
p a b -> p [a] [b]
travList p a b
p = p [a] [b]
go
  where
    go :: p [a] [b]
go =
      ([a] ~> Either () (a, [a]))
-> (Either () (b, [b]) ~> [b])
-> p (Either () (a, [a])) (Either () (b, [b]))
-> p [a] [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
        (\[a]
l -> case [a]
l of [] -> () -> Either () (a, [a])
forall a b. a -> Either a b
Left (); (a
x : [a]
xs) -> (a, [a]) -> Either () (a, [a])
forall a b. b -> Either a b
Right (a
x, [a]
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 (a, [a]) (b, [b]) -> p (() || (a, [a])) (() || (b, [b]))
forall {k} {k} (p :: k +-> k) (a :: k) (b :: k) (c :: k) (d :: k).
DistributiveProfunctor p =>
p a b -> p c d -> p (a || c) (b || d)
`copar` (p a b
p p a b -> p [a] [b] -> p (a ** [a]) (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 [a] [b]
go))