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