{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Object.BinaryCoproduct where

import Data.Kind (Type)
import Prelude (type (~))
import Prelude qualified as P

import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), Strong (..))
import Proarrow.Core (CAT, Category, CategoryOf (..), Is, PRO, Profunctor (..), Promonad (..), UN, type (+->))
import Proarrow.Object (Obj, obj, tgt)
import Proarrow.Object.BinaryProduct (PROD (..), Prod (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Profunctor.Coproduct (coproduct, (:+:) (..))

infixl 4 ||
infixl 4 |||
infixl 4 +++

class (CategoryOf k) => HasBinaryCoproducts k where
  type (a :: k) || (b :: k) :: k
  lft :: (Ob (a :: k), Ob b) => a ~> (a || b)
  lft @a @b = (a ~> a) -> Obj b -> a ~> (a || b)
forall (a :: k) (a' :: k) (b :: k).
(a ~> a') -> Obj b -> a ~> (a' || b)
forall k (a :: k) (a' :: k) (b :: k).
HasBinaryCoproducts k =>
(a ~> 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)
  lft' :: (a :: k) ~> a' -> Obj b -> a ~> (a' || b)
  lft' @_ @a' @b a ~> a'
a Obj b
b = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a' @b (a' ~> (a' || b)) -> (a ~> a') -> a ~> (a' || b)
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 ~> a'
a ((Ob a, Ob a') => a ~> (a' || b)) -> (a ~> a') -> a ~> (a' || 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 ~> a'
a ((Ob b, Ob b) => a ~> (a' || b)) -> Obj b -> a ~> (a' || 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
\\ Obj b
b
  rgt :: (Ob (a :: k), Ob b) => b ~> (a || b)
  rgt @a @b = Obj a -> (b ~> b) -> b ~> (a || b)
forall (a :: k) (b :: k) (b' :: k).
Obj a -> (b ~> b') -> b ~> (a || b')
forall k (a :: k) (b :: k) (b' :: k).
HasBinaryCoproducts k =>
Obj a -> (b ~> 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)
  rgt' :: Obj (a :: k) -> b ~> b' -> b ~> (a || b')
  rgt' @a @_ @b' Obj a
a b ~> b'
b = forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @b' (b' ~> (a || b')) -> (b ~> b') -> b ~> (a || b')
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 ~> b'
b ((Ob a, Ob a) => b ~> (a || b')) -> Obj a -> b ~> (a || 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
\\ Obj a
a ((Ob b, Ob b') => b ~> (a || b')) -> (b ~> b') -> b ~> (a || 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
\\ b ~> b'
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 k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @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 k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @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

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

codiag :: forall {k} (a :: k). (HasBinaryCoproducts k, Ob a) => (a || a) ~> a
codiag :: forall {k} (a :: k). (HasBinaryCoproducts k, Ob a) => (a || a) ~> a
codiag = 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 (a ~> a) -> (a ~> a) -> (a || a) ~> 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
||| 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

swapCoprod' :: (HasBinaryCoproducts k) => (a :: k) ~> a' -> b ~> b' -> (a || b) ~> (b' || a')
swapCoprod' :: forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
HasBinaryCoproducts k =>
(a ~> a') -> (b ~> b') -> (a || b) ~> (b' || a')
swapCoprod' a ~> a'
a b ~> b'
b = Obj b' -> (a ~> a') -> a ~> (b' || a')
forall (a :: k) (b :: k) (b' :: k).
Obj a -> (b ~> b') -> b ~> (a || b')
forall k (a :: k) (b :: k) (b' :: k).
HasBinaryCoproducts k =>
Obj a -> (b ~> b') -> b ~> (a || b')
rgt' ((b ~> b') -> Obj b'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt b ~> b'
b) a ~> a'
a (a ~> (b' || a')) -> (b ~> (b' || a')) -> (a || b) ~> (b' || 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
||| (b ~> b') -> Obj a' -> b ~> (b' || a')
forall (a :: k) (a' :: k) (b :: k).
(a ~> a') -> Obj b -> a ~> (a' || b)
forall k (a :: k) (a' :: k) (b :: k).
HasBinaryCoproducts k =>
(a ~> a') -> Obj b -> a ~> (a' || b)
lft' b ~> b'
b ((a ~> a') -> Obj a'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt a ~> a'
a)

swapCoprod :: (HasBinaryCoproducts k, Ob a, Ob b) => (a :: k) || b ~> b || a
swapCoprod :: forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(a || b) ~> (b || a)
swapCoprod @_ @a @b = (a ~> a) -> (b ~> b) -> (a || b) ~> (b || a)
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
HasBinaryCoproducts k =>
(a ~> a') -> (b ~> b') -> (a || b) ~> (b' || a')
swapCoprod' (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)

type HasCoproducts k = (HasInitialObject k, HasBinaryCoproducts k)

class ((a ** b) ~ (a || b)) => TensorIsCoproduct a b
instance ((a ** b) ~ (a || b)) => TensorIsCoproduct a b
class
  (HasCoproducts k, Monoidal k, (Unit :: k) ~ InitialObject, forall (a :: k) (b :: k). TensorIsCoproduct a b) =>
  Cocartesian k
instance
  (HasCoproducts k, Monoidal k, (Unit :: k) ~ InitialObject, forall (a :: k) (b :: k). TensorIsCoproduct a b)
  => Cocartesian k

instance HasBinaryCoproducts Type where
  type a || b = P.Either a b
  lft :: forall a b. (Ob a, Ob b) => a ~> (a || b)
lft = a ~> (a || b)
a -> Either a b
forall a b. a -> Either a b
P.Left
  rgt :: forall a b. (Ob a, Ob b) => b ~> (a || b)
rgt = 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 () where
  type '() || '() = '()
  lft :: forall (a :: ()) (b :: ()). (Ob a, Ob b) => a ~> (a || b)
lft = a ~> (a || b)
Unit '() '()
U.Unit
  rgt :: forall (a :: ()) (b :: ()). (Ob a, Ob b) => b ~> (a || b)
rgt = b ~> (a || b)
Unit '() '()
U.Unit
  x ~> a
Unit x a
U.Unit ||| :: forall (x :: ()) (a :: ()) (y :: ()).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| y ~> a
Unit y '()
U.Unit = (x || y) ~> a
Unit '() '()
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). (Ob a, Ob b) => a ~> (a || b)
lft = (a :~> (a :+: b)) -> Prof a (a :+: b)
forall {k} {j} (p :: j +-> k) (q :: 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). (Ob a, Ob b) => b ~> (a || b)
rgt = (b :~> (a :+: b)) -> Prof b (a :+: b)
forall {k} {j} (p :: j +-> k) (q :: 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 {k} {j} (p :: j +-> k) (q :: 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)

instance (HasBinaryCoproducts k) => HasBinaryCoproducts (PROD k) where
  type PR a || PR b = PR (a || b)
  lft :: forall (a :: PROD k) (b :: PROD k). (Ob a, Ob b) => a ~> (a || b)
lft @(PR a) @(PR b) = (UN 'PR a ~> (UN 'PR a || UN 'PR b))
-> Prod (~>) ('PR (UN 'PR a)) ('PR (UN 'PR a || UN 'PR b))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @a @b)
  rgt :: forall (a :: PROD k) (b :: PROD k). (Ob a, Ob b) => b ~> (a || b)
rgt @(PR a) @(PR b) = (UN 'PR b ~> (UN 'PR a || UN 'PR b))
-> Prod (~>) ('PR (UN 'PR b)) ('PR (UN 'PR a || UN 'PR b))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @a @b)
  Prod a1 ~> b1
l ||| :: forall (x :: PROD k) (a :: PROD k) (y :: PROD k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Prod a1 ~> b1
r = ((a1 || a1) ~> b1) -> Prod (~>) ('PR (a1 || a1)) ('PR b1)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod (a1 ~> b1
l (a1 ~> b1) -> (a1 ~> b1) -> (a1 || a1) ~> b1
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
||| a1 ~> b1
a1 ~> b1
r)

newtype COPROD k = COPR k
type instance UN COPR (COPR k) = k

type Coprod :: j +-> k -> COPROD j +-> COPROD k
data Coprod p a b where
  Coprod :: {forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Coprod p ('COPR a) ('COPR b) -> p a b
unCoprod :: p a b} -> Coprod p (COPR a) (COPR b)

instance (Profunctor p) => Profunctor (Coprod p) where
  dimap :: forall (c :: COPROD k) (a :: COPROD k) (b :: COPROD j)
       (d :: COPROD j).
(c ~> a) -> (b ~> d) -> Coprod p a b -> Coprod p c d
dimap (Coprod a ~> b
l) (Coprod a ~> b
r) (Coprod p a b
p) = p a b -> Coprod p ('COPR a) ('COPR b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p ('COPR a) ('COPR b)
Coprod ((a ~> a) -> (b ~> b) -> p a b -> p a b
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a ~> b
a ~> a
l a ~> b
b ~> b
r p a b
p)
  (Ob a, Ob b) => r
r \\ :: forall (a :: COPROD k) (b :: COPROD j) r.
((Ob a, Ob b) => r) -> Coprod p a b -> r
\\ Coprod p a b
f = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: k) (b :: j) 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
f
instance (Promonad p) => Promonad (Coprod p) where
  id :: forall (a :: COPROD j). Ob a => Coprod p a a
id = p (UN 'COPR a) (UN 'COPR a)
-> Coprod p ('COPR (UN 'COPR a)) ('COPR (UN 'COPR a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p ('COPR a) ('COPR b)
Coprod p (UN 'COPR a) (UN 'COPR a)
forall (a :: j). Ob a => p a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  Coprod p a b
f . :: forall (b :: COPROD j) (c :: COPROD j) (a :: COPROD j).
Coprod p b c -> Coprod p a b -> Coprod p a c
. Coprod p a b
g = p a b -> Coprod p ('COPR a) ('COPR b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p ('COPR a) ('COPR b)
Coprod (p a b
f p a b -> p a a -> p a b
forall (b :: j) (c :: j) (a :: j). p b c -> p a b -> p 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
. p a a
p a b
g)
instance (CategoryOf k) => CategoryOf (COPROD k) where
  type (~>) = Coprod (~>)
  type Ob a = (Is COPR a, Ob (UN COPR a))

instance (HasCoproducts k, Category cat) => MonoidalProfunctor (Coprod cat :: CAT (COPROD k)) where
  par0 :: Coprod cat Unit Unit
par0 = Coprod cat Unit Unit
Coprod cat ('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 cat a a
id
  Coprod cat a b
f par :: forall (x1 :: COPROD k) (x2 :: COPROD k) (y1 :: COPROD k)
       (y2 :: COPROD k).
Coprod cat x1 x2
-> Coprod cat y1 y2 -> Coprod cat (x1 ** y1) (x2 ** y2)
`par` Coprod cat a b
g = cat (a || a) (b || b)
-> Coprod cat ('COPR (a || a)) ('COPR (b || b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p ('COPR a) ('COPR b)
Coprod (cat a b
a ~> b
f (a ~> b) -> (a ~> b) -> (a || a) ~> (b || 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)
+++ cat a b
a ~> b
g)

instance (HasCoproducts k) => Monoidal (COPROD k) where
  type Unit = COPR InitialObject
  type a ** b = COPR (UN COPR a || UN COPR b)
  leftUnitor :: forall (a :: COPROD k). Ob a => (Unit ** a) ~> a
leftUnitor = ((InitialObject || UN 'COPR a) ~> UN 'COPR a)
-> Coprod
     (~>) ('COPR (InitialObject || UN 'COPR a)) ('COPR (UN 'COPR a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p ('COPR a) ('COPR b)
Coprod (InitialObject ~> UN 'COPR a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate (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
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id)
  leftUnitorInv :: forall (a :: COPROD k). Ob a => a ~> (Unit ** a)
leftUnitorInv = (UN 'COPR a ~> (InitialObject || UN 'COPR a))
-> Coprod
     (~>) ('COPR (UN 'COPR a)) ('COPR (InitialObject || UN 'COPR a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p ('COPR a) ('COPR b)
Coprod (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @InitialObject)
  rightUnitor :: forall (a :: COPROD k). Ob a => (a ** Unit) ~> a
rightUnitor = ((UN 'COPR a || InitialObject) ~> UN 'COPR a)
-> Coprod
     (~>) ('COPR (UN 'COPR a || InitialObject)) ('COPR (UN 'COPR a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p ('COPR a) ('COPR 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 (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
||| InitialObject ~> UN 'COPR a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
initiate)
  rightUnitorInv :: forall (a :: COPROD k). Ob a => a ~> (a ** Unit)
rightUnitorInv = (UN 'COPR a ~> (UN 'COPR a || InitialObject))
-> Coprod
     (~>) ('COPR (UN 'COPR a)) ('COPR (UN 'COPR a || InitialObject))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p ('COPR a) ('COPR b)
Coprod (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @_ @InitialObject)
  associator :: forall (a :: COPROD k) (b :: COPROD k) (c :: COPROD k).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(COPR a) @(COPR b) @(COPR 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 {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p ('COPR a) ('COPR b)
Coprod ((forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj (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)
+++ forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @b @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
||| (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @(b || 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
. forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @b @c) ((Ob (UN 'COPR b || UN 'COPR c), Ob (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 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))
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
\\ (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b Obj (UN 'COPR b)
-> (UN 'COPR c ~> UN 'COPR c)
-> (UN 'COPR b || UN 'COPR c) ~> (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)
+++ forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c))
  associatorInv :: forall (a :: COPROD k) (b :: COPROD k) (c :: COPROD k).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(COPR a) @(COPR b) @(COPR 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 {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p ('COPR a) ('COPR b)
Coprod ((forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @(a || b) @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
. forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @k @a @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
||| (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @k @a @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)
+++ forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @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
\\ (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj (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)
+++ forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b))

instance (HasCoproducts k) => SymMonoidal (COPROD k) where
  swap' :: forall (a :: COPROD k) (a' :: COPROD k) (b :: COPROD k)
       (b' :: COPROD k).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' (Coprod a ~> b
a) (Coprod a ~> b
b) = ((a || a) ~> (b || b))
-> Coprod (~>) ('COPR (a || a)) ('COPR (b || b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p ('COPR a) ('COPR b)
Coprod (Obj b -> (a ~> b) -> a ~> (b || b)
forall (a :: k) (b :: k) (b' :: k).
Obj a -> (b ~> b') -> b ~> (a || b')
forall k (a :: k) (b :: k) (b' :: k).
HasBinaryCoproducts k =>
Obj a -> (b ~> b') -> b ~> (a || b')
rgt' ((a ~> b) -> Obj b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt a ~> b
b) a ~> b
a (a ~> (b || b)) -> (a ~> (b || b)) -> (a || a) ~> (b || b)
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
||| (a ~> b) -> Obj b -> a ~> (b || b)
forall (a :: k) (a' :: k) (b :: k).
(a ~> a') -> Obj b -> a ~> (a' || b)
forall k (a :: k) (a' :: k) (b :: k).
HasBinaryCoproducts k =>
(a ~> a') -> Obj b -> a ~> (a' || b)
lft' a ~> b
b ((a ~> b) -> Obj b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt a ~> b
a))

instance Strong (Coprod (->)) (Coprod (->)) where
  act :: forall (a :: COPROD Type) (b :: COPROD Type) (x :: COPROD Type)
       (y :: COPROD Type).
Coprod (->) a b
-> Coprod (->) x y -> Coprod (->) (Act a x) (Act b y)
act = Coprod (->) a b -> Coprod (->) x y -> Coprod (->) (a ** x) (b ** y)
Coprod (->) a b
-> Coprod (->) x y -> Coprod (->) (Act a x) (Act b y)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: COPROD Type) (x2 :: COPROD Type) (y1 :: COPROD Type)
       (y2 :: COPROD Type).
Coprod (->) x1 x2
-> Coprod (->) y1 y2 -> Coprod (->) (x1 ** y1) (x2 ** y2)
par
instance MonoidalAction (COPROD Type) (COPROD Type) where
  type Act p x = p ** x
  unitor :: forall (x :: COPROD Type). Ob x => Act Unit x ~> x
unitor = (Unit ** 'COPR (UN 'COPR x)) ~> 'COPR (UN 'COPR x)
Act Unit x ~> x
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
forall (a :: COPROD Type). Ob a => (Unit ** a) ~> a
leftUnitor
  unitorInv :: forall (x :: COPROD Type). Ob x => x ~> Act Unit x
unitorInv = x ~> Act Unit x
'COPR (UN 'COPR x) ~> (Unit ** 'COPR (UN 'COPR x))
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
forall (a :: COPROD Type). Ob a => a ~> (Unit ** a)
leftUnitorInv
  multiplicator :: forall (a :: COPROD Type) (b :: COPROD Type) (x :: COPROD Type).
(Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator = ('COPR (UN 'COPR a) ** ('COPR (UN 'COPR b) ** 'COPR (UN 'COPR x)))
~> (('COPR (UN 'COPR a) ** 'COPR (UN 'COPR b))
    ** 'COPR (UN 'COPR x))
Act a (Act b x) ~> Act (a ** b) x
forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
forall (a :: COPROD Type) (b :: COPROD Type) (c :: COPROD Type).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv
  multiplicatorInv :: forall (a :: COPROD Type) (b :: COPROD Type) (x :: COPROD Type).
(Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv = (('COPR (UN 'COPR a) ** 'COPR (UN 'COPR b)) ** 'COPR (UN 'COPR x))
~> ('COPR (UN 'COPR a)
    ** ('COPR (UN 'COPR b) ** 'COPR (UN 'COPR x)))
Act (a ** b) x ~> Act a (Act b x)
forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
forall (a :: COPROD Type) (b :: COPROD Type) (c :: COPROD Type).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator

instance Strong (->) (Coprod (->)) where
  a -> b
l act :: forall a b (x :: COPROD Type) (y :: COPROD Type).
(a -> b) -> Coprod (->) x y -> Coprod (->) (Act a x) (Act b y)
`act` Coprod a -> b
r = ((a, a) -> (b, b)) -> Coprod (->) ('COPR (a, a)) ('COPR (b, b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p ('COPR a) ('COPR b)
Coprod (a -> b
l (a -> b) -> (a -> b) -> (a ** a) -> (b ** b)
forall x1 x2 y1 y2.
(x1 -> x2) -> (y1 -> y2) -> (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` a -> b
r)
instance MonoidalAction Type (COPROD Type) where
  type Act (p :: Type) (COPR x :: COPROD Type) = COPR (p ** x)
  unitor :: forall (x :: COPROD Type). Ob x => Act Unit x ~> x
unitor = (((), UN 'COPR x) -> UN 'COPR x)
-> Coprod (->) ('COPR ((), UN 'COPR x)) ('COPR (UN 'COPR x))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p ('COPR a) ('COPR b)
Coprod (Unit ** UN 'COPR x) ~> UN 'COPR x
((), UN 'COPR x) -> UN 'COPR x
forall a. Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor
  unitorInv :: forall (x :: COPROD Type). Ob x => x ~> Act Unit x
unitorInv = (UN 'COPR x -> ((), UN 'COPR x))
-> Coprod (->) ('COPR (UN 'COPR x)) ('COPR ((), UN 'COPR x))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p ('COPR a) ('COPR b)
Coprod UN 'COPR x ~> (Unit ** UN 'COPR x)
UN 'COPR x -> ((), UN 'COPR x)
forall a. Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv
  multiplicator :: forall a b (x :: COPROD Type).
(Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator = ((a, (b, UN 'COPR x)) -> ((a, b), UN 'COPR x))
-> Coprod
     (->) ('COPR (a, (b, UN 'COPR x))) ('COPR ((a, b), UN 'COPR x))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p ('COPR a) ('COPR b)
Coprod (a ** (b ** UN 'COPR x)) ~> ((a ** b) ** UN 'COPR x)
(a, (b, UN 'COPR x)) -> ((a, b), UN 'COPR x)
forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
forall a b c.
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv
  multiplicatorInv :: forall a b (x :: COPROD Type).
(Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv = (((a, b), UN 'COPR x) -> (a, (b, UN 'COPR x)))
-> Coprod
     (->) ('COPR ((a, b), UN 'COPR x)) ('COPR (a, (b, UN 'COPR x)))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p ('COPR a) ('COPR b)
Coprod ((a ** b) ** UN 'COPR x) ~> (a ** (b ** UN 'COPR x))
((a, b), UN 'COPR x) -> (a, (b, UN 'COPR x))
forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
forall a b c.
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator

instance Strong (Coprod (->)) (->) where
  f :: Coprod (->) a b
f@Coprod{} act :: forall (a :: COPROD Type) (b :: COPROD Type) x y.
Coprod (->) a b -> (x -> y) -> Act a x -> Act b y
`act` x -> y
g = Coprod (->) ('COPR (Either a x)) ('COPR (Either b y))
-> Either a x -> Either b y
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Coprod p ('COPR a) ('COPR b) -> p a b
unCoprod (Coprod (->) a b
f Coprod (->) a b
-> Coprod (->) ('COPR x) ('COPR y)
-> Coprod (->) (a ** 'COPR x) (b ** 'COPR y)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall (x1 :: COPROD Type) (x2 :: COPROD Type) (y1 :: COPROD Type)
       (y2 :: COPROD Type).
Coprod (->) x1 x2
-> Coprod (->) y1 y2 -> Coprod (->) (x1 ** y1) (x2 ** y2)
`par` (x -> y) -> Coprod (->) ('COPR x) ('COPR y)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Coprod p ('COPR a) ('COPR b)
Coprod x -> y
g)
instance MonoidalAction (COPROD Type) Type where
  type Act (p :: COPROD Type) (x :: Type) = UN COPR (p ** COPR x)
  unitor :: forall x. Ob x => Act Unit x ~> x
unitor = Coprod (->) ('COPR (Either Void x)) ('COPR x) -> Either Void x -> x
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Coprod p ('COPR a) ('COPR b) -> p a b
unCoprod (Unit ** 'COPR x) ~> 'COPR x
Coprod (->) ('COPR (Either Void x)) ('COPR x)
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
forall (a :: COPROD Type). Ob a => (Unit ** a) ~> a
leftUnitor
  unitorInv :: forall x. Ob x => x ~> Act Unit x
unitorInv = Coprod (->) ('COPR x) ('COPR (Either Void x)) -> x -> Either Void x
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Coprod p ('COPR a) ('COPR b) -> p a b
unCoprod 'COPR x ~> (Unit ** 'COPR x)
Coprod (->) ('COPR x) ('COPR (Either Void x))
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
forall (a :: COPROD Type). Ob a => a ~> (Unit ** a)
leftUnitorInv
  multiplicator :: forall (a :: COPROD Type) (b :: COPROD Type) x.
(Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator = Coprod
  (->)
  ('COPR (Either (UN 'COPR a) (Either (UN 'COPR b) x)))
  ('COPR (Either (Either (UN 'COPR a) (UN 'COPR b)) x))
-> Either (UN 'COPR a) (Either (UN 'COPR b) x)
-> Either (Either (UN 'COPR a) (UN 'COPR b)) x
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Coprod p ('COPR a) ('COPR b) -> p a b
unCoprod ('COPR (UN 'COPR a) ** ('COPR (UN 'COPR b) ** 'COPR x))
~> (('COPR (UN 'COPR a) ** 'COPR (UN 'COPR b)) ** 'COPR x)
Coprod
  (->)
  ('COPR (Either (UN 'COPR a) (Either (UN 'COPR b) x)))
  ('COPR (Either (Either (UN 'COPR a) (UN 'COPR b)) x))
forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
forall (a :: COPROD Type) (b :: COPROD Type) (c :: COPROD Type).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv
  multiplicatorInv :: forall (a :: COPROD Type) (b :: COPROD Type) x.
(Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv = Coprod
  (->)
  ('COPR (Either (Either (UN 'COPR a) (UN 'COPR b)) x))
  ('COPR (Either (UN 'COPR a) (Either (UN 'COPR b) x)))
-> Either (Either (UN 'COPR a) (UN 'COPR b)) x
-> Either (UN 'COPR a) (Either (UN 'COPR b) x)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Coprod p ('COPR a) ('COPR b) -> p a b
unCoprod (('COPR (UN 'COPR a) ** 'COPR (UN 'COPR b)) ** 'COPR x)
~> ('COPR (UN 'COPR a) ** ('COPR (UN 'COPR b) ** 'COPR x))
Coprod
  (->)
  ('COPR (Either (Either (UN 'COPR a) (UN 'COPR b)) x))
  ('COPR (Either (UN 'COPR a) (Either (UN 'COPR b) x)))
forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
forall (a :: COPROD Type) (b :: COPROD Type) (c :: COPROD Type).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator

class (Act a b ~ (a || b)) => ActIsCoprod a b
instance (Act a b ~ (a || b)) => ActIsCoprod a b
class (Strong ((~>) :: CAT k) p, HasCoproducts k, forall (a :: k) (b :: k). ActIsCoprod a b) => StrongCoprod (p :: CAT k)
instance (Strong ((~>) :: CAT k) p, HasCoproducts k, forall (a :: k) (b :: k). ActIsCoprod a b) => StrongCoprod (p :: CAT k)

left' :: forall {k} (p :: CAT k) c a b. (StrongCoprod p, Ob c) => p a b -> p (a || c) (b || c)
left' :: forall {k} (p :: CAT k) (c :: k) (a :: k) (b :: k).
(StrongCoprod p, Ob c) =>
p a b -> p (a || c) (b || c)
left' p a b
p = ((a || c) ~> (c || a))
-> ((c || b) ~> (b || c))
-> p (c || a) (c || b)
-> p (a || c) (b || c)
forall (c :: k) (a :: k) (b :: k) (d :: k).
(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 (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(a || b) ~> (b || a)
swapCoprod @_ @a @c) (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(a || b) ~> (b || a)
swapCoprod @_ @c @b) (forall {k} (p :: CAT k) (c :: k) (a :: k) (b :: k).
(StrongCoprod p, Ob c) =>
p a b -> p (c || a) (c || b)
forall (p :: CAT k) (c :: k) (a :: k) (b :: k).
(StrongCoprod p, Ob c) =>
p a b -> p (c || a) (c || b)
right' @_ @c p a b
p) ((Ob a, Ob b) => p (a || c) (b || c))
-> p a b -> p (a || c) (b || c)
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

right' :: forall {k} (p :: CAT k) c a b. (StrongCoprod p, Ob c) => p a b -> p (c || a) (c || b)
right' :: forall {k} (p :: CAT k) (c :: k) (a :: k) (b :: k).
(StrongCoprod p, Ob c) =>
p a b -> p (c || a) (c || b)
right' p a b
p = forall {m} {m'} {c} {d} (w :: m +-> m') (p :: c +-> d) (a :: m')
       (b :: m) (x :: d) (y :: c).
Strong w p =>
w a b -> p x y -> p (Act a x) (Act b y)
forall (w :: k +-> k) (p :: k +-> k) (a :: k) (b :: k) (x :: k)
       (y :: k).
Strong w p =>
w a b -> p x y -> p (Act a x) (Act b y)
act @((~>) :: CAT k) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c) p a b
p