{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Profunctor strength for a monoidal action: @'Strong' t p@ lets @p@ absorb the action of @t@
-- via 'act', with 'MonStrong' the self-action (tensor) case; 'Costrong' is the dual, and a
-- 'TracedMonoidal' category is one whose hom-profunctor is costrong for its own tensor.
module Proarrow.Category.Monoidal.Strength where

import Data.Kind (Constraint)

import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..), Tensor)
import Proarrow.Category.Monoidal.Action (Act, CoprodAction, MonoidalAction, ProdAction, actHom)
import Proarrow.Colimit.BinaryCoproduct (COPROD (..), HasBinaryCoproducts (..), swapCoprod)
import Proarrow.Core (CAT, CategoryOf (..), Hom, Kind, Profunctor (..), Promonad (..), obj, ($), type (+->))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), corepUniv)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Coproduct ((:+:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Instance.Product ((:*:) (..))
import Proarrow.Profunctor.Representable (Representable (..), repUniv)
import Proarrow.Tools.Laws (Law (..), Laws (..), ProLaw (..), ProLaws (..), (=:=), (===))

-- | Profunctorial strength for a monoidal action.
-- Gives functorial strength for representable profunctors,
-- and functorial costrength for corepresentable profunctors.
type Strong :: forall {m} {k}. (m, k) +-> k -> k +-> k -> Constraint
class (MonoidalAction t, Profunctor p) => Strong t p where
  act :: (Ob a) => p x y -> p (Act t a x) (Act t a y)

instance (Strong t p, Strong t q) => Strong t (p :*: q) where
  act :: forall (a :: m) (x :: j) (y :: j).
Ob a =>
(:*:) p q x y -> (:*:) p q (Act t a x) (Act t a y)
act @a (p x y
p :*: q x y
q) = forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (m, j) +-> j) (p :: j +-> j) (a :: m) (x :: j)
       (y :: j).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @t @_ @a p x y
p p (t % '(a, x)) (t % '(a, y))
-> q (t % '(a, x)) (t % '(a, y))
-> (:*:) p q (t % '(a, x)) (t % '(a, y))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> q a b -> (:*:) p q a b
:*: forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (m, j) +-> j) (p :: j +-> j) (a :: m) (x :: j)
       (y :: j).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @t @_ @a q x y
q

instance (Strong t p, Strong t q) => Strong t (p :+: q) where
  act :: forall (a :: m) (x :: j) (y :: j).
Ob a =>
(:+:) p q x y -> (:+:) p q (Act t a x) (Act t a y)
act @a (InjL p x y
p) = p (t % '(a, x)) (t % '(a, y))
-> (:+:) p q (t % '(a, x)) (t % '(a, y))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> (:+:) p q a b
InjL (forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (m, j) +-> j) (p :: j +-> j) (a :: m) (x :: j)
       (y :: j).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @t @_ @a p x y
p)
  act @a (InjR q x y
q) = q (t % '(a, x)) (t % '(a, y))
-> (:+:) p q (t % '(a, x)) (t % '(a, y))
forall {j} {k} (q :: j +-> k) (a :: k) (b :: j) (p :: j +-> k).
q a b -> (:+:) p q a b
InjR (forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (m, j) +-> j) (p :: j +-> j) (a :: m) (x :: j)
       (y :: j).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @t @_ @a q x y
q)

instance (MonoidalAction t) => Strong t (Id :: CAT k) where
  act :: forall (a :: m) (x :: k) (y :: k).
Ob a =>
Id x y -> Id (Act t a x) (Act t a y)
act @a (Id x ~> y
g) = ((t % '(a, x)) ~> (t % '(a, y))) -> Id (t % '(a, x)) (t % '(a, y))
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (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 @a) x ~> y
g)

instance (Strong t p, Strong t q) => Strong t (p :.: q) where
  act :: forall (a :: m) (x :: i) (y :: i).
Ob a =>
(:.:) p q x y -> (:.:) p q (Act t a x) (Act t a y)
act @x (p x b
p :.: q b y
q) = forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (m, i) +-> i) (p :: i +-> i) (a :: m) (x :: i)
       (y :: i).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @t @_ @x p x b
