{-# LANGUAGE AllowAmbiguousTypes #-} module Proarrow.Category.Monoidal.Distributive where import Data.Bifunctor (bimap) import Data.Kind (Constraint, Type) import Prelude qualified as P import Proarrow.Category.Instance.Unit qualified as U import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..)) import Proarrow.Category.Monoidal.Action (SelfAction, Strong (..)) import Proarrow.Core ( CAT , CategoryOf (..) , Profunctor (..) , Promonad (..) , lmap , rmap , src , tgt , (:~>) , type (+->) ) import Proarrow.Helper.CCC import Proarrow.Object.BinaryCoproduct (Coprod (..), HasBinaryCoproducts (..), HasCoproducts, codiag, copar, lft', rgt') import Proarrow.Object.BinaryProduct (Cartesian, PROD (..), Prod (..), diag, fst', snd', HasBinaryProducts (..)) 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 ((:*:) (..)) class (MonoidalProfunctor p, MonoidalProfunctor (Coprod p)) => DistributiveProfunctor p instance (MonoidalProfunctor p, MonoidalProfunctor (Coprod p)) => DistributiveProfunctor p class (Monoidal k, HasCoproducts k, DistributiveProfunctor (Id :: 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 :: Type -> 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 :: Type -> 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 (a :: k) (b :: k) (c :: k). (BiCCC k, Ob a, Ob b, Ob c) => (a && (b || c)) ~> ((a && b) || (a && c)) forall {k} (a :: k) (b :: k) (c :: k). (BiCCC k, Ob a, Ob b, Ob c) => (a && (b || c)) ~> ((a && b) || (a && c)) distLProd @a @b @c) 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 (a :: k) (b :: k) (c :: k). (BiCCC k, Ob a, Ob b, Ob c) => ((a || b) && c) ~> ((a && c) || (b && c)) forall {k} (a :: k) (b :: k) (c :: k). (BiCCC k, Ob a, Ob b, Ob c) => ((a || b) && c) ~> ((a && c) || (b && c)) distRProd @a @b @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)) distLProd :: forall {k} (a :: k) (b :: k) (c :: k). (BiCCC k, Ob a, Ob b, Ob c) => (a && (b || c)) ~> (a && b || a && c) distLProd :: forall {k} (a :: k) (b :: k) (c :: k). (BiCCC k, Ob a, Ob b, Ob c) => (a && (b || c)) ~> ((a && b) || (a && c)) distLProd = 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 a * ('F b + 'F c))) => x ~> ('F a * ('F b + 'F c))) -> (TermF && ('F a * ('F b + 'F c))) ~> (('F a * 'F b) + ('F a * 'F c))) -> TermF ~> (('F a * ('F b + 'F c)) ~~> (('F a * 'F b) + ('F a * 'F 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 a * ('F b + 'F c))) ~> 'F a a :& (TermF * ('F a * ('F b + 'F c))) ~> ('F b + 'F c) bc) -> ((TermF * ('F a * ('F b + 'F c))) ~> ('F b ~~> ('F a --> (('F a * 'F b) + ('F a * 'F c))))) -> ((TermF * ('F a * ('F b + 'F c))) ~> ('F c ~~> ('F a --> (('F a * 'F b) + ('F a * 'F c))))) -> (TermF * ('F a * ('F b + 'F c))) ~> (('F b || 'F c) ~~> ('F a --> (('F a * 'F b) + ('F a * 'F 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 a * ('F b + 'F c))) && 'F b) => x ~> 'F b) -> ((TermF * ('F a * ('F b + 'F c))) && 'F b) ~> ('F a --> (('F a * 'F b) + ('F a * 'F c)))) -> (TermF * ('F a * ('F b + 'F c))) ~> ('F b ~~> ('F a --> (('F a * 'F b) + ('F a * 'F 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 a * ('F b + 'F c))) && 'F b) => x ~> 'F b b -> ((forall (x :: FK k). Cast x (((TermF * ('F a * ('F b + 'F c))) * 'F b) && 'F a) => x ~> 'F a) -> (((TermF * ('F a * ('F b + 'F c))) * 'F b) && 'F a) ~> (('F a * 'F b) + ('F a * 'F c))) -> ((TermF * ('F a * ('F b + 'F c))) * 'F b) ~> ('F a ~~> (('F a * 'F b) + ('F a * 'F 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 a * ('F b + 'F c))) * 'F b) && 'F a) => x ~> 'F a a' -> ((((TermF * ('F a * ('F b + 'F c))) * 'F b) * 'F a) ~> ('F a * 'F b)) -> (((TermF * ('F a * ('F b + 'F c))) * 'F b) * 'F a) ~> (('F a * 'F b) || ('F a * 'F c)) forall {k} (a :: k) (b :: k) (i :: k). (HasBinaryCoproducts k, Ob a, Ob b) => (i ~> a) -> i ~> (a || b) left ((((TermF * ('F a * ('F b + 'F c))) * 'F b) * 'F a) ~> 'F a forall (x :: FK k). Cast x (((TermF * ('F a * ('F b + 'F c))) * 'F b) && 'F a) => x ~> 'F a a' ((((TermF * ('F a * ('F b + 'F c))) * 'F b) * 'F a) ~> 'F a) -> ((((TermF * ('F a * ('F b + 'F c))) * 'F b) * 'F a) ~> 'F b) -> (((TermF * ('F a * ('F b + 'F c))) * 'F b) * 'F a) ~> ('F a && 'F b) forall {k} (i :: k) (a :: k) (b :: k). (CCC k, Ob a, Ob b) => (i ~> a) -> (i ~> b) -> i ~> (a && b) :& (((TermF * ('F a * ('F b + 'F c))) * 'F b) * 'F a) ~> 'F b forall (x :: FK k). Cast x ((TermF * ('F a * ('F b + 'F c))) && 'F b) => x ~> 'F b b)) (((forall (x :: FK k). Cast x ((TermF * ('F a * ('F b + 'F c))) && 'F c) => x ~> 'F c) -> ((TermF * ('F a * ('F b + 'F c))) && 'F c) ~> ('F a --> (('F a * 'F b) + ('F a * 'F c)))) -> (TermF * ('F a * ('F b + 'F c))) ~> ('F c ~~> ('F a --> (('F a * 'F b) + ('F a * 'F 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 a * ('F b + 'F c))) && 'F c) => x ~> 'F c c -> ((forall (x :: FK k). Cast x (((TermF * ('F a * ('F b + 'F c))) * 'F c) && 'F a) => x ~> 'F a) -> (((TermF * ('F a * ('F b + 'F c))) * 'F c) && 'F a) ~> (('F a * 'F b) + ('F a * 'F c))) -> ((TermF * ('F a * ('F b + 'F c))) * 'F c) ~> ('F a ~~> (('F a * 'F b) + ('F a * 'F 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 a * ('F b + 'F c))) * 'F c) && 'F a) => x ~> 'F a a' -> ((((TermF * ('F a * ('F b + 'F c))) * 'F c) * 'F a) ~> ('F a * 'F c)) -> (((TermF * ('F a * ('F b + 'F c))) * 'F c) * 'F a) ~> (('F a * 'F b) || ('F a * 'F c)) forall {k} (a :: k) (b :: k) (i :: k). (HasBinaryCoproducts k, Ob a, Ob b) => (i ~> b) -> i ~> (a || b) right ((((TermF * ('F a * ('F b + 'F c))) * 'F c) * 'F a) ~> 'F a forall (x :: FK k). Cast x (((TermF * ('F a * ('F b + 'F c))) * 'F c) && 'F a) => x ~> 'F a a' ((((TermF * ('F a * ('F b + 'F c))) * 'F c) * 'F a) ~> 'F a) -> ((((TermF * ('F a * ('F b + 'F c))) * 'F c) * 'F a) ~> 'F c) -> (((TermF * ('F a * ('F b + 'F c))) * 'F c) * 'F a) ~> ('F a && 'F c) forall {k} (i :: k) (a :: k) (b :: k). (CCC k, Ob a, Ob b) => (i ~> a) -> (i ~> b) -> i ~> (a && b) :& (((TermF * ('F a * ('F b + 'F c))) * 'F c) * 'F a) ~> 'F c forall (x :: FK k). Cast x ((TermF * ('F a * ('F b + 'F c))) && 'F c) => x ~> 'F c c)) ((TermF * ('F a * ('F b + 'F c))) ~> (('F b + 'F c) ~~> ('F a --> (('F a * 'F b) + ('F a * 'F c))))) -> ((TermF * ('F a * ('F b + 'F c))) ~> ('F b + 'F c)) -> (TermF * ('F a * ('F b + 'F c))) ~> ('F a --> (('F a * 'F b) + ('F a * 'F c))) forall {k} (i :: k) (a :: k) (b :: k). (CCC k, Ob b) => (i ~> (a ~~> b)) -> (i ~> a) -> i ~> b $ (TermF * ('F a * ('F b + 'F c))) ~> ('F b + 'F c) bc ((TermF * ('F a * ('F b + 'F c))) ~> ('F a ~~> (('F a * 'F b) + ('F a * 'F c)))) -> ((TermF * ('F a * ('F b + 'F c))) ~> 'F a) -> (TermF * ('F a * ('F b + 'F c))) ~> (('F a * 'F b) + ('F a * 'F c)) forall {k} (i :: k) (a :: k) (b :: k). (CCC k, Ob b) => (i ~> (a ~~> b)) -> (i ~> a) -> i ~> b $ (TermF * ('F a * ('F b + 'F c))) ~> 'F a a) distRProd :: forall {k} (a :: k) (b :: k) (c :: k). (BiCCC k, Ob a, Ob b, Ob c) => ((a || b) && c) ~> (a && c || b && c) distRProd :: forall {k} (a :: k) (b :: k) (c :: k). (BiCCC k, Ob a, Ob b, Ob c) => ((a || b) && c) ~> ((a && c) || (b && c)) distRProd = 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 a + 'F b) * 'F c)) => x ~> (('F a + 'F b) * 'F c)) -> (TermF && (('F a + 'F b) * 'F c)) ~> (('F a * 'F c) + ('F b * 'F c))) -> TermF ~> ((('F a + 'F b) * 'F c) ~~> (('F a * 'F c) + ('F b * 'F 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 a + 'F b) * 'F c)) ~> ('F a + 'F b) ab :& (TermF * (('F a + 'F b) * 'F c)) ~> 'F c c) -> ((TermF * (('F a + 'F b) * 'F c)) ~> ('F a ~~> ('F c --> (('F a * 'F c) + ('F b * 'F c))))) -> ((TermF * (('F a + 'F b) * 'F c)) ~> ('F b ~~> ('F c --> (('F a * 'F c) + ('F b * 'F c))))) -> (TermF * (('F a + 'F b) * 'F c)) ~> (('F a || 'F b) ~~> ('F c --> (('F a * 'F c) + ('F b * 'F 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 a + 'F b) * 'F c)) && 'F a) => x ~> 'F a) -> ((TermF * (('F a + 'F b) * 'F c)) && 'F a) ~> ('F c --> (('F a * 'F c) + ('F b * 'F c)))) -> (TermF * (('F a + 'F b) * 'F c)) ~> ('F a ~~> ('F c --> (('F a * 'F c) + ('F b * 'F 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 a + 'F b) * 'F c)) && 'F a) => x ~> 'F a a -> ((forall (x :: FK k). Cast x (((TermF * (('F a + 'F b) * 'F c)) * 'F a) && 'F c) => x ~> 'F c) -> (((TermF * (('F a + 'F b) * 'F c)) * 'F a) && 'F c) ~> (('F a * 'F c) + ('F b * 'F c))) -> ((TermF * (('F a + 'F b) * 'F c)) * 'F a) ~> ('F c ~~> (('F a * 'F c) + ('F b * 'F 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 a + 'F b) * 'F c)) * 'F a) && 'F c) => x ~> 'F c c' -> ((((TermF * (('F a + 'F b) * 'F c)) * 'F a) * 'F c) ~> ('F a * 'F c)) -> (((TermF * (('F a + 'F b) * 'F c)) * 'F a) * 'F c) ~> (('F a * 'F c) || ('F b * 'F c)) forall {k} (a :: k) (b :: k) (i :: k). (HasBinaryCoproducts k, Ob a, Ob b) => (i ~> a) -> i ~> (a || b) left ((((TermF * (('F a + 'F b) * 'F c)) * 'F a) * 'F c) ~> 'F a forall (x :: FK k). Cast x ((TermF * (('F a + 'F b) * 'F c)) && 'F a) => x ~> 'F a a ((((TermF * (('F a + 'F b) * 'F c)) * 'F a) * 'F c) ~> 'F a) -> ((((TermF * (('F a + 'F b) * 'F c)) * 'F a) * 'F c) ~> 'F c) -> (((TermF * (('F a + 'F b) * 'F c)) * 'F a) * 'F c) ~> ('F a && 'F c) forall {k} (i :: k) (a :: k) (b :: k). (CCC k, Ob a, Ob b) => (i ~> a) -> (i ~> b) -> i ~> (a && b) :& (((TermF * (('F a + 'F b) * 'F c)) * 'F a) * 'F c) ~> 'F c forall (x :: FK k). Cast x (((TermF * (('F a + 'F b) * 'F c)) * 'F a) && 'F c) => x ~> 'F c c')) (((forall (x :: FK k). Cast x ((TermF * (('F a + 'F b) * 'F c)) && 'F b) => x ~> 'F b) -> ((TermF * (('F a + 'F b) * 'F c)) && 'F b) ~> ('F c --> (('F a * 'F c) + ('F b * 'F c)))) -> (TermF * (('F a + 'F b) * 'F c)) ~> ('F b ~~> ('F c --> (('F a * 'F c) + ('F b * 'F 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 a + 'F b) * 'F c)) && 'F b) => x ~> 'F b b -> ((forall (x :: FK k). Cast x (((TermF * (('F a + 'F b) * 'F c)) * 'F b) && 'F c) => x ~> 'F c) -> (((TermF * (('F a + 'F b) * 'F c)) * 'F b) && 'F c) ~> (('F a * 'F c) + ('F b * 'F c))) -> ((TermF * (('F a + 'F b) * 'F c)) * 'F b) ~> ('F c ~~> (('F a * 'F c) + ('F b * 'F 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 a + 'F b) * 'F c)) * 'F b) && 'F c) => x ~> 'F c c' -> ((((TermF * (('F a + 'F b) * 'F c)) * 'F b) * 'F c) ~> ('F b * 'F c)) -> (((TermF * (('F a + 'F b) * 'F c)) * 'F b) * 'F c) ~> (('F a * 'F c) || ('F b * 'F c)) forall {k} (a :: k) (b :: k) (i :: k). (HasBinaryCoproducts k, Ob a, Ob b) => (i ~> b) -> i ~> (a || b) right ((((TermF * (('F a + 'F b) * 'F c)) * 'F b) * 'F c) ~> 'F b forall (x :: FK k). Cast x ((TermF * (('F a + 'F b) * 'F c)) && 'F b) => x ~> 'F b b ((((TermF * (('F a + 'F b) * 'F c)) * 'F b) * 'F c) ~> 'F b) -> ((((TermF * (('F a + 'F b) * 'F c)) * 'F b) * 'F c) ~> 'F c) -> (((TermF * (('F a + 'F b) * 'F c)) * 'F b) * 'F c) ~> ('F b && 'F c) forall {k} (i :: k) (a :: k) (b :: k). (CCC k, Ob a, Ob b) => (i ~> a) -> (i ~> b) -> i ~> (a && b) :& (((TermF * (('F a + 'F b) * 'F c)) * 'F b) * 'F c) ~> 'F c forall (x :: FK k). Cast x (((TermF * (('F a + 'F b) * 'F c)) * 'F b) && 'F c) => x ~> 'F c c')) ((TermF * (('F a + 'F b) * 'F c)) ~> (('F a + 'F b) ~~> ('F c --> (('F a * 'F c) + ('F b * 'F c))))) -> ((TermF * (('F a + 'F b) * 'F c)) ~> ('F a + 'F b)) -> (TermF * (('F a + 'F b) * 'F c)) ~> ('F c --> (('F a * 'F c) + ('F b * 'F c))) forall {k} (i :: k) (a :: k) (b :: k). (CCC k, Ob b) => (i ~> (a ~~> b)) -> (i ~> a) -> i ~> b $ (TermF * (('F a + 'F b) * 'F c)) ~> ('F a + 'F b) ab ((TermF * (('F a + 'F b) * 'F c)) ~> ('F c ~~> (('F a * 'F c) + ('F b * 'F c)))) -> ((TermF * (('F a + 'F b) * 'F c)) ~> 'F c) -> (TermF * (('F a + 'F b) * 'F c)) ~> (('F a * 'F c) + ('F b * 'F c)) forall {k} (i :: k) (a :: k) (b :: k). (CCC k, Ob b) => (i ~> (a ~~> b)) -> (i ~> a) -> i ~> b $ (TermF * (('F a + 'F b) * 'F c)) ~> 'F c c) type Traversable :: forall {k}. (k +-> k) -> Constraint class (Profunctor t) => Traversable (t :: k +-> k) where traverse :: (DistributiveProfunctor (p :: k +-> k), Strong k p, SelfAction k) => t :.: p :~> p :.: t instance (CategoryOf k) => Traversable (Id :: k +-> k) where traverse :: forall (p :: k +-> k). (DistributiveProfunctor p, Strong k p, SelfAction k) => (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 :: Type -> Type -> Type). (DistributiveProfunctor p, Strong Type p, SelfAction Type) => ((->) :.: 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 :: k +-> k). (DistributiveProfunctor p, Strong k p, SelfAction k) => ((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 {k} (t :: k +-> k) (p :: k +-> k). (Traversable t, DistributiveProfunctor p, Strong k p, SelfAction k) => (t :.: p) :~> (p :.: t) forall (p :: k +-> k). (DistributiveProfunctor p, Strong k p, SelfAction k) => (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 {k} (t :: k +-> k) (p :: k +-> k). (Traversable t, DistributiveProfunctor p, Strong k p, SelfAction k) => (t :.: p) :~> (p :.: t) forall (p :: k +-> k). (DistributiveProfunctor p, Strong k p, SelfAction k) => (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, Strong k p, SelfAction k) => ((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 {k} (t :: k +-> k) (p :: k +-> k). (Traversable t, DistributiveProfunctor p, Strong k p, SelfAction k) => (t :.: p) :~> (p :.: t) forall (p :: k +-> k). (DistributiveProfunctor p, Strong k p, SelfAction k) => (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 {k} (t :: k +-> k) (p :: k +-> k). (Traversable t, DistributiveProfunctor p, Strong k p, SelfAction k) => (t :.: p) :~> (p :.: t) forall (p :: k +-> k). (DistributiveProfunctor p, Strong k p, SelfAction k) => (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 :: k +-> k). (DistributiveProfunctor p, Strong k p, SelfAction k) => ((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 {k} (t :: k +-> k) (p :: k +-> k). (Traversable t, DistributiveProfunctor p, Strong k p, SelfAction k) => (t :.: p) :~> (p :.: t) forall (p :: k +-> k). (DistributiveProfunctor p, Strong k p, SelfAction k) => (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 {k} (t :: k +-> k) (p :: k +-> k). (Traversable t, DistributiveProfunctor p, Strong k p, SelfAction k) => (t :.: p) :~> (p :.: t) forall (p :: k +-> k). (DistributiveProfunctor p, Strong k p, SelfAction k) => (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' type Cotraversable :: forall {k}. (k +-> k) -> Constraint class (Profunctor t) => Cotraversable (t :: k +-> k) where cotraverse :: (DistributiveProfunctor (p :: k +-> k), Strong k p, SelfAction k) => p :.: t :~> t :.: p instance (CategoryOf k) => Cotraversable (Id :: k +-> k) where cotraverse :: forall (p :: k +-> k). (DistributiveProfunctor p, Strong k p, SelfAction k) => (p :.: Id) :~> (Id :.: p) cotraverse (p a b p :.: Id b ~> b f) = (a ~> a) -> Id a a forall k (a :: k) (b :: k). (a ~> b) -> Id a b Id a ~> a forall (a :: k). Ob a => a ~> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id Id a a -> p a b -> (:.:) Id 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) -> p a b -> p a b forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j). Profunctor p => (b ~> d) -> p a b -> p a d rmap b ~> b f p a b p ((Ob a, Ob b) => (:.:) Id p a b) -> p a b -> (:.:) Id p 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 Cotraversable (->) where cotraverse :: forall (p :: Type -> Type -> Type). (DistributiveProfunctor p, Strong Type p, SelfAction Type) => (p :.: (->)) :~> ((->) :.: p) cotraverse (p a b p :.: b -> b f) = a -> a forall a. Ob a => a -> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id (a -> a) -> p a 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) -> p a b -> p a b forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j). Profunctor p => (b ~> d) -> p a b -> p a d rmap b ~> b b -> b f p a b p instance (Cotraversable p, Cotraversable q) => Cotraversable (p :.: q) where cotraverse :: forall (p :: k +-> k). (DistributiveProfunctor p, Strong k p, SelfAction k) => (p :.: (p :.: q)) :~> ((p :.: q) :.: p) cotraverse (p a b r :.: (p b b p :.: q b b q)) = case (:.:) p p a b -> (:.:) p p a b (p :.: p) :~> (p :.: p) forall {k} (t :: k +-> k) (p :: k +-> k). (Cotraversable t, DistributiveProfunctor p, Strong k p, SelfAction k) => (p :.: t) :~> (t :.: p) forall (p :: k +-> k). (DistributiveProfunctor p, Strong k p, SelfAction k) => (p :.: p) :~> (p :.: p) cotraverse (p a b r 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 p) of p a b p' :.: p b b r' -> case (:.:) p q b b -> (:.:) q p b b (p :.: q) :~> (q :.: p) forall {k} (t :: k +-> k) (p :: k +-> k). (Cotraversable t, DistributiveProfunctor p, Strong k p, SelfAction k) => (p :.: t) :~> (t :.: p) forall (p :: k +-> k). (DistributiveProfunctor p, Strong k p, SelfAction k) => (p :.: q) :~> (q :.: p) cotraverse (p b b r' 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) of q b b q' :.: p b b r'' -> (p a b p' p a b -> q b b -> (:.:) 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 q') (:.:) p q a b -> p b b -> (:.:) (p :.: 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'' instance (HasBinaryCoproducts k, Cotraversable p, Cotraversable q) => Cotraversable ((p :: k +-> k) :*: q) where cotraverse :: forall (p :: k +-> k). (DistributiveProfunctor p, Strong k p, SelfAction k) => (p :.: (p :*: q)) :~> ((p :*: q) :.: p) cotraverse (p a b r :.: (p b b p :*: q b b q)) = case ((:.:) p p a b -> (:.:) p p a b (p :.: p) :~> (p :.: p) forall {k} (t :: k +-> k) (p :: k +-> k). (Cotraversable t, DistributiveProfunctor p, Strong k p, SelfAction k) => (p :.: t) :~> (t :.: p) forall (p :: k +-> k). (DistributiveProfunctor p, Strong k p, SelfAction k) => (p :.: p) :~> (p :.: p) cotraverse (p a b r 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 p), (:.:) p q a b -> (:.:) q p a b (p :.: q) :~> (q :.: p) forall {k} (t :: k +-> k) (p :: k +-> k). (Cotraversable t, DistributiveProfunctor p, Strong k p, SelfAction k) => (p :.: t) :~> (t :.: p) forall (p :: k +-> k). (DistributiveProfunctor p, Strong k p, SelfAction k) => (p :.: q) :~> (q :.: p) cotraverse (p a b r p a b -> q b b -> (:.:) 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 q)) of (p a b p' :.: p b b r', q a b q' :.: p b b r'') -> ((b ~> (b || b)) -> p a b -> p a (b || b) forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j). Profunctor p => (b ~> d) -> p a b -> p a d rmap ((b ~> b) -> Obj b -> b ~> (b || b) forall {k} (a :: k) (a' :: k) (b :: k). HasBinaryCoproducts k => (a ~> a') -> Obj b -> a ~> (a' || b) lft' (p a b -> b ~> b forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt p a b p') (q a b -> Obj b forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt q a b q')) p a b p' p a (b || b) -> q a (b || b) -> (:*:) p q a (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 a b -> q a (b || b) forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j). Profunctor p => (b ~> d) -> p a b -> p a d rmap ((b ~> b) -> Obj b -> b ~> (b || b) forall {k} (a :: k) (b :: k) (b' :: k). HasBinaryCoproducts k => Obj a -> (b ~> b') -> b ~> (a || b') rgt' (p a b -> b ~> b forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt p a b p') (q a b -> Obj b forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt q a b q')) q a b q') (:*:) p q a (b || b) -> p (b || b) b -> (:.:) (p :*: 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 :.: ((b || b) ~> b) -> p (b || b) (b || b) -> p (b || b) b forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j). Profunctor p => (b ~> d) -> p a b -> p a d rmap (b || b) ~> b forall {k} (a :: k). (HasBinaryCoproducts k, Ob a) => (a || a) ~> a codiag (p b b r' p b b -> p 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 r'') ((Ob b, Ob b) => (:.:) (p :*: q) p a b) -> p b b -> (:.:) (p :*: q) p 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 (Cotraversable p, Cotraversable q) => Cotraversable (p :+: q) where cotraverse :: forall (p :: k +-> k). (DistributiveProfunctor p, Strong k p, SelfAction k) => (p :.: (p :+: q)) :~> ((p :+: q) :.: p) cotraverse (p a b r :.: InjL p b b p) = case (:.:) p p a b -> (:.:) p p a b (p :.: p) :~> (p :.: p) forall {k} (t :: k +-> k) (p :: k +-> k). (Cotraversable t, DistributiveProfunctor p, Strong k p, SelfAction k) => (p :.: t) :~> (t :.: p) forall (p :: k +-> k). (DistributiveProfunctor p, Strong k p, SelfAction k) => (p :.: p) :~> (p :.: p) cotraverse (p a b r 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 p) of p a b p' :.: p b b r' -> p a b -> (:+:) p q a 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 a b p' (:+:) p q a b -> p b b -> (:.:) (p :+: 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' cotraverse (p a b r :.: InjR q b b q) = case (:.:) p q a b -> (:.:) q p a b (p :.: q) :~> (q :.: p) forall {k} (t :: k +-> k) (p :: k +-> k). (Cotraversable t, DistributiveProfunctor p, Strong k p, SelfAction k) => (p :.: t) :~> (t :.: p) forall (p :: k +-> k). (DistributiveProfunctor p, Strong k p, SelfAction k) => (p :.: q) :~> (q :.: p) cotraverse (p a b r p a b -> q b b -> (:.:) 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 q) of q a b q' :.: p b b r' -> q a b -> (:+:) p q a 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 a b q' (:+:) p q a b -> p b b -> (:.:) (p :+: 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'