{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Monoidal.Action where

import Data.Kind (Constraint)

import Proarrow.Category.Instance.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Sub (SUBCAT (..), Sub (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal (Monoidal (..), Tensor)
import Proarrow.Colimit.BinaryCoproduct
  ( COPROD (..)
  , Coprod (..)
  , HasBinaryCoproducts (..)
  , HasCoproducts
  , associatorCoprod
  , associatorCoprodInv
  , leftUnitorCoprod
  , leftUnitorCoprodInv
  )
import Proarrow.Core (CategoryOf (..), OB, Promonad (..), obj, type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Limit.BinaryProduct
  ( HasBinaryProducts (..)
  , HasProducts
  , PROD (..)
  , Prod (..)
  , associatorProd
  , associatorProdInv
  , leftUnitorProd
  , leftUnitorProdInv
  )
import Proarrow.Profunctor.Representable (Rep (..), Representable (..))

type Act :: (m, k) +-> k -> m -> k -> k
type Act t a x = t % '(a, x)

type MonoidalAction :: forall {m} {k}. (m, k) +-> k -> Constraint
class (Representable t, Monoidal m) => MonoidalAction (t :: (m, k) +-> k) where
  unitor :: (Ob x) => Act t Unit x ~> x
  unitorInv :: (Ob x) => x ~> Act t Unit x
  multiplicator :: (Ob a, Ob b, Ob x) => Act t (a ** b) x ~> Act t a (Act t b x)
  multiplicatorInv :: (Ob a, Ob b, Ob x) => Act t a (Act t b x) ~> Act t (a ** b) x

actHom :: (Representable t) => a ~> b -> x ~> y -> Act t a x ~> Act t b y
actHom :: forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k)
       (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
actHom @t a ~> b
l x ~> y
r = forall {j} {k} (p :: j +-> k) (a :: j) (b :: j).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
forall (p :: (m, k) +-> k) (a :: (m, k)) (b :: (m, k)).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @t (a ~> b
l (a ~> b) -> (x ~> y) -> (:**:) (~>) (~>) '(a, x) '(b, y)
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)
:**: x ~> y
r)

composeActs
  :: forall {m} {k} t (x :: m) (y :: m) (c :: k) (a :: k) (b :: k)
   . (MonoidalAction t, Ob x, Ob y, Ob c)
  => a ~> Act t x b
  -> b ~> Act t y c
  -> a ~> Act t (x ** y) c
composeActs :: forall {m} {k} (t :: (m, k) +-> k) (x :: m) (y :: m) (c :: k)
       (a :: k) (b :: k).
(MonoidalAction t, Ob x, Ob y, Ob c) =>
(a ~> Act t x b) -> (b ~> Act t y c) -> a ~> Act t (x ** y) c
composeActs a ~> Act t x b
f b ~> Act t y c
g = forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t a (Act t b x) ~> Act t (a ** b) x
forall (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t a (Act t b x) ~> Act t (a ** b) x
multiplicatorInv @t @x @y @c (Act t x (Act t y c) ~> (t % '(x ** y, c)))
-> (a ~> Act t x (Act t y c)) -> a ~> (t % '(x ** y, c))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k)
       (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
forall (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k) (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
actHom @t (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x) b ~> Act t y c
g (Act t x b ~> Act t x (Act t y c))
-> (a ~> Act t x b) -> a ~> Act t x (Act t y c)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> Act t x b
f

decomposeActs
  :: forall {m} {k} t (x :: m) (y :: m) (c :: k) (a :: k) (b :: k)
   . (MonoidalAction t, Ob x, Ob y, Ob c)
  => Act t y c ~> b
  -> Act t x b ~> a
  -> Act t (x ** y) c ~> a
decomposeActs :: forall {m} {k} (t :: (m, k) +-> k) (x :: m) (y :: m) (c :: k)
       (a :: k) (b :: k).
(MonoidalAction t, Ob x, Ob y, Ob c) =>
(Act t y c ~> b) -> (Act t x b ~> a) -> Act t (x ** y) c ~> a
decomposeActs Act t y c ~> b
f Act t x b ~> a
g = Act t x b ~> a
g (Act t x b ~> a)
-> ((t % '(x ** y, c)) ~> Act t x b) -> (t % '(x ** y, c)) ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k)
       (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
forall (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k) (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
actHom @t (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x) Act t y c ~> b
f ((t % '(x, Act t y c)) ~> Act t x b)
-> ((t % '(x ** y, c)) ~> (t % '(x, Act t y c)))
-> (t % '(x ** y, c)) ~> Act t x b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t (a ** b) x ~> Act t a (Act t b x)
forall (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t (a ** b) x ~> Act t a (Act t b x)
multiplicator @t @x @y @c

data family NoAction :: ((), k) +-> k
instance (CategoryOf k) => FunctorForRep (NoAction :: ((), k) +-> k) where
  type NoAction @ '(a, x) = x
  fmap :: forall (a :: ((), k)) (b :: ((), k)).
(a ~> b) -> (NoAction @ a) ~> (NoAction @ b)
fmap (Unit a1 b1
U.Unit :**: a2 ~> b2
f) = a2 ~> b2
(NoAction @ a) ~> (NoAction @ b)
f
instance (CategoryOf k) => MonoidalAction (Rep NoAction :: ((), k) +-> k) where
  unitor :: forall (x :: k). Ob x => Act (Rep NoAction) Unit x ~> x
unitor = x ~> x
(Rep NoAction % '(Unit, x)) ~> x
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  unitorInv :: forall (x :: k). Ob x => x ~> Act (Rep NoAction) Unit x
unitorInv = x ~> x
x ~> (Rep NoAction % '(Unit, x))
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  multiplicator :: forall (a :: ()) (b :: ()) (x :: k).
(Ob a, Ob b, Ob x) =>
Act (Rep NoAction) (a ** b) x
~> Act (Rep NoAction) a (Act (Rep NoAction) b x)
multiplicator = x ~> x
(Rep NoAction % '(a ** b, x))
~> (Rep NoAction % '(a, Act (Rep NoAction) b x))
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  multiplicatorInv :: forall (a :: ()) (b :: ()) (x :: k).
(Ob a, Ob b, Ob x) =>
Act (Rep NoAction) a (Act (Rep NoAction) b x)
~> Act (Rep NoAction) (a ** b) x
multiplicatorInv = x ~> x
(Rep NoAction % '(a, Act (Rep NoAction) b x))
~> (Rep NoAction % '(a ** b, x))
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id

data family OpAction :: (m, k) +-> k -> (OPPOSITE m, OPPOSITE k) +-> OPPOSITE k
instance (Representable (t :: (m, k) +-> k), CategoryOf m) => FunctorForRep (OpAction t) where
  type OpAction t @ '(OP a, OP x) = OP (t % '(a, x))
  fmap :: forall (a :: (OPPOSITE m, OPPOSITE k))
       (b :: (OPPOSITE m, OPPOSITE k)).
(a ~> b) -> (OpAction t @ a) ~> (OpAction t @ b)
fmap (Op b1 ~> a1
l :**: Op b1 ~> a1
r) = ((t % '(b1, b1)) ~> (t % '(a1, a1)))
-> Op (~>) ('OP (t % '(a1, a1))) ('OP (t % '(b1, b1)))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op (forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k)
       (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
forall (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k) (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
actHom @t b1 ~> a1
l b1 ~> a1
r)
instance (MonoidalAction t) => MonoidalAction (Rep (OpAction t)) where
  unitor :: forall (x :: OPPOSITE k).
Ob x =>
Act (Rep (OpAction t)) Unit x ~> x
unitor = (UN 'OP x ~> (t % '(Unit, UN 'OP x)))
-> Op (~>) ('OP (t % '(Unit, UN 'OP x))) ('OP (UN 'OP x))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op (forall {m} {k} (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
x ~> Act t Unit x
forall (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
x ~> Act t Unit x
unitorInv @t)
  unitorInv :: forall (x :: OPPOSITE k).
Ob x =>
x ~> Act (Rep (OpAction t)) Unit x
unitorInv = ((t % '(Unit, UN 'OP x)) ~> UN 'OP x)
-> Op (~>) ('OP (UN 'OP x)) ('OP (t % '(Unit, UN 'OP x)))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op (forall {m} {k} (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
Act t Unit x ~> x
forall (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
Act t Unit x ~> x
unitor @t)
  multiplicator :: forall (a :: OPPOSITE m) (b :: OPPOSITE m) (x :: OPPOSITE k).
(Ob a, Ob b, Ob x) =>
Act (Rep (OpAction t)) (a ** b) x
~> Act (Rep (OpAction t)) a (Act (Rep (OpAction t)) b x)
multiplicator @(OP a) @(OP b) @(OP x) = ((t % '(UN 'OP a, t % '(UN 'OP b, UN 'OP x)))
 ~> (t % '(UN 'OP a ** UN 'OP b, UN 'OP x)))
-> Op
     (~>)
     ('OP (t % '(UN 'OP a ** UN 'OP b, UN 'OP x)))
     ('OP (t % '(UN 'OP a, t % '(UN 'OP b, UN 'OP x))))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op (forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t a (Act t b x) ~> Act t (a ** b) x
forall (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t a (Act t b x) ~> Act t (a ** b) x
multiplicatorInv @t @a @b @x)
  multiplicatorInv :: forall (a :: OPPOSITE m) (b :: OPPOSITE m) (x :: OPPOSITE k).
(Ob a, Ob b, Ob x) =>
Act (Rep (OpAction t)) a (Act (Rep (OpAction t)) b x)
~> Act (Rep (OpAction t)) (a ** b) x
multiplicatorInv @(OP a) @(OP b) @(OP x) = ((t % '(UN 'OP a ** UN 'OP b, UN 'OP x))
 ~> (t % '(UN 'OP a, t % '(UN 'OP b, UN 'OP x))))
-> Op
     (~>)
     ('OP (t % '(UN 'OP a, t % '(UN 'OP b, UN 'OP x))))
     ('OP (t % '(UN 'OP a ** UN 'OP b, UN 'OP x)))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op (forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t (a ** b) x ~> Act t a (Act t b x)
forall (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t (a ** b) x ~> Act t a (Act t b x)
multiplicator @t @a @b @x)

type SubAction ob t = Rep (SubAction' ob t)
data family SubAction' :: forall (ob :: OB m) -> (m, k) +-> k -> (SUBCAT ob, k) +-> k
instance (Monoidal k, Monoidal (SUBCAT (ob :: OB k)), Representable t) => FunctorForRep (SubAction' ob t) where
  type SubAction' ob t @ '(SUB a, x) = t % '(a, x)
  fmap :: forall (a :: (SUBCAT ob, k)) (b :: (SUBCAT ob, k)).
(a ~> b) -> (SubAction' ob t @ a) ~> (SubAction' ob t @ b)
fmap (Sub 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 :: (k, k) +-> k) (a :: (k, k)) (b :: (k, k)).
Representable p =>
(a ~> b) -> (p % a) ~> (p % b)
repMap @t (a1 ~> b1
f (a1 ~> b1) -> (a2 ~> b2) -> (:**:) (~>) (~>) '(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 ~> b2
g)
instance (Monoidal k, Monoidal (SUBCAT (ob :: OB k)), MonoidalAction t) => MonoidalAction (SubAction ob t) where
  unitor :: forall (x :: k). Ob x => Act (SubAction ob t) Unit x ~> x
unitor = forall {m} {k} (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
Act t Unit x ~> x
forall (t :: (k, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
Act t Unit x ~> x
unitor @t
  unitorInv :: forall (x :: k). Ob x => x ~> Act (SubAction ob t) Unit x
unitorInv = forall {m} {k} (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
x ~> Act t Unit x
forall (t :: (k, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
x ~> Act t Unit x
unitorInv @t
  multiplicator :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) (x :: k).
(Ob a, Ob b, Ob x) =>
Act (SubAction ob t) (a ** b) x
~> Act (SubAction ob t) a (Act (SubAction ob t) b x)
multiplicator @(SUB p) @(SUB q) @x = forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t (a ** b) x ~> Act t a (Act t b x)
forall (t :: (k, k) +-> k) (a :: k) (b :: k) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t (a ** b) x ~> Act t a (Act t b x)
multiplicator @t @p @q @x
  multiplicatorInv :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) (x :: k).
(Ob a, Ob b, Ob x) =>
Act (SubAction ob t) a (Act (SubAction ob t) b x)
~> Act (SubAction ob t) (a ** b) x
multiplicatorInv @(SUB p) @(SUB q) @x = forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t a (Act t b x) ~> Act t (a ** b) x
forall (t :: (k, k) +-> k) (a :: k) (b :: k) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t a (Act t b x) ~> Act t (a ** b) x
multiplicatorInv @t @p @q @x

instance (Monoidal k) => MonoidalAction (Tensor :: (k, k) +-> k) where
  unitor :: forall (x :: k). Ob x => Act Tensor Unit x ~> x
unitor = forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @k
  unitorInv :: forall (x :: k). Ob x => x ~> Act Tensor Unit x
unitorInv = forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @k
  multiplicator :: forall (a :: k) (b :: k) (x :: k).
(Ob a, Ob b, Ob x) =>
Act Tensor (a ** b) x ~> Act Tensor a (Act Tensor b x)
multiplicator @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))
associator @k @a @b @x
  multiplicatorInv :: forall (a :: k) (b :: k) (x :: k).
(Ob a, Ob b, Ob x) =>
Act Tensor a (Act Tensor b x) ~> Act Tensor (a ** b) x
multiplicatorInv @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)
associatorInv @k @a @b @x

type ProdAction = Rep ProdAction'
data family ProdAction' :: (PROD k, k) +-> k
instance (HasProducts k) => FunctorForRep (ProdAction' :: (PROD k, k) +-> k) where
  type ProdAction' @ '(PR a, b) = a && b
  fmap :: forall (a :: (PROD k, k)) (b :: (PROD k, k)).
(a ~> b) -> (ProdAction' @ a) ~> (ProdAction' @ b)
fmap (Prod a1 ~> b1
p :**: a2 ~> b2
q) = a1 ~> b1
p (a1 ~> b1) -> (a2 ~> b2) -> (a1 && a2) ~> (b1 && b2)
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).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
*** a2 ~> b2
q
instance (HasProducts k) => MonoidalAction (ProdAction :: (PROD k, k) +-> k) where
  unitor :: forall (x :: k). Ob x => Act ProdAction Unit x ~> x
unitor = (ProdAction % '(Unit, x)) ~> x
(TerminalObject && x) ~> x
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(TerminalObject && a) ~> a
leftUnitorProd
  unitorInv :: forall (x :: k). Ob x => x ~> Act ProdAction Unit x
unitorInv = x ~> (ProdAction % '(Unit, x))
x ~> (TerminalObject && x)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (TerminalObject && a)
leftUnitorProdInv
  multiplicator :: forall (a :: PROD k) (b :: PROD k) (x :: k).
(Ob a, Ob b, Ob x) =>
Act ProdAction (a ** b) x ~> Act ProdAction a (Act ProdAction b x)
multiplicator @(PR a) @(PR b) @x = forall (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
associatorProd @a @b @x
  multiplicatorInv :: forall (a :: PROD k) (b :: PROD k) (x :: k).
(Ob a, Ob b, Ob x) =>
Act ProdAction a (Act ProdAction b x) ~> Act ProdAction (a ** b) x
multiplicatorInv @(PR a) @(PR b) @x = forall (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
associatorProdInv @a @b @x

type CoprodAction = Rep CoprodAction'
data family CoprodAction' :: (COPROD k, k) +-> k
instance (HasCoproducts k) => FunctorForRep (CoprodAction' :: (COPROD k, k) +-> k) where
  type CoprodAction' @ '(COPR a, x) = a || x
  fmap :: forall (a :: (COPROD k, k)) (b :: (COPROD k, k)).
(a ~> b) -> (CoprodAction' @ a) ~> (CoprodAction' @ b)
fmap (Coprod a1 ~> b1
l :**: a2 ~> b2
r) = a1 ~> b1
l (a1 ~> b1) -> (a2 ~> b2) -> (a1 || a2) ~> (b1 || b2)
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)
+++ a2 ~> b2
r
instance (HasCoproducts k) => MonoidalAction (CoprodAction :: (COPROD k, k) +-> k) where
  unitor :: forall (x :: k). Ob x => Act CoprodAction Unit x ~> x
unitor = (CoprodAction % '(Unit, x)) ~> x
(InitialObject || x) ~> x
forall {k} (a :: k).
(HasCoproducts k, Ob a) =>
(InitialObject || a) ~> a
leftUnitorCoprod
  unitorInv :: forall (x :: k). Ob x => x ~> Act CoprodAction Unit x
unitorInv = x ~> (CoprodAction % '(Unit, x))
x ~> (InitialObject || x)
forall {k} (a :: k).
(HasCoproducts k, Ob a) =>
a ~> (InitialObject || a)
leftUnitorCoprodInv
  multiplicator :: forall (a :: COPROD k) (b :: COPROD k) (x :: k).
(Ob a, Ob b, Ob x) =>
Act CoprodAction (a ** b) x
~> Act CoprodAction a (Act CoprodAction b x)
multiplicator @(COPR a) @(COPR b) @x = forall (a :: k) (b :: k) (c :: k).
(HasCoproducts k, Ob a, Ob b, Ob c) =>
((a || b) || c) ~> (a || (b || c))
forall {k} (a :: k) (b :: k) (c :: k).
(HasCoproducts k, Ob a, Ob b, Ob c) =>
((a || b) || c) ~> (a || (b || c))
associatorCoprod @a @b @x
  multiplicatorInv :: forall (a :: COPROD k) (b :: COPROD k) (x :: k).
(Ob a, Ob b, Ob x) =>
Act CoprodAction a (Act CoprodAction b x)
~> Act CoprodAction (a ** b) x
multiplicatorInv @(COPR a) @(COPR b) @x = forall (a :: k) (b :: k) (c :: k).
(HasCoproducts k, Ob a, Ob b, Ob c) =>
(a || (b || c)) ~> ((a || b) || c)
forall {k} (a :: k) (b :: k) (c :: k).
(HasCoproducts k, Ob a, Ob b, Ob c) =>
(a || (b || c)) ~> ((a || b) || c)
associatorCoprodInv @a @b @x

-- newtype Action a x y = Action (Rep (Action' a) x y)
-- deriving newtype instance (Ob (a :: m), MonoidalAction m k) => Profunctor (Action a :: k +-> k)
-- deriving newtype instance (Ob (a :: m), MonoidalAction m k) => Representable (Action a :: k +-> k)

-- data family Action' :: m -> k +-> k
-- instance (MonoidalAction m k, Ob a) => FunctorForRep (Action' (a :: m) :: k +-> k) where
--   type Action' a @ x = Act a x
--   fmap = act @m (obj @a)

-- par0Action :: (MonoidalAction m k, Ob (x :: k)) => Action (Unit :: m) x x
-- par0Action @m @k = Action (Rep (unitorInv @m @k))

-- parAction
--   :: forall {m} {k} a b x y z
--    . (MonoidalAction m k, Ob a, Ob b) => Action (a :: m) (x :: k) y -> Action (b :: m) y z -> Action (a ** b) x z
-- parAction (Action (Rep f)) (Action (Rep g)) = Action (Rep (composeActs @a @b @z f g))