p p (t % '(a, x)) (t % '(a, b))
-> q (t % '(a, b)) (t % '(a, y))
-> (:.:) p q (t % '(a, x)) (t % '(a, y))
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (m, i) +-> i) (p :: i +-> i) (a :: m) (x :: i)
       (y :: i).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @t @_ @x q b y
q

instance (CategoryOf j, CategoryOf k) => Strong ProdAction (Prof :: CAT (j +-> k)) where
  act :: forall (a :: PROD (j +-> k)) (x :: j +-> k) (y :: j +-> k).
Ob a =>
Prof x y -> Prof (Act ProdAction a x) (Act ProdAction a y)
act (Prof x :~> y
n) = ((UN PR a :*: x) :~> (UN PR a :*: y))
-> Prof (UN PR a :*: x) (UN PR a :*: y)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(UN PR a a b
p :*: x a b
q) -> UN PR a a b
p UN PR a a b -> y a b -> (:*:) (UN PR a) y a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> q a b -> (:*:) p q a b
:*: x a b -> y a b
x :~> y
n x a b
q

-- | The laws of strength for the tensor acting on its own category: acting by the 'Unit' does
-- nothing and acting by a tensor is acting twice, up to the unitor and the associator, and 'act' is
-- natural in the element and dinatural in the acting object.
instance ProLaws (Strong Tensor) where
  proLaws :: [ProLaw (Strong Tensor)]
proLaws =
    [ String -> ProLawBody (Strong Tensor) -> ProLaw (Strong Tensor)
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"act unit" \ @p @a @b p a b
p forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> p a b
p p a b -> p a b -> m (ProEquation p)
forall {j} {k} (m :: Type -> Type) (p :: j +-> k) (a :: k)
       (b :: j).
Applicative m =>
p a b -> p a b -> m (ProEquation p)
=:= (a ~> (Unit ** a))
-> ((Unit ** b) ~> b) -> p (Unit ** a) (Unit ** b) -> p a b
forall (c :: j) (a :: j) (b :: j) (d :: j).
(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). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @_ @a) (forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @_ @b) (forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (j, j) +-> j) (p :: j +-> j) (a :: j) (x :: j)
       (y :: j).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @Tensor @p @Unit p a b
p)
    , String -> ProLawBody (Strong Tensor) -> ProLaw (Strong Tensor)
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"act tensor" \ @p @a @b @c @d p a b
p forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ ->
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @c @d ((Ob (c ** d) => m (ProEquation p)) -> m (ProEquation p))
-> (Ob (c ** d) => m (ProEquation p)) -> m (ProEquation p)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$
          forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (j, j) +-> j) (p :: j +-> j) (a :: j) (x :: j)
       (y :: j).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @Tensor @p @(c ** d) p a b
p
            p ((c ** d) ** a) ((c ** d) ** b)
-> p ((c ** d) ** a) ((c ** d) ** b) -> m (ProEquation p)
forall {j} {k} (m :: Type -> Type) (p :: j +-> k) (a :: k)
       (b :: j).
Applicative m =>
p a b -> p a b -> m (ProEquation p)
=:= (((c ** d) ** a) ~> (c ** (d ** a)))
-> ((c ** (d ** b)) ~> ((c ** d) ** b))
-> p (c ** (d ** a)) (c ** (d ** b))
-> p ((c ** d) ** a) ((c ** d) ** b)
forall (c :: j) (a :: j) (b :: j) (d :: j).
(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) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @c @d @a) (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @_ @c @d @b) (forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (j, j) +-> j) (p :: j +-> j) (a :: j) (x :: j)
       (y :: j).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @Tensor @p @c (forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (j, j) +-> j) (p :: j +-> j) (a :: j) (x :: j)
       (y :: j).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @Tensor @p @d p a b
p))
    , String -> ProLawBody (Strong Tensor) -> ProLaw (Strong Tensor)
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"act naturality" \ @p @a @b @c @d @e p a b
p forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morK forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morJ -> do
        g <- forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morK @c @a String
