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