{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Category.Instance.Product where

import Prelude (type (~))

import Proarrow.Category.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal, swap')
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), Strong (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), type (+->))
import Proarrow.Preorder.ThinCategory (Codiscrete, Discrete (..), ThinProfunctor (..), anyArr)
import Proarrow.Profunctor.Representable (Representable (..))

type Fst :: (a, b) -> a
type family Fst a where
  Fst '(a, b) = a
type Snd :: (a, b) -> b
type family Snd a where
  Snd '(a, b) = b

type (:**:) :: j1 +-> k1 -> j2 +-> k2 -> (j1, j2) +-> (k1, k2)
data (c :**: d) a b where
  (:**:) :: c a1 b1 -> d a2 b2 -> (c :**: d) '(a1, a2) '(b1, b2)

instance (CategoryOf k1, CategoryOf k2) => CategoryOf (k1, k2) where
  type (~>) = (~>) :**: (~>)
  type Ob a = (a ~ '(Fst a, Snd a), Ob (Fst a), Ob (Snd a))

-- | The product promonad of promonads `p` and `q`.
instance (Promonad p, Promonad q) => Promonad (p :**: q) where
  id :: forall (a :: (j1, j2)). Ob a => (:**:) p q a a
id = p (Fst a) (Fst a)
forall (a :: j1). Ob a => p a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id p (Fst a) (Fst a)
-> q (Snd a) (Snd a) -> (:**:) p q '(Fst a, Snd a) '(Fst a, Snd a)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: q (Snd a) (Snd a)
forall (a :: j2). Ob a => q a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  (p a1 b1
f1 :**: q a2 b2
f2) . :: forall (b :: (j1, j2)) (c :: (j1, j2)) (a :: (j1, j2)).
(:**:) p q b c -> (:**:) p q a b -> (:**:) p q a c
. (p a1 b1
g1 :**: q a2 b2
g2) = (p a1 b1
f1 p a1 b1 -> p a1 a1 -> p a1 b1
forall (b :: j1) (c :: j1) (a :: j1). 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 a1 a1
p a1 b1
g1) p a1 b1 -> q a2 b2 -> (:**:) p q '(a1, a2) '(b1, b2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (q a2 b2
f2 q a2 b2 -> q a2 a2 -> q a2 b2
forall (b :: j2) (c :: j2) (a :: j2). q b c -> q a b -> q 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
. q a2 a2
q a2 b2
g2)

instance (Profunctor p, Profunctor q) => Profunctor (p :**: q) where
  dimap :: forall (c :: (k1, k2)) (a :: (k1, k2)) (b :: (j1, j2))
       (d :: (j1, j2)).
(c ~> a) -> (b ~> d) -> (:**:) p q a b -> (:**:) p q c d
dimap (a1 ~> b1
l1 :**: a2 ~> b2
l2) (a1 ~> b1
r1 :**: a2 ~> b2
r2) (p a1 b1
f1 :**: q a2 b2
f2) = (a1 ~> a1) -> (b1 ~> b1) -> p a1 b1 -> p a1 b1
forall (c :: k1) (a :: k1) (b :: j1) (d :: j1).
(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 a1 ~> b1
a1 ~> a1
l1 a1 ~> b1
b1 ~> b1
r1 p a1 b1
f1 p a1 b1 -> q a2 b2 -> (:**:) p q '(a1, a2) '(b1, b2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (a2 ~> a2) -> (b2 ~> b2) -> q a2 b2 -> q a2 b2
forall (c :: k2) (a :: k2) (b :: j2) (d :: j2).
(c ~> a) -> (b ~> d) -> q a b -> q 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 a2 ~> b2
a2 ~> a2
l2 a2 ~> b2
b2 ~> b2
r2 q a2 b2
f2
  (Ob a, Ob b) => r
r \\ :: forall (a :: (k1, k2)) (b :: (j1, j2)) r.
((Ob a, Ob b) => r) -> (:**:) p q a b -> r
\\ (p a1 b1
f :**: q a2 b2
g) = r
(Ob a1, Ob b1) => r
(Ob a, Ob b) => r
r ((Ob a1, Ob b1) => r) -> p a1 b1 -> r
forall (a :: k1) (b :: j1) 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 a1 b1
f ((Ob a2, Ob b2) => r) -> q a2 b2 -> r
forall (a :: k2) (b :: j2) r. ((Ob a, Ob b) => r) -> q 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
\\ q a2 b2
g

instance (DaggerProfunctor p, DaggerProfunctor q) => DaggerProfunctor (p :**: q) where
  dagger :: forall (a :: (j1, j2)) (b :: (j1, j2)).
(:**:) p q a b -> (:**:) p q b a
dagger (p a1 b1
f :**: q a2 b2
g) = p a1 b1 -> p b1 a1
forall (a :: j1) (b :: j1). p a b -> p b a
forall {j} (p :: PRO j j) (a :: j) (b :: j).
DaggerProfunctor p =>
p a b -> p b a
dagger p a1 b1
f p b1 a1 -> q b2 a2 -> (:**:) p q '(b1, b2) '(a1, a2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: q a2 b2 -> q b2 a2
forall (a :: j2) (b :: j2). q a b -> q b a
forall {j} (p :: PRO j j) (a :: j) (b :: j).
DaggerProfunctor p =>
p a b -> p b a
dagger q a2 b2
g

instance (ThinProfunctor p, ThinProfunctor q) => ThinProfunctor (p :**: q) where
  type HasArrow (p :**: q) '(a1, a2) '(b1, b2) = (HasArrow p a1 b1, HasArrow q a2 b2)
  arr :: forall (a :: (k1, k2)) (b :: (j1, j2)).
(Ob a, Ob b, HasArrow (p :**: q) a b) =>
(:**:) p q a b
arr = p (Fst a) (Fst b)
forall (a :: k1) (b :: j1). (Ob a, Ob b, HasArrow p a b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr p (Fst a) (Fst b)
-> q (Snd a) (Snd b) -> (:**:) p q '(Fst a, Snd a) '(Fst b, Snd b)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: q (Snd a) (Snd b)
forall (a :: k2) (b :: j2). (Ob a, Ob b, HasArrow q a b) => q a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
arr
  withArr :: forall (a :: (k1, k2)) (b :: (j1, j2)) r.
(:**:) p q a b -> (HasArrow (p :**: q) a b => r) -> r
withArr (p a1 b1
f :**: q a2 b2
g) HasArrow (p :**: q) a b => r
r = p a1 b1 -> (HasArrow p a1 b1 => r) -> r
forall (a :: k1) (b :: j1) r. p a b -> (HasArrow p a b => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> (HasArrow p a b => r) -> r
withArr p a1 b1
f (q a2 b2 -> (HasArrow q a2 b2 => r) -> r
forall (a :: k2) (b :: j2) r. q a b -> (HasArrow q a b => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> (HasArrow p a b => r) -> r
withArr q a2 b2
g r
HasArrow q a2 b2 => r
HasArrow (p :**: q) a b => r
r)

instance (Codiscrete p, Codiscrete q) => Codiscrete (p :**: q) where
  anyArr :: forall (a :: (k1, k2)) (b :: (j1, j2)).
(Ob a, Ob b) =>
(:**:) p q a b
anyArr = p (Fst a) (Fst b)
forall (a :: k1) (b :: j1). (Ob a, Ob b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Codiscrete p, Ob a, Ob b) =>
p a b
anyArr p (Fst a) (Fst b)
-> q (Snd a) (Snd b) -> (:**:) p q '(Fst a, Snd a) '(Fst b, Snd b)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: q (Snd a) (Snd b)
forall (a :: k2) (b :: j2). (Ob a, Ob b) => q a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Codiscrete p, Ob a, Ob b) =>
p a b
anyArr

instance (Discrete p, Discrete q) => Discrete (p :**: q) where
  withEq :: forall (a :: (j1, j2)) (b :: (j1, j2)) r.
(:**:) p q a b -> ((a ~ b) => r) -> r
withEq (p a1 b1
f :**: q a2 b2
g) (a ~ b) => r
r = p a1 b1 -> ((a1 ~ b1) => r) -> r
forall (a :: j1) (b :: j1) r. p a b -> ((a ~ b) => r) -> r
forall {k} (p :: k +-> k) (a :: k) (b :: k) r.
Discrete p =>
p a b -> ((a ~ b) => r) -> r
withEq p a1 b1
f (q a2 b2 -> ((a2 ~ b2) => r) -> r
forall (a :: j2) (b :: j2) r. q a b -> ((a ~ b) => r) -> r
forall {k} (p :: k +-> k) (a :: k) (b :: k) r.
Discrete p =>
p a b -> ((a ~ b) => r) -> r
withEq q a2 b2
g r
(a2 ~ b2) => r
(a ~ b) => r
r)

instance (Representable p, Representable q) => Representable (p :**: q) where
  type (p :**: q) % '(a, b) = '(p % a, q % b)
  index :: forall (a :: (k1, k2)) (b :: (j1, j2)).
(:**:) p q a b -> a ~> ((p :**: q) % b)
index (p a1 b1
p :**: q a2 b2
q) = p a1 b1 -> a1 ~> (p % b1)
forall (a :: k1) (b :: j1). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index p a1 b1
p (a1 ~> (p % b1))
-> (a2 ~> (q % b2)) -> (:**:) (~>) (~>) '(a1, a2) '(p % b1, q % b2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: q a2 b2 -> a2 ~> (q % b2)
forall (a :: k2) (b :: j2). q a b -> a ~> (q % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index q a2 b2
q
  tabulate :: forall (b :: (j1, j2)) (a :: (k1, k2)).
Ob b =>
(a ~> ((p :**: q) % b)) -> (:**:) p q a b
tabulate (a1 ~> b1
f :**: a2 ~> b2
g) = (a1 ~> (p % Fst b)) -> p a1 (Fst b)
forall (b :: j1) (a :: k1). Ob b => (a ~> (p % b)) -> p a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate a1 ~> b1
a1 ~> (p % Fst b)
f p a1 (Fst b)
-> q a2 (Snd b) -> (:**:) p q '(a1, a2) '(Fst b, Snd b)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (a2 ~> (q % Snd b)) -> q a2 (Snd b)
forall (b :: j2) (a :: k2). Ob b => (a ~> (q % b)) -> q a b
forall {j} {k} (p :: j +-> k) (b :: j) (a :: k).
(Representable p, Ob b) =>
(a ~> (p % b)) -> p a b
tabulate a2 ~> b2
a2 ~> (q % Snd b)
g
  repMap :: forall (a :: (j1, j2)) (b :: (j1, j2)).
(a ~> b) -> ((p :**: q) % a) ~> ((p :**: q) % b)
repMap (a1 ~> b1
f :**: a2 ~> b2
g) = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j1 +-> k1) (a :: j1) (b :: j1).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @p a1 ~> b1
f ((p % a1) ~> (p % b1))
-> ((q % a2) ~> (q % b2))
-> (:**:) (~>) (~>) '(p % a1, q % a2) '(p % b1, q % b2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: j2 +-> k2) (a :: j2) (b :: j2).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @q a2 ~> b2
g

instance (MonoidalProfunctor p, MonoidalProfunctor q) => MonoidalProfunctor (p :**: q) where
  par0 :: (:**:) p q Unit Unit
par0 = p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0 p Unit Unit
-> q Unit Unit -> (:**:) p q '(Unit, Unit) '(Unit, Unit)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: q Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0
  (p a1 b1
f1 :**: q a2 b2
f2) par :: forall (x1 :: (k1, k2)) (x2 :: (j1, j2)) (y1 :: (k1, k2))
       (y2 :: (j1, j2)).
(:**:) p q x1 x2
-> (:**:) p q y1 y2 -> (:**:) p q (x1 ** y1) (x2 ** y2)
`par` (p a1 b1
g1 :**: q a2 b2
g2) = (p a1 b1
f1 p a1 b1 -> p a1 b1 -> p (a1 ** a1) (b1 ** b1)
forall (x1 :: k1) (x2 :: j1) (y1 :: k1) (y2 :: j1).
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 a1 b1
g1) p (a1 ** a1) (b1 ** b1)
-> q (a2 ** a2) (b2 ** b2)
-> (:**:) p q '(a1 ** a1, a2 ** a2) '(b1 ** b1, b2 ** b2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (q a2 b2
f2 q a2 b2 -> q a2 b2 -> q (a2 ** a2) (b2 ** b2)
forall (x1 :: k2) (x2 :: j2) (y1 :: k2) (y2 :: j2).
q x1 x2 -> q y1 y2 -> q (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` q a2 b2
g2)

instance (Monoidal j, Monoidal k) => Monoidal (j, k) where
  type Unit = '(Unit, Unit)
  type '(a1, a2) ** '(b1, b2) = '(a1 ** b1, a2 ** b2)
  leftUnitor :: forall (a :: (j, k)). Ob a => (Unit ** a) ~> a
leftUnitor @'(a1, a2) = forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @j @a1 ((Unit ** Fst a) ~> Fst a)
-> ((Unit ** Snd a) ~> Snd a)
-> (:**:) (~>) (~>) '(Unit ** Fst a, Unit ** Snd a) '(Fst a, Snd a)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @k @a2
  leftUnitorInv :: forall (a :: (j, k)). Ob a => a ~> (Unit ** a)
leftUnitorInv @'(a1, a2) = forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @j @a1 (Fst a ~> (Unit ** Fst a))
-> (Snd a ~> (Unit ** Snd a))
-> (:**:) (~>) (~>) '(Fst a, Snd a) '(Unit ** Fst a, Unit ** Snd a)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @k @a2
  rightUnitor :: forall (a :: (j, k)). Ob a => (a ** Unit) ~> a
rightUnitor @'(a1, a2) = forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor @j @a1 ((Fst a ** Unit) ~> Fst a)
-> ((Snd a ** Unit) ~> Snd a)
-> (:**:) (~>) (~>) '(Fst a ** Unit, Snd a ** Unit) '(Fst a, Snd a)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor @k @a2
  rightUnitorInv :: forall (a :: (j, k)). Ob a => a ~> (a ** Unit)
rightUnitorInv @'(a1, a2) = forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv @j @a1 (Fst a ~> (Fst a ** Unit))
-> (Snd a ~> (Snd a ** Unit))
-> (:**:) (~>) (~>) '(Fst a, Snd a) '(Fst a ** Unit, Snd a ** Unit)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv @k @a2
  associator :: forall (a :: (j, k)) (b :: (j, k)) (c :: (j, k)).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @'(a1, a2) @'(b1, b2) @'(c1, c2) = forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @j @a1 @b1 @c1 (((Fst a ** Fst b) ** Fst c) ~> (Fst a ** (Fst b ** Fst c)))
-> (((Snd a ** Snd b) ** Snd c) ~> (Snd a ** (Snd b ** Snd c)))
-> (:**:)
     (~>)
     (~>)
     '((Fst a ** Fst b) ** Fst c, (Snd a ** Snd b) ** Snd c)
     '(Fst a ** (Fst b ** Fst c), Snd a ** (Snd b ** Snd c))
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @a2 @b2 @c2
  associatorInv :: forall (a :: (j, k)) (b :: (j, k)) (c :: (j, k)).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @'(a1, a2) @'(b1, b2) @'(c1, c2) = forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @j @a1 @b1 @c1 ((Fst a ** (Fst b ** Fst c)) ~> ((Fst a ** Fst b) ** Fst c))
-> ((Snd a ** (Snd b ** Snd c)) ~> ((Snd a ** Snd b) ** Snd c))
-> (:**:)
     (~>)
     (~>)
     '(Fst a ** (Fst b ** Fst c), Snd a ** (Snd b ** Snd c))
     '((Fst a ** Fst b) ** Fst c, (Snd a ** Snd b) ** Snd c)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @a2 @b2 @c2

instance (SymMonoidal j, SymMonoidal k) => SymMonoidal (j, k) where
  swap' :: forall (a :: (j, k)) (a' :: (j, k)) (b :: (j, k)) (b' :: (j, k)).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' (a1 ~> b1
a1 :**: a2 ~> b2
a2) (a1 ~> b1
b1 :**: a2 ~> b2
b2) = (a1 ~> b1) -> (a1 ~> b1) -> (a1 ** a1) ~> (b1 ** b1)
forall (a :: j) (a' :: j) (b :: j) (b' :: j).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
SymMonoidal k =>
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' a1 ~> b1
a1 a1 ~> b1
b1 ((a1 ** a1) ~> (b1 ** b1))
-> ((a2 ** a2) ~> (b2 ** b2))
-> (:**:) (~>) (~>) '(a1 ** a1, a2 ** a2) '(b1 ** b1, b2 ** b2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (a2 ~> b2) -> (a2 ~> b2) -> (a2 ** a2) ~> (b2 ** b2)
forall (a :: k) (a' :: k) (b :: k) (b' :: k).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
SymMonoidal k =>
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' a2 ~> b2
a2 a2 ~> b2
b2

instance (Strong v p, Strong w q) => Strong (v :**: w) (p :**: q) where
  act :: forall (a :: (k1, k2)) (b :: (j1, j2)) (x :: (k1, k2))
       (y :: (j1, j2)).
(:**:) v w a b -> (:**:) p q x y -> (:**:) p q (Act a x) (Act b y)
act (v a1 b1
p :**: w a2 b2
q) (p a1 b1
x :**: q a2 b2
y) = v a1 b1 -> p a1 b1 -> p (Act a1 a1) (Act b1 b1)
forall (a :: k1) (b :: j1) (x :: k1) (y :: j1).
v a b -> p x y -> p (Act a x) (Act b y)
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)
act v a1 b1
p p a1 b1
x p (Act a1 a1) (Act b1 b1)
-> q (Act a2 a2) (Act b2 b2)
-> (:**:) p q '(Act a1 a1, Act a2 a2) '(Act b1 b1, Act b2 b2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: w a2 b2 -> q a2 b2 -> q (Act a2 a2) (Act b2 b2)
forall (a :: k2) (b :: j2) (x :: k2) (y :: j2).
w a b -> q x y -> q (Act a x) (Act b y)
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)
act w a2 b2
q q a2 b2
y
instance (MonoidalAction n j, MonoidalAction m k) => MonoidalAction (n, m) (j, k) where
  type Act '(p, q) '(x, y) = '(Act p x, Act q y)
  unitor :: forall (x :: (j, k)). Ob x => Act Unit x ~> x
unitor = forall m k (x :: k). (MonoidalAction m k, Ob x) => Act Unit x ~> x
unitor @n (Act Unit (Fst x) ~> Fst x)
-> (Act Unit (Snd x) ~> Snd x)
-> (:**:)
     (~>) (~>) '(Act Unit (Fst x), Act Unit (Snd x)) '(Fst x, Snd x)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall m k (x :: k). (MonoidalAction m k, Ob x) => Act Unit x ~> x
unitor @m
  unitorInv :: forall (x :: (j, k)). Ob x => x ~> Act Unit x
unitorInv = forall m k (x :: k). (MonoidalAction m k, Ob x) => x ~> Act Unit x
unitorInv @n (Fst x ~> Act Unit (Fst x))
-> (Snd x ~> Act Unit (Snd x))
-> (:**:)
     (~>) (~>) '(Fst x, Snd x) '(Act Unit (Fst x), Act Unit (Snd x))
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall m k (x :: k). (MonoidalAction m k, Ob x) => x ~> Act Unit x
unitorInv @m
  multiplicator :: forall (a :: (n, m)) (b :: (n, m)) (x :: (j, k)).
(Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator @'(p, q) @'(r, s) @'(x, y) = forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator @n @j @p @r @x (Act (Fst a) (Act (Fst b) (Fst x)) ~> Act (Fst a ** Fst b) (Fst x))
-> (Act (Snd a) (Act (Snd b) (Snd x))
    ~> Act (Snd a ** Snd b) (Snd x))
-> (:**:)
     (~>)
     (~>)
     '(Act (Fst a) (Act (Fst b) (Fst x)),
       Act (Snd a) (Act (Snd b) (Snd x)))
     '(Act (Fst a ** Fst b) (Fst x), Act (Snd a ** Snd b) (Snd x))
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator @m @k @q @s @y
  multiplicatorInv :: forall (a :: (n, m)) (b :: (n, m)) (x :: (j, k)).
(Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv @'(p, q) @'(r, s) @'(x, y) = forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv @n @j @p @r @x (Act (Fst a ** Fst b) (Fst x) ~> Act (Fst a) (Act (Fst b) (Fst x)))
-> (Act (Snd a ** Snd b) (Snd x)
    ~> Act (Snd a) (Act (Snd b) (Snd x)))
-> (:**:)
     (~>)
     (~>)
     '(Act (Fst a ** Fst b) (Fst x), Act (Snd a ** Snd b) (Snd x))
     '(Act (Fst a) (Act (Fst b) (Fst x)),
       Act (Snd a) (Act (Snd b) (Snd x)))
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv @m @k @q @s @y