"g"
        h <- morJ @b @d "h"
        act @Tensor @p @e (dimap g h p) =:= dimap (obj @e ** g) (obj @e ** h) (act @Tensor @p @e p)
    , String -> ProLawBody (Strong Tensor) -> ProLaw (Strong Tensor)
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"act dinaturality" \ @p @a @b @c @_ @e p a b
p forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morK forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> do
        g <- forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morK @e @c String
"g"
        lmap (g ** obj @a) (act @Tensor @p @c p) =:= rmap (g ** obj @b) (act @Tensor @p @e p)
    ]

type MonStrong (p :: k +-> k) = (Strong Tensor p, SymMonoidal k)

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

-- | If a strong profunctor is corepresentable, we get the usual costrength for the representing functor.
costrength
  :: forall {m} t p a b. (Corepresentable p, Strong t p, Ob (a :: m), Ob b) => p %% Act t a b ~> Act t a (p %% b)
costrength :: forall {j} {m} (t :: (m, j) +-> j) (p :: j +-> j) (a :: m)
       (b :: j).
(Corepresentable p, Strong t p, Ob a, Ob b) =>
(p %% Act t a b) ~> Act t a (p %% b)
costrength = p (t % '(a, b)) (t % '(a, p %% b))
-> (p %% (t % '(a, b))) ~> (t % '(a, p %% b))
forall (a :: j) (b :: j). 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 (forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (m, j) +-> j) (p :: j +-> j) (a :: m) (x :: j)
       (y :: j).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @t @p @a (forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
forall (p :: j +-> j) (a :: j).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv @p @b))

first'
  :: forall {k} {p :: k +-> k} c a b. (MonStrong p, Ob c) => p a b -> p (a ** c) (b ** c)
first' :: forall {k} {p :: k +-> k} (c :: k) (a :: k) (b :: k).
(MonStrong 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).
(MonStrong p, Ob c) =>
p a b -> p (c ** a) (c ** b)
forall {k} {p :: k +-> k} (c :: k) (a :: k) (b :: k).
(MonStrong 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 :: k +-> k} c a b. (MonStrong p, Ob c) => p a b -> p (c ** a) (c ** b)
second' :: forall {k} {p :: k +-> k} (c :: k) (a :: k) (b :: k).
(MonStrong p, Ob c) =>
p a b -> p (c ** a) (c ** b)
second' p a b
p = forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (k, k) +-> k) (p :: k +-> k) (a :: k) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @Tensor @p @c p a b
p

left'
  :: forall {k} (p :: k +-> k) c a b. (Strong CoprodAction p, HasBinaryCoproducts k, Ob c) => p a b -> p (a || c) (b || c)
