{-# LANGUAGE AllowAmbiguousTypes #-} module Proarrow.Object.BinaryCoproduct where import Data.Kind (Type) import qualified Prelude as P import Proarrow.Core (CAT, PRO, CategoryOf(..), Promonad (..), Profunctor(..), UN, Is, dimapDefault) import Proarrow.Object (Obj, obj) import Proarrow.Object.Initial (HasInitialObject(..)) import Proarrow.Profunctor.Coproduct ((:+:)(..), coproduct) import Proarrow.Category.Instance.Prof (Prof(..)) import Proarrow.Category.Instance.Unit qualified as U import Proarrow.Category.Monoidal (Monoidal(..), SymMonoidal (..), MonoidalProfunctor (..)) class CategoryOf k => HasBinaryCoproducts k where type (a :: k) || (b :: k) :: k lft' :: Obj (a :: k) -> Obj b -> a ~> (a || b) rgt' :: Obj (a :: k) -> Obj b -> b ~> (a || b) (|||) :: (x :: k) ~> a -> y ~> a -> (x || y) ~> a (+++) :: forall a b x y. (a :: k) ~> x -> b ~> y -> a || b ~> x || y a ~> x l +++ b ~> y r = (forall (a :: k) (b :: k). (HasBinaryCoproducts k, Ob a, Ob b) => a ~> (a || b) forall {k} (a :: k) (b :: k). (HasBinaryCoproducts k, Ob a, Ob b) => a ~> (a || b) lft @x @y (x ~> (x || y)) -> (a ~> x) -> a ~> (x || y) forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c . a ~> x l) (a ~> (x || y)) -> (b ~> (x || y)) -> (a || b) ~> (x || y) forall (x :: k) (a :: k) (y :: k). (x ~> a) -> (y ~> a) -> (x || y) ~> a forall k (x :: k) (a :: k) (y :: k). HasBinaryCoproducts k => (x ~> a) -> (y ~> a) -> (x || y) ~> a ||| (forall (a :: k) (b :: k). (HasBinaryCoproducts k, Ob a, Ob b) => b ~> (a || b) forall {k} (a :: k) (b :: k). (HasBinaryCoproducts k, Ob a, Ob b) => b ~> (a || b) rgt @x @y (y ~> (x || y)) -> (b ~> y) -> b ~> (x || y) forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c . b ~> y r) ((Ob a, Ob x) => (a || b) ~> (x || y)) -> (a ~> x) -> (a || b) ~> (x || y) forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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 \\ a ~> x l ((Ob b, Ob y) => (a || b) ~> (x || y)) -> (b ~> y) -> (a || b) ~> (x || y) forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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 \\ b ~> y r lft :: forall {k} (a :: k) (b :: k). (HasBinaryCoproducts k, Ob a, Ob b) => a ~> (a || b) lft :: forall {k} (a :: k) (b :: k). (HasBinaryCoproducts k, Ob a, Ob b) => a ~> (a || b) lft = Obj a -> Obj b -> a ~> (a || b) forall (a :: k) (b :: k). Obj a -> Obj b -> a ~> (a || b) forall k (a :: k) (b :: k). HasBinaryCoproducts k => Obj a -> Obj b -> a ~> (a || b) lft' (forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @a) (forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @b) rgt :: forall {k} (a :: k) (b :: k). (HasBinaryCoproducts k, Ob a, Ob b) => b ~> (a || b) rgt :: forall {k} (a :: k) (b :: k). (HasBinaryCoproducts k, Ob a, Ob b) => b ~> (a || b) rgt = Obj a -> Obj b -> b ~> (a || b) forall (a :: k) (b :: k). Obj a -> Obj b -> b ~> (a || b) forall k (a :: k) (b :: k). HasBinaryCoproducts k => Obj a -> Obj b -> b ~> (a || b) rgt' (forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @a) (forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @b) left :: forall {k} (c :: k) (a :: k) (b :: k). (HasBinaryCoproducts k, Ob c) => a ~> b -> (a || c) ~> (b || c) left :: forall {k} (c :: k) (a :: k) (b :: k). (HasBinaryCoproducts k, Ob c) => (a ~> b) -> (a || c) ~> (b || c) left a ~> b f = a ~> b f (a ~> b) -> (c ~> c) -> (a || c) ~> (b || c) forall (a :: k) (b :: k) (x :: k) (y :: k). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryCoproducts k => (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) +++ forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @c right :: forall {k} (c :: k) (a :: k) (b :: k). (HasBinaryCoproducts k, Ob c) => a ~> b -> (c || a) ~> (c || b) right :: forall {k} (c :: k) (a :: k) (b :: k). (HasBinaryCoproducts k, Ob c) => (a ~> b) -> (c || a) ~> (c || b) right a ~> b f = forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @c Obj c -> (a ~> b) -> (c || a) ~> (c || b) forall (a :: k) (b :: k) (x :: k) (y :: k). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryCoproducts k => (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) +++ a ~> b f type HasCoproducts k = (HasInitialObject k, HasBinaryCoproducts k) instance HasBinaryCoproducts Type where type a || b = P.Either a b lft' :: forall a b. Obj a -> Obj b -> a ~> (a || b) lft' Obj a _ Obj b _ = a ~> (a || b) a -> Either a b forall a b. a -> Either a b P.Left rgt' :: forall a b. Obj a -> Obj b -> b ~> (a || b) rgt' Obj a _ Obj b _ = b ~> (a || b) b -> Either a b forall a b. b -> Either a b P.Right ||| :: forall x a y. (x ~> a) -> (y ~> a) -> (x || y) ~> a (|||) = (x ~> a) -> (y ~> a) -> (x || y) ~> a (x -> a) -> (y -> a) -> Either x y -> a forall a c b. (a -> c) -> (b -> c) -> Either a b -> c P.either instance HasBinaryCoproducts U.UNIT where type U.U || U.U = U.U lft' :: forall (a :: UNIT) (b :: UNIT). Obj a -> Obj b -> a ~> (a || b) lft' Obj a Unit a a U.Unit Obj b Unit b b U.Unit = a ~> (a || b) Unit U U U.Unit rgt' :: forall (a :: UNIT) (b :: UNIT). Obj a -> Obj b -> b ~> (a || b) rgt' Obj a Unit a a U.Unit Obj b Unit b b U.Unit = b ~> (a || b) Unit U U U.Unit x ~> a Unit x a U.Unit ||| :: forall (x :: UNIT) (a :: UNIT) (y :: UNIT). (x ~> a) -> (y ~> a) -> (x || y) ~> a ||| y ~> a Unit y U U.Unit = (x || y) ~> a Unit U U U.Unit instance (CategoryOf j, CategoryOf k) => HasBinaryCoproducts (PRO j k) where type p || q = p :+: q lft' :: forall (a :: PRO j k) (b :: PRO j k). Obj a -> Obj b -> a ~> (a || b) lft' Prof{} Prof{} = (a :~> (a :+: b)) -> Prof a (a :+: b) forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof a a b -> (:+:) a b a b a :~> (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 rgt' :: forall (a :: PRO j k) (b :: PRO j k). Obj a -> Obj b -> b ~> (a || b) rgt' Prof{} Prof{} = (b :~> (a :+: b)) -> Prof b (a :+: b) forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof b a b -> (:+:) a b a b b :~> (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 Prof x :~> a l ||| :: forall (x :: PRO j k) (a :: PRO j k) (y :: PRO j k). (x ~> a) -> (y ~> a) -> (x || y) ~> a ||| Prof y :~> a r = ((x :+: y) :~> a) -> Prof (x :+: y) a forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof ((x :~> a) -> (y :~> a) -> (x :+: y) :~> a forall {k} {k1} (p :: k -> k1 -> Type) (r :: k -> k1 -> Type) (q :: k -> k1 -> Type). (p :~> r) -> (q :~> r) -> (p :+: q) :~> r coproduct x a b -> a a b x :~> a l y a b -> a a b y :~> a r) newtype COPROD k = COPR k type instance UN COPR (COPR k) = k type Coprod :: CAT (COPROD k) data Coprod a b where Coprod :: (Ob a, Ob b) => { forall {j} (a :: COPROD j) (b :: COPROD j). Coprod a b -> UN 'COPR a ~> UN 'COPR b getCoprod :: UN COPR a ~> UN COPR b } -> Coprod a b mkCoprod :: CategoryOf k => (a :: k) ~> b -> Coprod (COPR a) (COPR b) mkCoprod :: forall k (a :: k) (b :: k). CategoryOf k => (a ~> b) -> Coprod ('COPR a) ('COPR b) mkCoprod a ~> b f = (UN 'COPR ('COPR a) ~> UN 'COPR ('COPR b)) -> Coprod ('COPR a) ('COPR b) forall {j} (a :: COPROD j) (b :: COPROD j). (Ob a, Ob b) => (UN 'COPR a ~> UN 'COPR b) -> Coprod a b Coprod a ~> b UN 'COPR ('COPR a) ~> UN 'COPR ('COPR b) f ((Ob a, Ob b) => Coprod ('COPR a) ('COPR b)) -> (a ~> b) -> Coprod ('COPR a) ('COPR b) forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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 \\ a ~> b f instance CategoryOf k => Profunctor (Coprod :: CAT (COPROD k)) where dimap :: forall (c :: COPROD k) (a :: COPROD k) (b :: COPROD k) (d :: COPROD k). (c ~> a) -> (b ~> d) -> Coprod a b -> Coprod c d dimap = (c ~> a) -> (b ~> d) -> Coprod a b -> Coprod c d Coprod c a -> Coprod b d -> Coprod a b -> Coprod c d forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k). Promonad p => p c a -> p b d -> p a b -> p c d dimapDefault (Ob a, Ob b) => r r \\ :: forall (a :: COPROD k) (b :: COPROD k) r. ((Ob a, Ob b) => r) -> Coprod a b -> r \\ Coprod UN 'COPR a ~> UN 'COPR b f = r (Ob (UN 'COPR a), Ob (UN 'COPR b)) => r (Ob a, Ob b) => r r ((Ob (UN 'COPR a), Ob (UN 'COPR b)) => r) -> (UN 'COPR a ~> UN 'COPR b) -> r forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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 \\ UN 'COPR a ~> UN 'COPR b f instance CategoryOf k => Promonad (Coprod :: CAT (COPROD k)) where id :: forall (a :: COPROD k). Ob a => Coprod a a id = (UN 'COPR a ~> UN 'COPR a) -> Coprod a a forall {j} (a :: COPROD j) (b :: COPROD j). (Ob a, Ob b) => (UN 'COPR a ~> UN 'COPR b) -> Coprod a b Coprod UN 'COPR a ~> UN 'COPR a forall (a :: k). Ob a => a ~> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id Coprod UN 'COPR b ~> UN 'COPR c f . :: forall (b :: COPROD k) (c :: COPROD k) (a :: COPROD k). Coprod b c -> Coprod a b -> Coprod a c . Coprod UN 'COPR a ~> UN 'COPR b g = (UN 'COPR a ~> UN 'COPR c) -> Coprod a c forall {j} (a :: COPROD j) (b :: COPROD j). (Ob a, Ob b) => (UN 'COPR a ~> UN 'COPR b) -> Coprod a b Coprod (UN 'COPR b ~> UN 'COPR c f (UN 'COPR b ~> UN 'COPR c) -> (UN 'COPR a ~> UN 'COPR b) -> UN 'COPR a ~> UN 'COPR c forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c . UN 'COPR a ~> UN 'COPR b g) instance CategoryOf k => CategoryOf (COPROD k) where type (~>) = Coprod type Ob a = (Is COPR a, Ob (UN COPR a)) instance HasCoproducts k => Monoidal (COPROD k) where type Unit = COPR InitialObject type a ** b = COPR (UN COPR a || UN COPR b) Coprod UN 'COPR a ~> UN 'COPR b f par :: forall (a :: COPROD k) (b :: COPROD k) (c :: COPROD k) (d :: COPROD k). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` Coprod UN 'COPR c ~> UN 'COPR d g = ((UN 'COPR a || UN 'COPR c) ~> (UN 'COPR b || UN 'COPR d)) -> Coprod ('COPR (UN 'COPR a || UN 'COPR c)) ('COPR (UN 'COPR b || UN 'COPR d)) forall k (a :: k) (b :: k). CategoryOf k => (a ~> b) -> Coprod ('COPR a) ('COPR b) mkCoprod (UN 'COPR a ~> UN 'COPR b f (UN 'COPR a ~> UN 'COPR b) -> (UN 'COPR c ~> UN 'COPR d) -> (UN 'COPR a || UN 'COPR c) ~> (UN 'COPR b || UN 'COPR d) forall (a :: k) (b :: k) (x :: k) (y :: k). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryCoproducts k => (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) +++ UN 'COPR c ~> UN 'COPR d g) leftUnitor :: forall (a :: COPROD k). Obj a -> (Unit ** a) ~> a leftUnitor (Coprod UN 'COPR a ~> UN 'COPR a a) = ((InitialObject || UN 'COPR a) ~> UN 'COPR a) -> Coprod ('COPR (InitialObject || UN 'COPR a)) ('COPR (UN 'COPR a)) forall k (a :: k) (b :: k). CategoryOf k => (a ~> b) -> Coprod ('COPR a) ('COPR b) mkCoprod ((UN 'COPR a ~> UN 'COPR a) -> InitialObject ~> UN 'COPR a forall (a :: k). Obj a -> InitialObject ~> a forall k (a :: k). HasInitialObject k => Obj a -> InitialObject ~> a initiate' UN 'COPR a ~> UN 'COPR a a (InitialObject ~> UN 'COPR a) -> (UN 'COPR a ~> UN 'COPR a) -> (InitialObject || UN 'COPR a) ~> UN 'COPR a forall (x :: k) (a :: k) (y :: k). (x ~> a) -> (y ~> a) -> (x || y) ~> a forall k (x :: k) (a :: k) (y :: k). HasBinaryCoproducts k => (x ~> a) -> (y ~> a) -> (x || y) ~> a ||| UN 'COPR a ~> UN 'COPR a a) leftUnitorInv :: forall (a :: COPROD k). Obj a -> a ~> (Unit ** a) leftUnitorInv (Coprod UN 'COPR a ~> UN 'COPR a a) = (UN 'COPR a ~> (InitialObject || UN 'COPR a)) -> Coprod ('COPR (UN 'COPR a)) ('COPR (InitialObject || UN 'COPR a)) forall k (a :: k) (b :: k). CategoryOf k => (a ~> b) -> Coprod ('COPR a) ('COPR b) mkCoprod (Obj InitialObject -> (UN 'COPR a ~> UN 'COPR a) -> UN 'COPR a ~> (InitialObject || UN 'COPR a) forall (a :: k) (b :: k). Obj a -> Obj b -> b ~> (a || b) forall k (a :: k) (b :: k). HasBinaryCoproducts k => Obj a -> Obj b -> b ~> (a || b) rgt' (forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @InitialObject) UN 'COPR a ~> UN 'COPR a a) rightUnitor :: forall (a :: COPROD k). Obj a -> (a ** Unit) ~> a rightUnitor (Coprod UN 'COPR a ~> UN 'COPR a a) = ((UN 'COPR a || InitialObject) ~> UN 'COPR a) -> Coprod ('COPR (UN 'COPR a || InitialObject)) ('COPR (UN 'COPR a)) forall k (a :: k) (b :: k). CategoryOf k => (a ~> b) -> Coprod ('COPR a) ('COPR b) mkCoprod (UN 'COPR a ~> UN 'COPR a a (UN 'COPR a ~> UN 'COPR a) -> (InitialObject ~> UN 'COPR a) -> (UN 'COPR a || InitialObject) ~> UN 'COPR a forall (x :: k) (a :: k) (y :: k). (x ~> a) -> (y ~> a) -> (x || y) ~> a forall k (x :: k) (a :: k) (y :: k). HasBinaryCoproducts k => (x ~> a) -> (y ~> a) -> (x || y) ~> a ||| (UN 'COPR a ~> UN 'COPR a) -> InitialObject ~> UN 'COPR a forall (a :: k). Obj a -> InitialObject ~> a forall k (a :: k). HasInitialObject k => Obj a -> InitialObject ~> a initiate' UN 'COPR a ~> UN 'COPR a a) rightUnitorInv :: forall (a :: COPROD k). Obj a -> a ~> (a ** Unit) rightUnitorInv (Coprod UN 'COPR a ~> UN 'COPR a a) = (UN 'COPR a ~> (UN 'COPR a || InitialObject)) -> Coprod ('COPR (UN 'COPR a)) ('COPR (UN 'COPR a || InitialObject)) forall k (a :: k) (b :: k). CategoryOf k => (a ~> b) -> Coprod ('COPR a) ('COPR b) mkCoprod ((UN 'COPR a ~> UN 'COPR a) -> Obj InitialObject -> UN 'COPR a ~> (UN 'COPR a || InitialObject) forall (a :: k) (b :: k). Obj a -> Obj b -> a ~> (a || b) forall k (a :: k) (b :: k). HasBinaryCoproducts k => Obj a -> Obj b -> a ~> (a || b) lft' UN 'COPR a ~> UN 'COPR a a (forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @InitialObject)) associator :: forall (a :: COPROD k) (b :: COPROD k) (c :: COPROD k). Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c)) associator (Coprod UN 'COPR a ~> UN 'COPR a a) (Coprod UN 'COPR b ~> UN 'COPR b b) (Coprod UN 'COPR c ~> UN 'COPR c c) = (((UN 'COPR a || UN 'COPR b) || UN 'COPR c) ~> (UN 'COPR a || (UN 'COPR b || UN 'COPR c))) -> Coprod ('COPR ((UN 'COPR a || UN 'COPR b) || UN 'COPR c)) ('COPR (UN 'COPR a || (UN 'COPR b || UN 'COPR c))) forall k (a :: k) (b :: k). CategoryOf k => (a ~> b) -> Coprod ('COPR a) ('COPR b) mkCoprod ((UN 'COPR a ~> UN 'COPR a a (UN 'COPR a ~> UN 'COPR a) -> (UN 'COPR b ~> (UN 'COPR b || UN 'COPR c)) -> (UN 'COPR a || UN 'COPR b) ~> (UN 'COPR a || (UN 'COPR b || UN 'COPR c)) forall (a :: k) (b :: k) (x :: k) (y :: k). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryCoproducts k => (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) +++ (UN 'COPR b ~> UN 'COPR b) -> (UN 'COPR c ~> UN 'COPR c) -> UN 'COPR b ~> (UN 'COPR b || UN 'COPR c) forall (a :: k) (b :: k). Obj a -> Obj b -> a ~> (a || b) forall k (a :: k) (b :: k). HasBinaryCoproducts k => Obj a -> Obj b -> a ~> (a || b) lft' UN 'COPR b ~> UN 'COPR b b UN 'COPR c ~> UN 'COPR c c) ((UN 'COPR a || UN 'COPR b) ~> (UN 'COPR a || (UN 'COPR b || UN 'COPR c))) -> (UN 'COPR c ~> (UN 'COPR a || (UN 'COPR b || UN 'COPR c))) -> ((UN 'COPR a || UN 'COPR b) || UN 'COPR c) ~> (UN 'COPR a || (UN 'COPR b || UN 'COPR c)) forall (x :: k) (a :: k) (y :: k). (x ~> a) -> (y ~> a) -> (x || y) ~> a forall k (x :: k) (a :: k) (y :: k). HasBinaryCoproducts k => (x ~> a) -> (y ~> a) -> (x || y) ~> a ||| ((UN 'COPR a ~> UN 'COPR a) -> Obj (UN 'COPR b || UN 'COPR c) -> (UN 'COPR b || UN 'COPR c) ~> (UN 'COPR a || (UN 'COPR b || UN 'COPR c)) forall (a :: k) (b :: k). Obj a -> Obj b -> b ~> (a || b) forall k (a :: k) (b :: k). HasBinaryCoproducts k => Obj a -> Obj b -> b ~> (a || b) rgt' UN 'COPR a ~> UN 'COPR a a (UN 'COPR b ~> UN 'COPR b b (UN 'COPR b ~> UN 'COPR b) -> (UN 'COPR c ~> UN 'COPR c) -> Obj (UN 'COPR b || UN 'COPR c) forall (a :: k) (b :: k) (x :: k) (y :: k). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryCoproducts k => (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) +++ UN 'COPR c ~> UN 'COPR c c) ((UN 'COPR b || UN 'COPR c) ~> (UN 'COPR a || (UN 'COPR b || UN 'COPR c))) -> (UN 'COPR c ~> (UN 'COPR b || UN 'COPR c)) -> UN 'COPR c ~> (UN 'COPR a || (UN 'COPR b || UN 'COPR c)) forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c . (UN 'COPR b ~> UN 'COPR b) -> (UN 'COPR c ~> UN 'COPR c) -> UN 'COPR c ~> (UN 'COPR b || UN 'COPR c) forall (a :: k) (b :: k). Obj a -> Obj b -> b ~> (a || b) forall k (a :: k) (b :: k). HasBinaryCoproducts k => Obj a -> Obj b -> b ~> (a || b) rgt' UN 'COPR b ~> UN 'COPR b b UN 'COPR c ~> UN 'COPR c c) ((Ob (UN 'COPR a || UN 'COPR b), Ob (UN 'COPR a || UN 'COPR b)) => ((UN 'COPR a || UN 'COPR b) || UN 'COPR c) ~> (UN 'COPR a || (UN 'COPR b || UN 'COPR c))) -> ((UN 'COPR a || UN 'COPR b) ~> (UN 'COPR a || UN 'COPR b)) -> ((UN 'COPR a || UN 'COPR b) || UN 'COPR c) ~> (UN 'COPR a || (UN 'COPR b || UN 'COPR c)) forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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 \\ (UN 'COPR a ~> UN 'COPR a a (UN 'COPR a ~> UN 'COPR a) -> (UN 'COPR b ~> UN 'COPR b) -> (UN 'COPR a || UN 'COPR b) ~> (UN 'COPR a || UN 'COPR b) forall (a :: k) (b :: k) (x :: k) (y :: k). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryCoproducts k => (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) +++ UN 'COPR b ~> UN 'COPR b b)) associatorInv :: forall (a :: COPROD k) (b :: COPROD k) (c :: COPROD k). Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c) associatorInv (Coprod UN 'COPR a ~> UN 'COPR a a) (Coprod UN 'COPR b ~> UN 'COPR b b) (Coprod UN 'COPR c ~> UN 'COPR c c) = ((UN 'COPR a || (UN 'COPR b || UN 'COPR c)) ~> ((UN 'COPR a || UN 'COPR b) || UN 'COPR c)) -> Coprod ('COPR (UN 'COPR a || (UN 'COPR b || UN 'COPR c))) ('COPR ((UN 'COPR a || UN 'COPR b) || UN 'COPR c)) forall k (a :: k) (b :: k). CategoryOf k => (a ~> b) -> Coprod ('COPR a) ('COPR b) mkCoprod ((Obj (UN 'COPR a || UN 'COPR b) -> (UN 'COPR c ~> UN 'COPR c) -> (UN 'COPR a || UN 'COPR b) ~> ((UN 'COPR a || UN 'COPR b) || UN 'COPR c) forall (a :: k) (b :: k). Obj a -> Obj b -> a ~> (a || b) forall k (a :: k) (b :: k). HasBinaryCoproducts k => Obj a -> Obj b -> a ~> (a || b) lft' (UN 'COPR a ~> UN 'COPR a a (UN 'COPR a ~> UN 'COPR a) -> (UN 'COPR b ~> UN 'COPR b) -> Obj (UN 'COPR a || UN 'COPR b) forall (a :: k) (b :: k) (x :: k) (y :: k). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryCoproducts k => (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) +++ UN 'COPR b ~> UN 'COPR b b) UN 'COPR c ~> UN 'COPR c c ((UN 'COPR a || UN 'COPR b) ~> ((UN 'COPR a || UN 'COPR b) || UN 'COPR c)) -> (UN 'COPR a ~> (UN 'COPR a || UN 'COPR b)) -> UN 'COPR a ~> ((UN 'COPR a || UN 'COPR b) || UN 'COPR c) forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k). Promonad p => p b c -> p a b -> p a c . (UN 'COPR a ~> UN 'COPR a) -> (UN 'COPR b ~> UN 'COPR b) -> UN 'COPR a ~> (UN 'COPR a || UN 'COPR b) forall (a :: k) (b :: k). Obj a -> Obj b -> a ~> (a || b) forall k (a :: k) (b :: k). HasBinaryCoproducts k => Obj a -> Obj b -> a ~> (a || b) lft' UN 'COPR a ~> UN 'COPR a a UN 'COPR b ~> UN 'COPR b b) (UN 'COPR a ~> ((UN 'COPR a || UN 'COPR b) || UN 'COPR c)) -> ((UN 'COPR b || UN 'COPR c) ~> ((UN 'COPR a || UN 'COPR b) || UN 'COPR c)) -> (UN 'COPR a || (UN 'COPR b || UN 'COPR c)) ~> ((UN 'COPR a || UN 'COPR b) || UN 'COPR c) forall (x :: k) (a :: k) (y :: k). (x ~> a) -> (y ~> a) -> (x || y) ~> a forall k (x :: k) (a :: k) (y :: k). HasBinaryCoproducts k => (x ~> a) -> (y ~> a) -> (x || y) ~> a ||| ((UN 'COPR a ~> UN 'COPR a) -> (UN 'COPR b ~> UN 'COPR b) -> UN 'COPR b ~> (UN 'COPR a || UN 'COPR b) forall (a :: k) (b :: k). Obj a -> Obj b -> b ~> (a || b) forall k (a :: k) (b :: k). HasBinaryCoproducts k => Obj a -> Obj b -> b ~> (a || b) rgt' UN 'COPR a ~> UN 'COPR a a UN 'COPR b ~> UN 'COPR b b (UN 'COPR b ~> (UN 'COPR a || UN 'COPR b)) -> (UN 'COPR c ~> UN 'COPR c) -> (UN 'COPR b || UN 'COPR c) ~> ((UN 'COPR a || UN 'COPR b) || UN 'COPR c) forall (a :: k) (b :: k) (x :: k) (y :: k). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryCoproducts k => (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) +++ UN 'COPR c ~> UN 'COPR c c) ((Ob (UN 'COPR a || UN 'COPR b), Ob (UN 'COPR a || UN 'COPR b)) => (UN 'COPR a || (UN 'COPR b || UN 'COPR c)) ~> ((UN 'COPR a || UN 'COPR b) || UN 'COPR c)) -> Obj (UN 'COPR a || UN 'COPR b) -> (UN 'COPR a || (UN 'COPR b || UN 'COPR c)) ~> ((UN 'COPR a || UN 'COPR b) || UN 'COPR c) forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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 \\ (UN 'COPR a ~> UN 'COPR a a (UN 'COPR a ~> UN 'COPR a) -> (UN 'COPR b ~> UN 'COPR b) -> Obj (UN 'COPR a || UN 'COPR b) forall (a :: k) (b :: k) (x :: k) (y :: k). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) forall k (a :: k) (b :: k) (x :: k) (y :: k). HasBinaryCoproducts k => (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) +++ UN 'COPR b ~> UN 'COPR b b)) instance HasCoproducts k => SymMonoidal (COPROD k) where swap' :: forall (a :: COPROD k) (b :: COPROD k). Obj a -> Obj b -> (a ** b) ~> (b ** a) swap' (Coprod UN 'COPR a ~> UN 'COPR a a) (Coprod UN 'COPR b ~> UN 'COPR b b) = ((UN 'COPR a || UN 'COPR b) ~> (UN 'COPR b || UN 'COPR a)) -> Coprod ('COPR (UN 'COPR a || UN 'COPR b)) ('COPR (UN 'COPR b || UN 'COPR a)) forall k (a :: k) (b :: k). CategoryOf k => (a ~> b) -> Coprod ('COPR a) ('COPR b) mkCoprod ((UN 'COPR b ~> UN 'COPR b) -> (UN 'COPR a ~> UN 'COPR a) -> UN 'COPR a ~> (UN 'COPR b || UN 'COPR a) forall (a :: k) (b :: k). Obj a -> Obj b -> b ~> (a || b) forall k (a :: k) (b :: k). HasBinaryCoproducts k => Obj a -> Obj b -> b ~> (a || b) rgt' UN 'COPR b ~> UN 'COPR b b UN 'COPR a ~> UN 'COPR a a (UN 'COPR a ~> (UN 'COPR b || UN 'COPR a)) -> (UN 'COPR b ~> (UN 'COPR b || UN 'COPR a)) -> (UN 'COPR a || UN 'COPR b) ~> (UN 'COPR b || UN 'COPR a) forall (x :: k) (a :: k) (y :: k). (x ~> a) -> (y ~> a) -> (x || y) ~> a forall k (x :: k) (a :: k) (y :: k). HasBinaryCoproducts k => (x ~> a) -> (y ~> a) -> (x || y) ~> a ||| (UN 'COPR b ~> UN 'COPR b) -> (UN 'COPR a ~> UN 'COPR a) -> UN 'COPR b ~> (UN 'COPR b || UN 'COPR a) forall (a :: k) (b :: k). Obj a -> Obj b -> a ~> (a || b) forall k (a :: k) (b :: k). HasBinaryCoproducts k => Obj a -> Obj b -> a ~> (a || b) lft' UN 'COPR b ~> UN 'COPR b b UN 'COPR a ~> UN 'COPR a a) instance HasCoproducts k => MonoidalProfunctor (Coprod :: CAT (COPROD k)) where lift0 :: Coprod Unit Unit lift0 = Coprod Unit Unit Coprod ('COPR InitialObject) ('COPR InitialObject) forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a forall (a :: COPROD k). Ob a => Coprod a a id lift2 :: forall (x1 :: COPROD k) (x2 :: COPROD k) (y1 :: COPROD k) (y2 :: COPROD k). Coprod x1 x2 -> Coprod y1 y2 -> Coprod (x1 ** y1) (x2 ** y2) lift2 = (x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2) Coprod x1 x2 -> Coprod y1 y2 -> Coprod (x1 ** y1) (x2 ** y2) forall k (a :: k) (b :: k) (c :: k) (d :: k). Monoidal k => (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) forall (a :: COPROD k) (b :: COPROD k) (c :: COPROD k) (d :: COPROD k). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) par