{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Monoidal.Action where

import Data.Kind (Constraint, Type)
import Prelude (type (~))

import Proarrow.Category.Instance.Sub (SUBCAT (..), Sub (..), SubMonoidal)
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Core (CAT, CategoryOf (..), Hom, Kind, OB, Profunctor (..), Promonad (..), UN, obj, type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), trivialCorep)
import Proarrow.Profunctor.Representable (Rep (..), Representable (..), trivialRep)

-- | Profuntorial strength for a monoidal action.
-- Gives functorial strength for representable profunctors,
-- and functorial costrength for corepresentable profunctors.
type Strong :: forall {j} {k}. Kind -> j +-> k -> Constraint
class (MonoidalAction m c, MonoidalAction m d, Profunctor p) => Strong m (p :: c +-> d) where
  act :: forall (a :: m) b x y. a ~> b -> p x y -> p (Act a x) (Act b y)

class (Monoidal m, CategoryOf k, Strong m (Hom k)) => MonoidalAction m k where
  -- I would like to default Act to `**`, but that doesn't seem possible without GHC thinking `m` and `k` are the same.
  type Act (a :: m) (x :: k) :: k
  withObAct :: (Ob (a :: m), Ob (x :: k)) => ((Ob (Act a x)) => r) -> r
  unitor :: (Ob (x :: k)) => Act (Unit :: m) x ~> x
  unitorInv :: (Ob (x :: k)) => x ~> Act (Unit :: m) x
  multiplicator :: (Ob (a :: m), Ob (b :: m), Ob (x :: k)) => Act (a ** b) x ~> Act a (Act b x)
  multiplicatorInv :: (Ob (a :: m), Ob (b :: m), Ob (x :: k)) => Act a (Act b x) ~> Act (a ** b) x

instance (CategoryOf k, Strong () (Hom k)) => MonoidalAction () k where
  type Act '() x = x
  withObAct :: forall (a :: ()) (x :: k) r.
(Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct Ob (Act a x) => r
r = r
Ob (Act a x) => r
r
  unitor :: forall (x :: k). Ob x => Act Unit x ~> x
unitor = x ~> x
Act 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 Unit x
unitorInv = x ~> x
x ~> Act 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 (a ** b) x ~> Act a (Act b x)
multiplicator = x ~> x
Act (a ** b) x ~> Act a (Act 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 a (Act b x) ~> Act (a ** b) x
multiplicatorInv = x ~> x
Act a (Act b x) ~> Act (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

instance (Strong k p) => Strong (OPPOSITE k) (Op p) where
  act :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (x :: OPPOSITE j)
       (y :: OPPOSITE k).
(a ~> b) -> Op p x y -> Op p (Act a x) (Act b y)
act (Op b1 ~> a1
w) (Op p b1 a1
p) = p (Act b1 b1) (Act a1 a1)
-> Op p ('OP (Act a1 a1)) ('OP (Act b1 b1))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op ((b1 ~> a1) -> p b1 a1 -> p (Act b1 b1) (Act a1 a1)
forall (a :: k) (b :: k) (x :: k) (y :: j).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act b1 ~> a1
w p b1 a1
p)
instance (MonoidalAction m k) => MonoidalAction (OPPOSITE m) (OPPOSITE k) where
  type Act (OP a) (OP b) = OP (Act a b)
  withObAct :: forall (a :: OPPOSITE m) (x :: OPPOSITE k) r.
(Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @(OP a) @(OP b) Ob (Act a x) => r
r = forall m k (a :: m) (x :: k) r.
(MonoidalAction m k, Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @m @k @a @b r
Ob (Act (UN 'OP a) (UN 'OP x)) => r
Ob (Act a x) => r
r
  unitor :: forall (x :: OPPOSITE k). Ob x => Act Unit x ~> x
unitor = (UN 'OP x ~> Act Unit (UN 'OP x))
-> Op (Hom k) ('OP (Act 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 (x :: k). (MonoidalAction m k, Ob x) => x ~> Act Unit x
unitorInv @m)
  unitorInv :: forall (x :: OPPOSITE k). Ob x => x ~> Act Unit x
unitorInv = (Act Unit (UN 'OP x) ~> UN 'OP x)
-> Op (Hom k) ('OP (UN 'OP x)) ('OP (Act 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 (x :: k). (MonoidalAction m k, Ob x) => Act Unit x ~> x
unitor @m)
  multiplicator :: forall (a :: OPPOSITE m) (b :: OPPOSITE m) (x :: OPPOSITE k).
(Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicator @(OP a) @(OP b) @(OP x) = (Act (UN 'OP a) (Act (UN 'OP b) (UN 'OP x))
 ~> Act (UN 'OP a ** UN 'OP b) (UN 'OP x))
-> Op
     (Hom k)
     ('OP (Act (UN 'OP a ** UN 'OP b) (UN 'OP x)))
     ('OP (Act (UN 'OP a) (Act (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 (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicatorInv @m @k @a @b @x)
  multiplicatorInv :: forall (a :: OPPOSITE m) (b :: OPPOSITE m) (x :: OPPOSITE k).
(Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicatorInv @(OP a) @(OP b) @(OP x) = (Act (UN 'OP a ** UN 'OP b) (UN 'OP x)
 ~> Act (UN 'OP a) (Act (UN 'OP b) (UN 'OP x)))
-> Op
     (Hom k)
     ('OP (Act (UN 'OP a) (Act (UN 'OP b) (UN 'OP x))))
     ('OP (Act (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 (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicator @m @k @a @b @x)

instance (SubMonoidal ob) => Strong (SUBCAT (ob :: OB Type)) (->) where
  act :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) x y.
(a ~> b) -> (x -> y) -> Act a x -> Act b y
act (Sub a1 -> b1
f) x -> y
g = a1 -> b1
f (a1 -> b1) -> (x -> y) -> (a1 ** x) -> (b1 ** y)
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` x -> y
g
instance (SubMonoidal ob) => Strong (SUBCAT (ob :: OB ())) U.Unit where
  act :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) (x :: ()) (y :: ()).
(a ~> b) -> Unit x y -> Unit (Act a x) (Act b y)
act (Sub Unit a1 b1
f) Unit x y
g = Unit a1 b1
f Unit a1 b1 -> Unit x y -> Unit (a1 ** x) (b1 ** 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 :: ()) (x2 :: ()) (y1 :: ()) (y2 :: ()).
Unit x1 x2 -> Unit y1 y2 -> Unit (x1 ** y1) (x2 ** y2)
`par` Unit x y
g

instance
  (Monoidal k, Monoidal (SUBCAT (ob :: OB k)), Strong (SUBCAT (ob :: OB k)) (Hom k))
  => MonoidalAction (SUBCAT (ob :: OB k)) k
  where
  type Act (p :: SUBCAT ob) (x :: k) = UN SUB p ** x
  withObAct :: forall (a :: SUBCAT ob) (x :: k) r.
(Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @(SUB a) @x Ob (Act a x) => r
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @x r
Ob (UN SUB a ** x) => r
Ob (Act a x) => r
r
  unitor :: forall (x :: k). Ob x => Act 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 Unit x
unitorInv = forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @k
  multiplicator :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) (x :: k).
(Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicator @(SUB p) @(SUB q) @x = forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @p @q @x
  multiplicatorInv :: forall (a :: SUBCAT ob) (b :: SUBCAT ob) (x :: k).
(Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicatorInv @(SUB p) @(SUB q) @x = forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @_ @p @q @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 :: forall (a :: k) (b :: k).
(a ~> b) -> (Action' a @ a) ~> (Action' a @ b)
fmap = forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall m (p :: k +-> k) (a :: m) (b :: m) (x :: k) (y :: k).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act @m (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a)

par0Action :: (MonoidalAction m k, Ob (x :: k)) => Action (Unit :: m) x x
par0Action :: forall m k (x :: k). (MonoidalAction m k, Ob x) => Action Unit x x
par0Action @m @k = Rep (Action' Unit) x x -> Action Unit x x
forall {m} {j} (a :: m) (x :: j) (y :: j).
Rep (Action' a) x y -> Action a x y
Action ((x ~> (Action' Unit @ x)) -> Rep (Action' Unit) x x
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (forall m k (x :: k). (MonoidalAction m k, Ob x) => x ~> Act Unit x
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 :: forall {m} {k} (a :: m) (b :: m) (x :: k) (y :: k) (z :: k).
(MonoidalAction m k, Ob a, Ob b) =>
Action a x y -> Action b y z -> Action (a ** b) x z
parAction (Action (Rep x ~> (Action' a @ y)
f)) (Action (Rep y ~> (Action' b @ z)
g)) = Rep (Action' (a ** b)) x z -> Action (a ** b) x z
forall {m} {j} (a :: m) (x :: j) (y :: j).
Rep (Action' a) x y -> Action a x y
Action ((x ~> (Action' (a ** b) @ z)) -> Rep (Action' (a ** b)) x z
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (forall (x :: m) (y :: m) (c :: k) (a :: k) (b :: k).
(MonoidalAction m k, Ob x, Ob y, Ob c) =>
(a ~> Act x b) -> (b ~> Act y c) -> a ~> Act (x ** y) c
forall {m} {k} (x :: m) (y :: m) (c :: k) (a :: k) (b :: k).
(MonoidalAction m k, Ob x, Ob y, Ob c) =>
(a ~> Act x b) -> (b ~> Act y c) -> a ~> Act (x ** y) c
composeActs @a @b @z x ~> (Action' a @ y)
x ~> Act a y
f y ~> (Action' b @ z)
y ~> Act b z
g))

class (MonoidalAction m k, SymMonoidal m) => SymMonoidalAction m k
instance (MonoidalAction m k, SymMonoidal m) => SymMonoidalAction m k

class (Act a b ~ a ** b) => ActIsTensor a b
instance (Act a b ~ a ** b) => ActIsTensor a b
class (Act a (Act b c) ~ a ** (b ** c), a ** (Act b c) ~ a ** (b ** c), Act a (b ** c) ~ a ** (b ** c)) => ActIsTensor3 a b c
instance (Act a (Act b c) ~ a ** (b ** c), a ** (Act b c) ~ a ** (b ** c), Act a (b ** c) ~ a ** (b ** c)) => ActIsTensor3 a b c
class
  ( SymMonoidalAction k k
  , Strong k ((~>) :: k +-> k)
  , forall (a :: k) (b :: k). ActIsTensor a b
  , forall (a :: k) (b :: k) (c :: k). ActIsTensor3 a b c
  ) =>
  SelfAction k
instance
  ( SymMonoidalAction k k
  , Strong k ((~>) :: k +-> k)
  , forall (a :: k) (b :: k). ActIsTensor a b
  , forall (a :: k) (b :: k) (c :: k). ActIsTensor3 a b c
  )
  => SelfAction k

toSelfAct :: forall {k} (a :: k) b. (SelfAction k, Ob a, Ob b) => a ** b ~> Act a b
toSelfAct :: forall {k} (a :: k) (b :: k).
(SelfAction k, Ob a, Ob b) =>
(a ** b) ~> Act a b
toSelfAct = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (b ~> b) -> Act a b ~> Act a b
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
`act` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b

fromSelfAct :: forall {k} (a :: k) b. (SelfAction k, Ob a, Ob b) => Act a b ~> a ** b
fromSelfAct :: forall {k} (a :: k) (b :: k).
(SelfAction k, Ob a, Ob b) =>
Act a b ~> (a ** b)
fromSelfAct = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (b ~> b) -> Act a b ~> Act a b
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
`act` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b

composeActs
  :: forall {m} {k} (x :: m) y (c :: k) a b
   . (MonoidalAction m k, Ob x, Ob y, Ob c)
  => a ~> Act x b
  -> b ~> Act y c
  -> a ~> Act (x ** y) c
composeActs :: forall {m} {k} (x :: m) (y :: m) (c :: k) (a :: k) (b :: k).
(MonoidalAction m k, Ob x, Ob y, Ob c) =>
(a ~> Act x b) -> (b ~> Act y c) -> a ~> Act (x ** y) c
composeActs a ~> Act x b
f b ~> Act y c
g = 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
multiplicatorInv @m @k @x @y @c (Act x (Act y c) ~> Act (x ** y) c)
-> (a ~> Act x (Act y c)) -> a ~> Act (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
. (x ~> x) -> (b ~> Act y c) -> Act x b ~> Act x (Act y c)
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x) b ~> Act y c
g (Act x b ~> Act x (Act y c))
-> (a ~> Act x b) -> a ~> Act x (Act 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 x b
f

decomposeActs
  :: forall {m} {k} (x :: m) y (c :: k) a b
   . (MonoidalAction m k, Ob x, Ob y, Ob c)
  => Act y c ~> b
  -> Act x b ~> a
  -> Act (x ** y) c ~> a
decomposeActs :: forall {m} {k} (x :: m) (y :: m) (c :: k) (a :: k) (b :: k).
(MonoidalAction m k, Ob x, Ob y, Ob c) =>
(Act y c ~> b) -> (Act x b ~> a) -> Act (x ** y) c ~> a
decomposeActs Act y c ~> b
f Act x b ~> a
g = Act x b ~> a
g (Act x b ~> a)
-> (Act (x ** y) c ~> Act x b) -> Act (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
. (x ~> x) -> (Act y c ~> b) -> Act x (Act y c) ~> Act x b
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x) Act y c ~> b
f (Act x (Act y c) ~> Act x b)
-> (Act (x ** y) c ~> Act x (Act y c)) -> Act (x ** y) c ~> Act 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 (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicator @m @k @x @y @c

first' :: forall {k} {p :: CAT k} c a b. (SelfAction k, Strong k p, Ob c) => p a b -> p (a ** c) (b ** c)
first' :: forall {k} {p :: CAT k} (c :: k) (a :: k) (b :: k).
(SelfAction k, Strong k p, Ob c) =>
p a b -> p (a ** c) (b ** c)
first' 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 :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @a @c) (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @c @b) (forall (c :: k) (a :: k) (b :: k).
(SelfAction k, Strong k p, Ob c) =>
p a b -> p (c ** a) (c ** b)
forall {k} {p :: CAT k} (c :: k) (a :: k) (b :: k).
(SelfAction k, Strong k p, Ob c) =>
p a b -> p (c ** a) (c ** b)
second' @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 :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

second' :: forall {k} {p :: CAT k} c a b. (SelfAction k, Strong k p, Ob c) => p a b -> p (c ** a) (c ** b)
second' :: forall {k} {p :: CAT k} (c :: k) (a :: k) (b :: k).
(SelfAction k, Strong k p, Ob c) =>
p a b -> p (c ** a) (c ** b)
second' p a b
p = (c ~> c) -> p a b -> p (Act c a) (Act c b)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (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

-- | If a strong profunctor is representable, we get the usual strength for the representing functor.
strength :: forall {m} p a b. (Representable p, Strong m p, Ob (a :: m), Ob b) => Act a (p % b) ~> p % Act a b
strength :: forall {k} {k} {m} (p :: k +-> k) (a :: m) (b :: k).
(Representable p, Strong m p, Ob a, Ob b) =>
Act a (p % b) ~> (p % Act a b)
strength = p (Act a (p % b)) (Act a b) -> Act a (p % b) ~> (p % Act a b)
forall (a :: k) (b :: k). 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 ((a ~> a) -> p (p % b) b -> p (Act a (p % b)) (Act a b)
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: k +-> k) (a :: k).
(Representable p, Ob a) =>
p (p % a) a
trivialRep @p @b))

-- | If a strong profunctor is corepresentable, we get the usual costrength for the representing functor.
costrength :: forall {m} p a b. (Corepresentable p, Strong m p, Ob (a :: m), Ob b) => p %% Act a b ~> Act a (p %% b)
costrength :: forall {k} {k} {m} (p :: k +-> k) (a :: m) (b :: k).
(Corepresentable p, Strong m p, Ob a, Ob b) =>
(p %% Act a b) ~> Act a (p %% b)
costrength = p (Act a b) (Act a (p %% b)) -> (p %% Act a b) ~> Act a (p %% b)
forall (a :: k) (b :: k). p a b -> (p %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex ((a ~> a) -> p b (p %% b) -> p (Act a b) (Act a (p %% b))
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) (forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
forall (p :: k +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep @p @b))

-- | This is not monoidal `par` but premonoidal, i.e. no sliding.
-- So with `prepar f g` the effects of f happen before the effects of g.
-- p needs to be a commutative promonad for this to be monoidal `par`.
prepar
  :: forall {k} {p :: CAT k} a b c d. (SelfAction k, Strong k p, Promonad p) => p a b -> p c d -> p (a ** c) (b ** d)
prepar :: forall {k} {p :: CAT k} (a :: k) (b :: k) (c :: k) (d :: k).
(SelfAction k, Strong k p, Promonad p) =>
p a b -> p c d -> p (a ** c) (b ** d)
prepar p a b
f p c d
g = forall (c :: k) (a :: k) (b :: k).
(SelfAction k, Strong k p, Ob c) =>
p a b -> p (c ** a) (c ** b)
forall {k} {p :: CAT k} (c :: k) (a :: k) (b :: k).
(SelfAction k, Strong k p, Ob c) =>
p a b -> p (c ** a) (c ** b)
second' @b p c d
g p (b ** c) (b ** d) -> p (a ** c) (b ** c) -> p (a ** c) (b ** d)
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p 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 (c :: k) (a :: k) (b :: k).
(SelfAction k, Strong k p, Ob c) =>
p a b -> p (a ** c) (b ** c)
forall {k} {p :: CAT k} (c :: k) (a :: k) (b :: k).
(SelfAction k, Strong k p, Ob c) =>
p a b -> p (a ** c) (b ** c)
first' @c p a b
f ((Ob a, Ob b) => p (a ** c) (b ** d))
-> p a b -> p (a ** c) (b ** d)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
f ((Ob c, Ob d) => p (a ** c) (b ** d))
-> p c d -> p (a ** c) (b ** d)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p c d
g

strongPar0 :: forall {k} {p :: CAT k} a. (SelfAction k, Strong k p, MonoidalProfunctor p, Ob a) => p a a
strongPar0 :: forall {k} {p :: CAT k} (a :: k).
(SelfAction k, Strong k p, MonoidalProfunctor p, Ob a) =>
p a a
strongPar0 = (a ~> (a ** Unit))
-> ((a ** Unit) ~> a) -> p (a ** Unit) (a ** Unit) -> p a a
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a ~> (a ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv (a ** Unit) ~> a
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor ((a ~> a) -> p Unit Unit -> p (Act a Unit) (Act a Unit)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0)

type Costrong :: forall {j} {k}. Kind -> j +-> k -> Constraint
class (MonoidalAction m c, MonoidalAction m d, Profunctor p) => Costrong m (p :: c +-> d) where
  coact :: forall (a :: m) (x :: d) (y :: c). (Ob a, Ob x, Ob y) => p (Act a x) (Act a y) -> p x y

trace :: forall {k} (p :: k +-> k) u x y. (SelfAction k, Costrong k p, Ob x, Ob y, Ob u) => p (x ** u) (y ** u) -> p x y
trace :: forall {k} (p :: k +-> k) (u :: k) (x :: k) (y :: k).
(SelfAction k, Costrong k p, Ob x, Ob y, Ob u) =>
p (x ** u) (y ** u) -> p x y
trace p (x ** u) (y ** u)
p = forall {c} {d} m (p :: c +-> d) (a :: m) (x :: d) (y :: c).
(Costrong m p, Ob a, Ob x, Ob y) =>
p (Act a x) (Act a y) -> p x y
forall m (p :: k +-> k) (a :: m) (x :: k) (y :: k).
(Costrong m p, Ob a, Ob x, Ob y) =>
p (Act a x) (Act a y) -> p x y
coact @k @p @u @x @y ((Act u x ~> (x ** u))
-> ((y ** u) ~> Act u y)
-> p (x ** u) (y ** u)
-> p (Act u x) (Act u y)
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @u @x) (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @y @u) p (x ** u) (y ** u)
p) ((Ob (x ** u), Ob (y ** u)) => p x y)
-> p (x ** u) (y ** u) -> p x y
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p (x ** u) (y ** u)
p

class (SelfAction k, Costrong k (Hom k)) => TracedMonoidal k
instance (SelfAction k, Costrong k (Hom k)) => TracedMonoidal k