left' :: forall {k} (p :: k +-> k) (c :: k) (a :: k) (b :: k).
(Strong CoprodAction p, HasBinaryCoproducts k, 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 :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (forall (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(a || b) ~> (b || a)
forall {k} (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(a || b) ~> (b || a)
swapCoprod @a @c) (forall (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(a || b) ~> (b || a)
forall {k} (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(a || b) ~> (b || a)
swapCoprod @c @b) (forall {k} (p :: k +-> k) (c :: k) (a :: k) (b :: k).
(Strong CoprodAction p, Ob c) =>
p a b -> p (c || a) (c || b)
forall (p :: k +-> k) (c :: k) (a :: k) (b :: k).
(Strong CoprodAction 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 :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

right' :: forall {k} (p :: k +-> k) c a b. (Strong CoprodAction p, Ob c) => p a b -> p (c || a) (c || b)
right' :: forall {k} (p :: k +-> k) (c :: k) (a :: k) (b :: k).
(Strong CoprodAction p, Ob c) =>
p a b -> p (c || a) (c || b)
right' p a b
p = forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (COPROD k, k) +-> k) (p :: k +-> k) (a :: COPROD k)
       (x :: k) (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @CoprodAction @p @(COPR c) p a b
p

-- | This is not monoidal ** but premonoidal, i.e. no sliding.
-- So with `premon f g` the effects of f happen before the effects of g.
-- p needs to be a commutative promonad for this to be monoidal **.
premon
  :: forall {k} {p :: CAT k} a b c d. (MonStrong p, Promonad p) => p a b -> p c d -> p (a ** c) (b ** d)
premon :: forall {k} {p :: CAT k} (a :: k) (b :: k) (c :: k) (d :: k).
(MonStrong p, Promonad p) =>
p a b -> p c d -> p (a ** c) (b ** d)
premon p a b
f p c d
g = forall (c :: k) (a :: k) (b :: k).
(MonStrong p, Ob c) =>
p a b -> p (c ** a) (c ** b)
forall {k} {p :: k +-> k} (c :: k) (a :: k) (b :: k).
(MonStrong 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 :: CAT 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).
(MonStrong p, Ob c) =>
p a b -> p (a ** c) (b ** c)
forall {k} {p :: k +-> k} (c :: k) (a :: k) (b :: k).
(MonStrong 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

strongId :: forall {k} {p :: k +-> k} a. (MonStrong p, MonoidalProfunctor p, Ob a) => p a a
strongId :: forall {k} {p :: k +-> k} (a :: k).
(MonStrong p, MonoidalProfunctor p, Ob a) =>
p a a
strongId = (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 (forall (c :: k) (a :: k) (b :: k).
(MonStrong p, Ob c) =>
p a b -> p (c ** a) (c ** b)
forall {k} {p :: k +-> k} (c :: k) (a :: k) (b :: k).
(MonStrong p, Ob c) =>
p a b -> p (c ** a) (c ** b)
second' @a p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one)

-- | A monoidal promonad is automatically strong.
monActDefault :: forall {p} a x y. (MonoidalProfunctor p, Promonad p, Ob a) => p x y -> p (a ** x) (a ** y)
monActDefault :: forall {k} {p :: k +-> k} (a :: k) (x :: k) (y :: k).
(MonoidalProfunctor p, Promonad p, Ob a) =>
p x y -> p (a ** x) (a ** y)
monActDefault p x y
p = forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id @p @a p a a -> p x y -> p (a ** x) (a ** y)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
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)
** p x y
p

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

instance Costrong Tensor (->) where
  coact :: forall a x y.
(Ob a, Ob x, Ob y) =>
(Act Tensor a x -> Act Tensor a y) -> x -> y
coact Act Tensor a x -> Act Tensor a y
f x
x = let (a
u, y
y) = Act Tensor a x -> Act Tensor a y
f (a
u, x
x) in y
y

instance (MonoidalAction t, Costrong t (Hom k)) => Costrong t (Id :: CAT k) where
  coact :: forall (a :: m) (x :: k) (y :: k).
(Ob a, Ob x, Ob y) =>
Id (Act t a x) (Act t a y) -> Id x y
coact @a (Id Act t a x ~> Act t a y
g) = (x ~> y) -> Id x y
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
forall (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
coact @t @(Hom k) @a Act t a x ~> Act t a y
g)

-- | The laws of costrength for the tensor acting on its own category: 'coact' is natural in the
-- element and dinatural in the acting object (sliding), and coacting by the 'Unit' or by a tensor
-- is doing nothing or coacting twice (vanishing). An element with tensored endpoints is made from
-- the drawn element @p@ with arbitrary arrows into and out of it.
instance ProLaws (Costrong Tensor) where
  proLaws :: [ProLaw (Costrong Tensor)]
proLaws =
    [ String -> ProLawBody (Costrong Tensor) -> ProLaw (Costrong Tensor)
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"coact unit" \ @p @a @b p a b
p forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ ->
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @Unit @a ((Ob (Unit ** a) => m (ProEquation p)) -> m (ProEquation p))
-> (Ob (Unit ** a) => m (ProEquation p)) -> m (ProEquation p)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$
          forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @Unit @b ((Ob (Unit ** b) => m (ProEquation p)) -> m (ProEquation p))
-> (Ob (Unit ** b) => m (ProEquation p)) -> m (ProEquation p)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$
            p a b
p p a b -> p a b -> m (ProEquation p)
forall {j} {k} (m :: Type -> Type) (p :: j +-> k) (a :: k)
       (b :: j).
Applicative m =>
p a b -> p a b -> m (ProEquation p)
=:= forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
forall (t :: (j, j) +-> j) (p :: j +-> j) (a :: j) (x :: j)
       (y :: j).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
coact @Tensor @p @Unit (((Unit ** a) ~> a)
-> (b ~> (Unit ** b)) -> p a b -> p (Unit ** a) (Unit ** b)
forall (c :: j) (a :: j) (b :: j) (d :: j).
(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). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @_ @a) (forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @_ @b) p a b
p)
    , String -> ProLawBody (Costrong Tensor) -> ProLaw (Costrong Tensor)
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"coact tensor" \ @p @a @b @c @d @e @f p a b
p forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morK forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ ->
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @c @e ((Ob (c ** e) => m (ProEquation p)) -> m (ProEquation p))
-> (Ob (c ** e) => m (ProEquation p)) -> m (ProEquation p)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$
          forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(c ** e) @d ((Ob ((c ** e) ** d) => m (ProEquation p)) -> m (ProEquation p))
-> (Ob ((c ** e) ** d) => m (ProEquation p)) -> m (ProEquation p)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$
            forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(c ** e) @f ((Ob ((c ** e) ** f) => m (ProEquation p)) -> m (ProEquation p))
-> (Ob ((c ** e) ** f) => m (ProEquation p)) -> m (ProEquation p)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$
              forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @e @d ((Ob (e ** d) => m (ProEquation p)) -> m (ProEquation p))
-> (Ob (e ** d) => m (ProEquation p)) -> m (ProEquation p)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$
                forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @e @f ((Ob (e ** f) => m (ProEquation p)) -> m (ProEquation p))
-> (Ob (e ** f) => m (ProEquation p)) -> m (ProEquation p)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$
                  forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @c @(e ** d) ((Ob (c ** (e ** d)) => m (ProEquation p)) -> m (ProEquation p))
-> (Ob (c ** (e ** d)) => m (ProEquation p)) -> m (ProEquation p)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @c @(e ** f) do
                    g <- forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morK @((c ** e) ** d) @a String
"g"
                    h <- morK @b @((c ** e) ** f) "h"
                    let q = (((c ** e) ** d) ~> a)
-> (b ~> ((c ** e) ** f))
-> p a b
-> p ((c ** e) ** d) ((c ** e) ** f)
forall (c :: j) (a :: j) (b :: j) (d :: j).
(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 ((c ** e) ** d) ~> a
g b ~> ((c ** e) ** f)
h p a b
p
                    coact @Tensor @p @(c ** e) q
                      =:= coact @Tensor @p @e @d @f (coact @Tensor @p @c (dimap (associatorInv @_ @c @e @d) (associator @_ @c @e @f) q))
    , String -> ProLawBody (Costrong Tensor) -> ProLaw (Costrong Tensor)
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"coact naturality" \ @p @a @b @c @d @e @f p a b
p forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morK forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ ->
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @c @d ((Ob (c ** d) => m (ProEquation p)) -> m (ProEquation p))
-> (Ob (c ** d) => m (ProEquation p)) -> m (ProEquation p)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @c @f ((Ob (c ** f) => m (ProEquation p)) -> m (ProEquation p))
-> (Ob (c ** f) => m (ProEquation p)) -> m (ProEquation p)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @c @e do
          g <- forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morK @(c ** d) @a String
"g"
          h <- morK @b @(c ** f) "h"
          g' <- morK @e @d "g'"
          h' <- morK @f @e "h'"
          let q = ((c ** d) ~> a) -> (b ~> (c ** f)) -> p a b -> p (c ** d) (c ** f)
forall (c :: j) (a :: j) (b :: j) (d :: j).
(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 (c ** d) ~> a
g b ~> (c ** f)
h p a b
p
          coact @Tensor @p @c (dimap (obj @c ** g') (obj @c ** h') q) =:= dimap g' h' (coact @Tensor @p @c q)
    , String -> ProLawBody (Costrong Tensor) -> ProLaw (Costrong Tensor)
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"coact sliding" \ @p @a @b @c @d @e @f p a b
p forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morK forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ ->
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @c @d ((Ob (c ** d) => m (ProEquation p)) -> m (ProEquation p))
-> (Ob (c ** d) => m (ProEquation p)) -> m (ProEquation p)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @c @f ((Ob (c ** f) => m (ProEquation p)) -> m (ProEquation p))
-> (Ob (c ** f) => m (ProEquation p)) -> m (ProEquation p)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @e @d ((Ob (e ** d) => m (ProEquation p)) -> m (ProEquation p))
-> (Ob (e ** d) => m (ProEquation p)) -> m (ProEquation p)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @e @f do
          g <- forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morK @(c ** d) @a String
"g"
          h <- morK @b @(e ** f) "h"
          k <- morK @e @c "k"
          let q = ((c ** d) ~> a) -> (b ~> (e ** f)) -> p a b -> p (c ** d) (e ** f)
forall (c :: j) (a :: j) (b :: j) (d :: j).
(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 (c ** d) ~> a
g b ~> (e ** f)
h p a b
p
          coact @Tensor @p @e @d @f (lmap (k ** obj @d) q) =:= coact @Tensor @p @c @d @f (rmap (k ** obj @f) q)
    ]

trace
  :: forall {k} (p :: k +-> k) u x y
   . (Costrong Tensor p, Ob x, Ob y, Ob u, SymMonoidal k) => p (x ** u) (y ** u) -> p x y
trace :: forall {k} (p :: k +-> k) (u :: k) (x :: k) (y :: k).
(Costrong Tensor p, Ob x, Ob y, Ob u, SymMonoidal k) =>
p (x ** u) (y ** u) -> p x y
trace p (x ** u) (y ** u)
p = forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
forall (t :: (k, k) +-> k) (p :: k +-> k) (a :: k) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
coact @Tensor @p @u @x @y (((u ** x) ~> (x ** u))
-> ((y ** u) ~> (u ** y))
-> p (x ** u) (y ** u)
-> p (u ** x) (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 (Costrong Tensor (Hom k), SymMonoidal k) => TracedMonoidal k
instance (Costrong Tensor (Hom k), SymMonoidal k) => TracedMonoidal k

-- | The structures the laws of a traced monoidal category are stated for.
type TracedStructures :: [Kind -> Constraint]
type TracedStructures = '[Monoidal, SymMonoidal, TracedMonoidal]

-- | The trace laws, for 'trace' over @u@ of @f : x ** u ~> y ** u@: natural in @x@ and @y@,
-- dinatural in @u@ (sliding), trivial over the unit and iterated over a tensor (vanishing),
-- compatible with tensoring on the left (superposing), and the trace of a swap is the identity
-- (yanking).
instance Laws TracedStructures where
  laws :: [Law TracedStructures]
laws =
    [ String -> LawBody TracedStructures -> Law TracedStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"naturality" \ @x @y @u @d @e forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @x @u ((Ob (a ** c) => m (Equation k)) -> m (Equation k))
-> (Ob (a ** c) => m (Equation k)) -> m (Equation k)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @y @u ((Ob (b ** c) => m (Equation k)) -> m (Equation k))
-> (Ob (b ** c) => m (Equation k)) -> m (Equation k)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @e @u ((Ob (e ** c) => m (Equation k)) -> m (Equation k))
-> (Ob (e ** c) => m (Equation k)) -> m (Equation k)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @d @u do
        f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @(x ** u) @(y ** u) String
"f"
        g <- mor @y @d "g"
        h <- mor @e @x "h"
        g . trace @(~>) @u @x @y f . h === trace @(~>) @u @e @d ((g ** obj @u) . f . (h ** obj @u))
    , String -> LawBody TracedStructures -> Law TracedStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"sliding" \ @x @y @u @v forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @x @u ((Ob (a ** c) => m (Equation k)) -> m (Equation k))
-> (Ob (a ** c) => m (Equation k)) -> m (Equation k)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @y @u ((Ob (b ** c) => m (Equation k)) -> m (Equation k))
-> (Ob (b ** c) => m (Equation k)) -> m (Equation k)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @x @v ((Ob (a ** d) => m (Equation k)) -> m (Equation k))
-> (Ob (a ** d) => m (Equation k)) -> m (Equation k)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @y @v do
        f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @(x ** v) @(y ** u) String
"f"
        g <- mor @u @v "g"
        trace @(~>) @u @x @y (f . (obj @x ** g)) === trace @(~>) @v @x @y ((obj @y ** g) . f)
    , String -> LawBody TracedStructures -> Law TracedStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"vanishing (unit)" \ @x @y forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @x @Unit ((Ob (a ** Unit) => m (Equation k)) -> m (Equation k))
-> (Ob (a ** Unit) => m (Equation k)) -> m (Equation k)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @y @Unit do
        f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @(x ** Unit) @(y ** Unit) String
"f"
        trace @(~>) @Unit @x @y f === rightUnitor @_ @y . f . rightUnitorInv @_ @x
    , String -> LawBody TracedStructures -> Law TracedStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"vanishing (tensor)" \ @x @y @u @v forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor ->
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @u @v ((Ob (c ** d) => m (Equation k)) -> m (Equation k))
-> (Ob (c ** d) => m (Equation k)) -> m (Equation k)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$
          forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @x @(u ** v) ((Ob (a ** (c ** d)) => m (Equation k)) -> m (Equation k))
-> (Ob (a ** (c ** d)) => m (Equation k)) -> m (Equation k)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$
            forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @y @(u ** v) ((Ob (b ** (c ** d)) => m (Equation k)) -> m (Equation k))
-> (Ob (b ** (c ** d)) => m (Equation k)) -> m (Equation k)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$
              forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @x @u ((Ob (a ** c) => m (Equation k)) -> m (Equation k))
-> (Ob (a ** c) => m (Equation k)) -> m (Equation k)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$
                forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @y @u ((Ob (b ** c) => m (Equation k)) -> m (Equation k))
-> (Ob (b ** c) => m (Equation k)) -> m (Equation k)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$
                  forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(x ** u) @v ((Ob ((a ** c) ** d) => m (Equation k)) -> m (Equation k))
-> (Ob ((a ** c) ** d) => m (Equation k)) -> m (Equation k)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$
                    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(y ** u) @v do
                      f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @(x ** (u ** v)) @(y ** (u ** v)) String
"f"
                      trace @(~>) @(u ** v) @x @y f
                        === trace @(~>) @u @x @y (trace @(~>) @v @(x ** u) @(y ** u) (associatorInv @_ @y @u @v . f . associator @_ @x @u @v))
    , String -> LawBody TracedStructures -> Law TracedStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"superposing" \ @x @y @u @w forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor ->
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @x @u ((Ob (a ** c) => m (Equation k)) -> m (Equation k))
-> (Ob (a ** c) => m (Equation k)) -> m (Equation k)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$
          forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @y @u ((Ob (b ** c) => m (Equation k)) -> m (Equation k))
-> (Ob (b ** c) => m (Equation k)) -> m (Equation k)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$
            forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @w @x ((Ob (d ** a) => m (Equation k)) -> m (Equation k))
-> (Ob (d ** a) => m (Equation k)) -> m (Equation k)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$
              forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @w @y ((Ob (d ** b) => m (Equation k)) -> m (Equation k))
-> (Ob (d ** b) => m (Equation k)) -> m (Equation k)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$
                forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @w @(x ** u) ((Ob (d ** (a ** c)) => m (Equation k)) -> m (Equation k))
-> (Ob (d ** (a ** c)) => m (Equation k)) -> m (Equation k)
forall (c :: Constraint) r. ((c => r) -> r) -> (c => r) -> r
$
                  forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @w @(y ** u) do
                    f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @(x ** u) @(y ** u) String
"f"
                    obj @w
                      ** trace @(~>) @u @x @y f
                      === trace @(~>) @u @(w ** x) @(w ** y) (associatorInv @_ @w @y @u . (obj @w ** f) . associator @_ @w @x @u)
    , String -> LawBody TracedStructures -> Law TracedStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"yanking" \ @u forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @u @u (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @u Obj a -> Obj a -> m (Equation k)
forall {i} (m :: Type -> Type) r (a :: i) (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== forall {k} (p :: k +-> k) (u :: k) (x :: k) (y :: k).
(Costrong Tensor p, Ob x, Ob y, Ob u, SymMonoidal k) =>
p (x ** u) (y ** u) -> p x y
forall (p :: k +-> k) (u :: k) (x :: k) (y :: k).
(Costrong Tensor p, Ob x, Ob y, Ob u, SymMonoidal k) =>
p (x ** u) (y ** u) -> p x y
trace @(~>) @u @u @u (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @u @u))
    ]