{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Monoidal.Action where

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

import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Core (CAT, CategoryOf (..), Kind, Profunctor (..), Promonad (..), obj, type (+->))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Representable (Representable (..), trivialRep)
import Proarrow.Profunctor.Corepresentable (Corepresentable(..), trivialCorep)

-- | 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)

actHom :: (MonoidalAction m k) => (a :: m) ~> b -> (x :: k) ~> y -> Act a x ~> Act b y
actHom :: forall m k (a :: m) (b :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
actHom a ~> b
ab x ~> y
xy = Id (Act a x) (Act b y) -> Act a x ~> Act b y
forall k (a :: k) (b :: k). Id a b -> a ~> b
unId ((a ~> b) -> Id x y -> Id (Act a x) (Act b y)
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> Id x y -> Id (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 a ~> b
ab ((x ~> y) -> Id x y
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id x ~> y
xy))

instance (Profunctor p) => Strong () p where
  act :: forall (a :: ()) (b :: ()) (x :: d) (y :: c).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act a ~> b
Unit a b
U.Unit p x y
p = p x y
p (Act a x) (Act b y)
p

instance (Strong m p, Strong m' q) => Strong (m, m') (p :**: q) where
  act :: forall (a :: (m, m')) (b :: (m, m')) (x :: (k1, k2))
       (y :: (j1, j2)).
(a ~> b) -> (:**:) p q x y -> (:**:) p q (Act a x) (Act b y)
act (a1 ~> b1
p :**: a2 ~> b2
q) (p a1 b1
x :**: q a2 b2
y) = (a1 ~> b1) -> p a1 b1 -> p (Act a1 a1) (Act b1 b1)
forall (a :: m) (b :: m) (x :: k1) (y :: j1).
(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 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)
:**: (a2 ~> b2) -> q a2 b2 -> q (Act a2 a2) (Act b2 b2)
forall (a :: m') (b :: m') (x :: k2) (y :: j2).
(a ~> b) -> q x y -> q (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 a2 ~> b2
q q a2 b2
y

class (Monoidal m, CategoryOf k, Strong m (Id :: CAT 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 (Act b x) ~> Act (a ** b) x
  multiplicatorInv :: (Ob (a :: m), Ob (b :: m), Ob (x :: k)) => Act (a ** b) x ~> Act a (Act b x)

instance (CategoryOf 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 (Act b x) ~> Act (a ** b) x
multiplicator = 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
  multiplicatorInv :: forall (a :: ()) (b :: ()) (x :: k).
(Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv = 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

instance (Strong m (Id :: CAT p), Strong n (Id :: CAT q)) => Strong (m, n) (Id :: CAT (p, q)) where
  act :: forall (a :: (m, n)) (b :: (m, n)) (x :: (p, q)) (y :: (p, q)).
(a ~> b) -> Id x y -> Id (Act a x) (Act b y)
act (a1 ~> b1
f :**: a2 ~> b2
f') (Id (a1 ~> b1
g :**: a2 ~> b2
g')) = ('(Act a1 a1, Act a2 a2) ~> '(Act b1 b1, Act b2 b2))
-> Id '(Act a1 a1, Act a2 a2) '(Act b1 b1, Act b2 b2)
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id ((a1 ~> b1) -> (a1 ~> b1) -> Act a1 a1 ~> Act b1 b1
forall m k (a :: m) (b :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
actHom a1 ~> b1
f a1 ~> b1
g (Act a1 a1 ~> Act b1 b1)
-> (Act a2 a2 ~> Act b2 b2)
-> (:**:) (~>) (~>) '(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)
:**: (a2 ~> b2) -> (a2 ~> b2) -> Act a2 a2 ~> Act b2 b2
forall m k (a :: m) (b :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
actHom a2 ~> b2
f' a2 ~> b2
g')

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)
  withObAct :: forall (a :: (n, m)) (x :: (j, k)) r.
(Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @'(p, q) @'(x, y) 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 @n @j @p @x (forall m k (a :: m) (x :: k) r.
(MonoidalAction m k, Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @m @k @q @y r
Ob (Act (Snd a) (Snd x)) => r
Ob (Act a x) => r
r)
  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

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
  , 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
  , 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 = Id (a ** b) (Act a b) -> (a ** b) ~> Act a b
forall k (a :: k) (b :: k). Id a b -> a ~> b
unId (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> Id b b -> Id (Act a b) (Act a b)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> b) -> Id x y -> Id (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` (b ~> b) -> Id b b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (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 = Id (Act a b) (a ** b) -> Act a b ~> (a ** b)
forall k (a :: k) (b :: k). Id a b -> a ~> b
unId (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> Id b b -> Id (Act a b) (Act a b)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> b) -> Id x y -> Id (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` (b ~> b) -> Id b b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (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
multiplicator @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 m k (a :: m) (b :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
actHom (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 m k (a :: m) (b :: m) (x :: k) (y :: k).
MonoidalAction m k =>
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
actHom (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)
multiplicatorInv @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 represented 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 represented 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 ((~>) :: CAT k)) => TracedMonoidal k
instance (SelfAction k, Costrong k ((~>) :: CAT k)) => TracedMonoidal k