{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Monoidal where

import Data.Kind (Constraint)
import Prelude (($))

import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Kind
  , Obj
  , Profunctor (..)
  , Promonad (..)
  , UN
  , obj
  , src
  , tgt
  , type (+->)
  )
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Optic (Iso, iso)
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), trivialCorep)
import Proarrow.Profunctor.Representable (CorepStar, RepCostar, Representable (..), trivialRep)
import Proarrow.Profunctor.Constant (review, view)

infixl 8 ||
infixl 7 ==

-- This is equal to a lax monoidal functor for representable profunctors
-- and to an oplax monoidal functor for corepresentable profunctors.
type MonoidalProfunctor :: forall {j} {k}. j +-> k -> Constraint
class (Monoidal j, Monoidal k, Profunctor p) => MonoidalProfunctor (p :: j +-> k) where
  par0 :: p Unit Unit
  par :: p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)

instance MonoidalProfunctor U.Unit where
  par0 :: Unit Unit Unit
par0 = Unit '() '()
Unit Unit Unit
U.Unit
  Unit x1 x2
U.Unit par :: forall (x1 :: ()) (x2 :: ()) (y1 :: ()) (y2 :: ()).
Unit x1 x2 -> Unit y1 y2 -> Unit (x1 ** y1) (x2 ** y2)
`par` Unit y1 y2
U.Unit = Unit '() '()
Unit (x1 ** y1) (x2 ** y2)
U.Unit

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

par0Rep :: (Representable p, MonoidalProfunctor p) => Unit ~> p % Unit
par0Rep :: forall {j} {k} (p :: j +-> k).
(Representable p, MonoidalProfunctor p) =>
Unit ~> (p % Unit)
par0Rep @p = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index @p p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0

parRep :: (Representable p, MonoidalProfunctor p, Ob x, Ob y) => (p % x) ** (p % y) ~> p % (x ** y)
parRep :: forall {k} {k} (p :: k +-> k) (x :: k) (y :: k).
(Representable p, MonoidalProfunctor p, Ob x, Ob y) =>
((p % x) ** (p % y)) ~> (p % (x ** y))
parRep @p @x @y = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
forall (p :: k +-> k) (a :: k) (b :: k).
Representable p =>
p a b -> a ~> (p % b)
index @p (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 @x p (p % x) x -> p (p % y) y -> p ((p % x) ** (p % y)) (x ** 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)
`par` 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 @y)

unpar0Corep :: (Corepresentable p, MonoidalProfunctor p) => p %% Unit ~> Unit
unpar0Corep :: forall {k} {k} (p :: k +-> k).
(Corepresentable p, MonoidalProfunctor p) =>
(p %% Unit) ~> Unit
unpar0Corep @p = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
forall (p :: k +-> k) (a :: k) (b :: k).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex @p p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0

unparCorep :: (Corepresentable p, MonoidalProfunctor p, Ob x, Ob y) => p %% (x ** y) ~> (p %% x) ** (p %% y)
unparCorep :: forall {j} {k} (p :: j +-> k) (x :: k) (y :: k).
(Corepresentable p, MonoidalProfunctor p, Ob x, Ob y) =>
(p %% (x ** y)) ~> ((p %% x) ** (p %% y))
unparCorep @p @x @y = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
forall (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex @p (forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
forall (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep @p @x p x (p %% x) -> p y (p %% y) -> p (x ** y) ((p %% x) ** (p %% y))
forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
forall (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
trivialCorep @p @y)

type StrongMonoidalRep p = (Representable p, MonoidalProfunctor p, MonoidalProfunctor (RepCostar p))

unpar0Rep :: (StrongMonoidalRep p) => p % Unit ~> Unit
unpar0Rep :: forall {j} {k} (p :: j +-> k).
StrongMonoidalRep p =>
(p % Unit) ~> Unit
unpar0Rep @p = forall {k} {k} (p :: k +-> k).
(Corepresentable p, MonoidalProfunctor p) =>
(p %% Unit) ~> Unit
forall (p :: k +-> j).
(Corepresentable p, MonoidalProfunctor p) =>
(p %% Unit) ~> Unit
unpar0Corep @(RepCostar p)

unparRep :: (StrongMonoidalRep p, Ob x, Ob y) => p % (x ** y) ~> (p % x) ** (p % y)
unparRep :: forall {j} {k} (p :: j +-> k) (x :: j) (y :: j).
(StrongMonoidalRep p, Ob x, Ob y) =>
(p % (x ** y)) ~> ((p % x) ** (p % y))
unparRep @p @x @y = forall {j} {k} (p :: j +-> k) (x :: k) (y :: k).
(Corepresentable p, MonoidalProfunctor p, Ob x, Ob y) =>
(p %% (x ** y)) ~> ((p %% x) ** (p %% y))
forall (p :: k +-> j) (x :: j) (y :: j).
(Corepresentable p, MonoidalProfunctor p, Ob x, Ob y) =>
(p %% (x ** y)) ~> ((p %% x) ** (p %% y))
unparCorep @(RepCostar p) @x @y

type StrongMonoidalCorep p = (Corepresentable p, MonoidalProfunctor p, MonoidalProfunctor (CorepStar p))

par0Corep :: (StrongMonoidalCorep p) => Unit ~> p %% Unit
par0Corep :: forall {k} {k} (p :: k +-> k).
StrongMonoidalCorep p =>
Unit ~> (p %% Unit)
par0Corep @p = forall {j} {k} (p :: j +-> k).
(Representable p, MonoidalProfunctor p) =>
Unit ~> (p % Unit)
forall (p :: k +-> k).
(Representable p, MonoidalProfunctor p) =>
Unit ~> (p % Unit)
par0Rep @(CorepStar p)

parCorep :: (StrongMonoidalCorep p, Ob x, Ob y) => (p %% x) ** (p %% y) ~> p %% (x ** y)
parCorep :: forall {j} {k} (p :: j +-> k) (x :: k) (y :: k).
(StrongMonoidalCorep p, Ob x, Ob y) =>
((p %% x) ** (p %% y)) ~> (p %% (x ** y))
parCorep @p @x @y = forall {k} {k} (p :: k +-> k) (x :: k) (y :: k).
(Representable p, MonoidalProfunctor p, Ob x, Ob y) =>
((p % x) ** (p % y)) ~> (p % (x ** y))
forall (p :: k +-> j) (x :: k) (y :: k).
(Representable p, MonoidalProfunctor p, Ob x, Ob y) =>
((p % x) ** (p % y)) ~> (p % (x ** y))
parRep @(CorepStar p) @x @y

type Monoidal :: Kind -> Constraint
class (CategoryOf k, MonoidalProfunctor ((~>) :: CAT k), Ob (Unit :: k)) => Monoidal k where
  type Unit :: k
  type (a :: k) ** (b :: k) :: k
  withOb2 :: (Ob (a :: k), Ob b) => ((Ob (a ** b)) => r) -> r
  leftUnitor :: (Ob (a :: k)) => Unit ** a ~> a
  leftUnitorInv :: (Ob (a :: k)) => a ~> Unit ** a
  leftUnitorInv = Optic' Profunctor (Unit ** a) a -> a ~> (Unit ** a)
forall {k} (c :: (k -> k -> Type) -> Constraint) (t :: k) (b :: k).
(CategoryOf k, Ob b => c (Corep (Constant b))) =>
Optic' c t b -> b ~> t
review Optic' Profunctor (Unit ** a) a
forall k (a :: k) (a' :: k).
(Monoidal k, Ob a, Ob a') =>
Iso (Unit ** a) (Unit ** a') a a'
leftUnitorIso
  rightUnitor :: (Ob (a :: k)) => a ** Unit ~> a
  rightUnitorInv :: (Ob (a :: k)) => a ~> a ** Unit
  associator :: (Ob (a :: k), Ob b, Ob c) => (a ** b) ** c ~> a ** (b ** c)
  associator @a @b @c = Optic' Profunctor ((a ** b) ** c) (a ** (b ** c))
-> ((a ** b) ** c) ~> (a ** (b ** c))
forall {k} (c :: (k -> k -> Type) -> Constraint) (s :: k) (a :: k).
(CategoryOf k, Ob a => c (Rep (Constant a))) =>
Optic' c s a -> s ~> a
view (forall k (a :: k) (b :: k) (c :: k) (a' :: k) (b' :: k) (c' :: k).
(Monoidal k, Ob a, Ob b, Ob c, Ob a', Ob b', Ob c') =>
Iso
  ((a ** b) ** c)
  ((a' ** b') ** c')
  (a ** (b ** c))
  (a' ** (b' ** c'))
associatorIso @k @a @b @c @a @b @c)
  associatorInv :: (Ob (a :: k), Ob b, Ob c) => a ** (b ** c) ~> (a ** b) ** c
  associatorInv @a @b @c = Optic' Profunctor ((a ** b) ** c) (a ** (b ** c))
-> (a ** (b ** c)) ~> ((a ** b) ** c)
forall {k} (c :: (k -> k -> Type) -> Constraint) (t :: k) (b :: k).
(CategoryOf k, Ob b => c (Corep (Constant b))) =>
Optic' c t b -> b ~> t
review (forall k (a :: k) (b :: k) (c :: k) (a' :: k) (b' :: k) (c' :: k).
(Monoidal k, Ob a, Ob b, Ob c, Ob a', Ob b', Ob c') =>
Iso
  ((a ** b) ** c)
  ((a' ** b') ** c')
  (a ** (b ** c))
  (a' ** (b' ** c'))
associatorIso @k @a @b @c @a @b @c)

leftUnitorIso :: (Monoidal k, Ob (a :: k), Ob (a' :: k)) => Iso (Unit ** a) (Unit ** a') a a'
leftUnitorIso :: forall k (a :: k) (a' :: k).
(Monoidal k, Ob a, Ob a') =>
Iso (Unit ** a) (Unit ** a') a a'
leftUnitorIso = ((Unit ** a) ~> a)
-> (a' ~> (Unit ** a'))
-> Optic_ (OPT a a') (OPT (Unit ** a) (Unit ** a'))
forall {j} {k} (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k) =>
(s ~> a) -> (b ~> t) -> Iso s t a b
iso (Unit ** a) ~> a
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor a' ~> (Unit ** a')
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv

rightUnitorIso :: (Monoidal k, Ob (a :: k), Ob (a' :: k)) => Iso (a ** Unit) (a' ** Unit) a a'
rightUnitorIso :: forall k (a :: k) (a' :: k).
(Monoidal k, Ob a, Ob a') =>
Iso (a ** Unit) (a' ** Unit) a a'
rightUnitorIso = ((a ** Unit) ~> a)
-> (a' ~> (a' ** Unit))
-> Optic_ (OPT a a') (OPT (a ** Unit) (a' ** Unit))
forall {j} {k} (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k) =>
(s ~> a) -> (b ~> t) -> Iso s t a b
iso (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' ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv

associatorIso
  :: (Monoidal k, Ob (a :: k), Ob b, Ob c, Ob (a' :: k), Ob b', Ob c')
  => Iso ((a ** b) ** c) ((a' ** b') ** c') (a ** (b ** c)) (a' ** (b' ** c'))
associatorIso :: forall k (a :: k) (b :: k) (c :: k) (a' :: k) (b' :: k) (c' :: k).
(Monoidal k, Ob a, Ob b, Ob c, Ob a', Ob b', Ob c') =>
Iso
  ((a ** b) ** c)
  ((a' ** b') ** c')
  (a ** (b ** c))
  (a' ** (b' ** c'))
associatorIso @k @a @b @c @a' @b' @c' = (((a ** b) ** c) ~> (a ** (b ** c)))
-> ((a' ** (b' ** c')) ~> ((a' ** b') ** c'))
-> Optic_
     (OPT (a ** (b ** c)) (a' ** (b' ** c')))
     (OPT ((a ** b) ** c) ((a' ** b') ** c'))
forall {j} {k} (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k) =>
(s ~> a) -> (b ~> t) -> Iso s t a b
iso (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 @c) (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' @c')

instance Monoidal () where
  type Unit = '()
  type '() ** '() = '()
  withOb2 :: forall (a :: ()) (b :: ()) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @'() @'() Ob (a ** b) => r
r = r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: ()). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
Unit '() '()
U.Unit
  leftUnitorInv :: forall (a :: ()). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
Unit '() '()
U.Unit
  rightUnitor :: forall (a :: ()). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
Unit '() '()
U.Unit
  rightUnitorInv :: forall (a :: ()). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
Unit '() '()
U.Unit
  associator :: forall (a :: ()) (b :: ()) (c :: ()).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = ((a ** b) ** c) ~> (a ** (b ** c))
Unit '() '()
U.Unit
  associatorInv :: forall (a :: ()) (b :: ()) (c :: ()).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = (a ** (b ** c)) ~> ((a ** b) ** c)
Unit '() '()
U.Unit

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

instance (MonoidalProfunctor p) => MonoidalProfunctor (Op p) where
  par0 :: Op p Unit Unit
par0 = p Unit Unit -> Op p ('OP Unit) ('OP Unit)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0
  Op p b1 a1
l par :: forall (x1 :: OPPOSITE j) (x2 :: OPPOSITE k) (y1 :: OPPOSITE j)
       (y2 :: OPPOSITE k).
Op p x1 x2 -> Op p y1 y2 -> Op p (x1 ** y1) (x2 ** y2)
`par` Op p b1 a1
r = p (b1 ** b1) (a1 ** a1) -> Op p ('OP (a1 ** a1)) ('OP (b1 ** b1))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op (p b1 a1
l p b1 a1 -> p b1 a1 -> p (b1 ** b1) (a1 ** a1)
forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` p b1 a1
r)

-- | The opposite of a monoidal category is also monoidal, with the same tensor product.
instance (Monoidal k) => Monoidal (OPPOSITE k) where
  type Unit = OP Unit
  type a ** b = OP (UN OP a ** UN OP b)
  withOb2 :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @(OP a) @(OP b) Ob (a ** b) => r
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @b r
Ob (UN 'OP a ** UN 'OP b) => r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: OPPOSITE k). Ob a => (Unit ** a) ~> a
leftUnitor = (UN 'OP a ~> (Unit ** UN 'OP a))
-> Op (~>) ('OP (Unit ** UN 'OP a)) ('OP (UN 'OP a))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op UN 'OP a ~> (Unit ** UN 'OP a)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv
  leftUnitorInv :: forall (a :: OPPOSITE k). Ob a => a ~> (Unit ** a)
leftUnitorInv = ((Unit ** UN 'OP a) ~> UN 'OP a)
-> Op (~>) ('OP (UN 'OP a)) ('OP (Unit ** UN 'OP a))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op (Unit ** UN 'OP a) ~> UN 'OP a
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor
  rightUnitor :: forall (a :: OPPOSITE k). Ob a => (a ** Unit) ~> a
rightUnitor = (UN 'OP a ~> (UN 'OP a ** Unit))
-> Op (~>) ('OP (UN 'OP a ** Unit)) ('OP (UN 'OP a))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op UN 'OP a ~> (UN 'OP a ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv
  rightUnitorInv :: forall (a :: OPPOSITE k). Ob a => a ~> (a ** Unit)
rightUnitorInv = ((UN 'OP a ** Unit) ~> UN 'OP a)
-> Op (~>) ('OP (UN 'OP a)) ('OP (UN 'OP a ** Unit))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op (UN 'OP a ** Unit) ~> UN 'OP a
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor
  associator :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (c :: OPPOSITE k).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(OP a) @(OP b) @(OP c) = ((UN 'OP a ** (UN 'OP b ** UN 'OP c))
 ~> ((UN 'OP a ** UN 'OP b) ** UN 'OP c))
-> Op
     (~>)
     ('OP ((UN 'OP a ** UN 'OP b) ** UN 'OP c))
     ('OP (UN 'OP a ** (UN 'OP b ** UN 'OP c)))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op (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 @c)
  associatorInv :: forall (a :: OPPOSITE k) (b :: OPPOSITE k) (c :: OPPOSITE k).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(OP a) @(OP b) @(OP c) = (((UN 'OP a ** UN 'OP b) ** UN 'OP c)
 ~> (UN 'OP a ** (UN 'OP b ** UN 'OP c)))
-> Op
     (~>)
     ('OP (UN 'OP a ** (UN 'OP b ** UN 'OP c)))
     ('OP ((UN 'OP a ** UN 'OP b) ** UN 'OP c))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op (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 @c)

instance (SymMonoidal k) => SymMonoidal (OPPOSITE k) where
  swap :: forall (a :: OPPOSITE k) (b :: OPPOSITE k).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @(OP a) @(OP b) = ((UN 'OP b ** UN 'OP a) ~> (UN 'OP a ** UN 'OP b))
-> Op
     (~>) ('OP (UN 'OP a ** UN 'OP b)) ('OP (UN 'OP b ** UN 'OP a))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @b @a)

(||) :: (Monoidal k) => (a :: k) ~> b -> c ~> d -> a ** c ~> b ** d
|| :: forall k (a :: k) (b :: k) (c :: k) (d :: k).
Monoidal k =>
(a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
(||) = (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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

(==) :: (CategoryOf k) => (a :: k) ~> b -> b ~> c -> a ~> c
a ~> b
f == :: forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== b ~> c
g = b ~> c
g (b ~> c) -> (a ~> b) -> a ~> 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 ~> b
f

obj2 :: forall {k} a b. (Monoidal k, Ob (a :: k), Ob b) => Obj (a ** b)
obj2 :: forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
obj2 = 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) -> (a ** b) ~> (a ** b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b

leftUnitor' :: (Monoidal k) => (a :: k) ~> b -> Unit ** a ~> b
leftUnitor' :: forall k (a :: k) (b :: k).
Monoidal k =>
(a ~> b) -> (Unit ** a) ~> b
leftUnitor' a ~> b
f = a ~> b
f (a ~> b) -> ((Unit ** a) ~> a) -> (Unit ** a) ~> 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
. (Unit ** a) ~> a
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor ((Ob a, Ob b) => (Unit ** a) ~> b) -> (a ~> b) -> (Unit ** a) ~> b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ a ~> b
f

leftUnitorInv' :: (Monoidal k) => (a :: k) ~> b -> a ~> Unit ** b
leftUnitorInv' :: forall k (a :: k) (b :: k).
Monoidal k =>
(a ~> b) -> a ~> (Unit ** b)
leftUnitorInv' a ~> b
f = b ~> (Unit ** b)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv (b ~> (Unit ** b)) -> (a ~> b) -> a ~> (Unit ** 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
. a ~> b
f ((Ob a, Ob b) => a ~> (Unit ** b)) -> (a ~> b) -> a ~> (Unit ** b)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ a ~> b
f

rightUnitor' :: (Monoidal k) => (a :: k) ~> b -> a ** Unit ~> b
rightUnitor' :: forall k (a :: k) (b :: k).
Monoidal k =>
(a ~> b) -> (a ** Unit) ~> b
rightUnitor' a ~> b
f = a ~> b
f (a ~> b) -> ((a ** Unit) ~> a) -> (a ** Unit) ~> 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
. (a ** Unit) ~> a
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor ((Ob a, Ob b) => (a ** Unit) ~> b) -> (a ~> b) -> (a ** Unit) ~> b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ a ~> b
f

rightUnitorInv' :: (Monoidal k) => (a :: k) ~> b -> a ~> b ** Unit
rightUnitorInv' :: forall k (a :: k) (b :: k).
Monoidal k =>
(a ~> b) -> a ~> (b ** Unit)
rightUnitorInv' a ~> b
f = b ~> (b ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv (b ~> (b ** Unit)) -> (a ~> b) -> a ~> (b ** Unit)
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 ~> b
f ((Ob a, Ob b) => a ~> (b ** Unit)) -> (a ~> b) -> a ~> (b ** Unit)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ a ~> b
f

associator' :: forall {k} a b c. (Monoidal k) => Obj (a :: k) -> Obj b -> Obj c -> (a ** b) ** c ~> a ** (b ** c)
associator' :: forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator' Obj a
a Obj b
b Obj c
c = 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 @c ((Ob a, Ob a) => ((a ** b) ** c) ~> (a ** (b ** c)))
-> Obj a -> ((a ** b) ** c) ~> (a ** (b ** c))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ Obj a
a ((Ob b, Ob b) => ((a ** b) ** c) ~> (a ** (b ** c)))
-> Obj b -> ((a ** b) ** c) ~> (a ** (b ** c))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ Obj b
b ((Ob c, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)))
-> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ Obj c
c

associatorInv' :: forall {k} a b c. (Monoidal k) => Obj (a :: k) -> Obj b -> Obj c -> a ** (b ** c) ~> (a ** b) ** c
associatorInv' :: forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv' Obj a
a Obj b
b Obj c
c = 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 @c ((Ob a, Ob a) => (a ** (b ** c)) ~> ((a ** b) ** c))
-> Obj a -> (a ** (b ** c)) ~> ((a ** b) ** c)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ Obj a
a ((Ob b, Ob b) => (a ** (b ** c)) ~> ((a ** b) ** c))
-> Obj b -> (a ** (b ** c)) ~> ((a ** b) ** c)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ Obj b
b ((Ob c, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c))
-> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ Obj c
c

leftUnitorWith :: forall {k} a b. (Monoidal k, Ob (a :: k)) => b ~> Unit -> b ** a ~> a
leftUnitorWith :: forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (b ** a) ~> a
leftUnitorWith b ~> Unit
f = (Unit ** a) ~> a
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor ((Unit ** a) ~> a) -> ((b ** a) ~> (Unit ** a)) -> (b ** a) ~> 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
. (b ~> Unit
f (b ~> Unit) -> (a ~> a) -> (b ** a) ~> (Unit ** a)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a)

leftUnitorInvWith :: forall {k} a b. (Monoidal k, Ob (a :: k)) => Unit ~> b -> a ~> b ** a
leftUnitorInvWith :: forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(Unit ~> b) -> a ~> (b ** a)
leftUnitorInvWith Unit ~> b
f = (Unit ~> b
f (Unit ~> b) -> (a ~> a) -> (Unit ** a) ~> (b ** a)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) ((Unit ** a) ~> (b ** a)) -> (a ~> (Unit ** a)) -> a ~> (b ** 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
. a ~> (Unit ** a)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv

rightUnitorWith :: forall {k} a b. (Monoidal k, Ob (a :: k)) => b ~> Unit -> a ** b ~> a
rightUnitorWith :: forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (a ** b) ~> a
rightUnitorWith b ~> Unit
f = (a ** Unit) ~> a
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor ((a ** Unit) ~> a) -> ((a ** b) ~> (a ** Unit)) -> (a ** b) ~> 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 (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (b ~> Unit) -> (a ** b) ~> (a ** Unit)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` b ~> Unit
f)

rightUnitorInvWith :: forall {k} a b. (Monoidal k, Ob (a :: k)) => Unit ~> b -> a ~> a ** b
rightUnitorInvWith :: forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(Unit ~> b) -> a ~> (a ** b)
rightUnitorInvWith Unit ~> b
f = (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (Unit ~> b) -> (a ** Unit) ~> (a ** b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` Unit ~> b
f) ((a ** Unit) ~> (a ** b)) -> (a ~> (a ** Unit)) -> a ~> (a ** 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
. a ~> (a ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv

unitObj :: (Monoidal k) => Obj (Unit :: k)
unitObj :: forall k. Monoidal k => Obj Unit
unitObj = Unit ~> Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0

first :: forall {k} c a b. (Monoidal k, Ob (c :: k)) => (a ~> b) -> (a ** c) ~> (b ** c)
first :: forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
first a ~> b
f = a ~> b
f (a ~> b) -> (c ~> c) -> (a ** c) ~> (b ** c)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c

second :: forall {k} c a b. (Monoidal k, Ob (c :: k)) => (a ~> b) -> (c ** a) ~> (c ** b)
second :: forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
second a ~> b
f = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c Obj c -> (a ~> b) -> (c ** a) ~> (c ** b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` a ~> b
f

type State a = Unit ~> a
type Costate a = a ~> Unit
type Scalar k = (Unit :: k) ~> Unit

class (Monoidal k) => SymMonoidal k where
  swap :: (Ob (a :: k), Ob b) => (a ** b) ~> (b ** a)

instance SymMonoidal () where
  swap :: forall (a :: ()) (b :: ()). (Ob a, Ob b) => (a ** b) ~> (b ** a)
swap = (a ** b) ~> (b ** a)
Unit '() '()
U.Unit

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

swap' :: forall {k} (a :: k) a' b b'. (SymMonoidal k) => a ~> a' -> b ~> b' -> (a ** b) ~> (b' ** a')
swap' :: forall {k} (a :: k) (a' :: k) (b :: k) (b' :: k).
SymMonoidal k =>
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' a ~> a'
f b ~> b'
g = forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @a' @b' ((a' ** b') ~> (b' ** a'))
-> ((a ** b) ~> (a' ** b')) -> (a ** b) ~> (b' ** 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
. (a ~> a'
f (a ~> a') -> (b ~> b') -> (a ** b) ~> (a' ** b')
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` b ~> b'
g) ((Ob a, Ob a') => (a ** b) ~> (b' ** a'))
-> (a ~> a') -> (a ** b) ~> (b' ** a')
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ a ~> a'
f ((Ob b, Ob b') => (a ** b) ~> (b' ** a'))
-> (b ~> b') -> (a ** b) ~> (b' ** a')
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ b ~> b'
g

swapInner'
  :: (SymMonoidal k)
  => (a :: k) ~> a'
  -> b ~> b'
  -> c ~> c'
  -> d ~> d'
  -> ((a ** b) ** (c ** d)) ~> ((a' ** c') ** (b' ** d'))
swapInner' :: forall k (a :: k) (a' :: k) (b :: k) (b' :: k) (c :: k) (c' :: k)
       (d :: k) (d' :: k).
SymMonoidal k =>
(a ~> a')
-> (b ~> b')
-> (c ~> c')
-> (d ~> d')
-> ((a ** b) ** (c ** d)) ~> ((a' ** c') ** (b' ** d'))
swapInner' a ~> a'
a b ~> b'
b c ~> c'
c d ~> d'
d =
  Obj a'
-> Obj c'
-> Obj (b' ** d')
-> (a' ** (c' ** (b' ** d'))) ~> ((a' ** c') ** (b' ** d'))
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv' ((a ~> a') -> Obj a'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt a ~> a'
a) ((c ~> c') -> Obj c'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt c ~> c'
c) ((b ~> b') -> b' ~> b'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt b ~> b'
b (b' ~> b') -> (d' ~> d') -> Obj (b' ** d')
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` (d ~> d') -> d' ~> d'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt d ~> d'
d)
    ((a' ** (c' ** (b' ** d'))) ~> ((a' ** c') ** (b' ** d')))
-> (((a ** b) ** (c ** d)) ~> (a' ** (c' ** (b' ** d'))))
-> ((a ** b) ** (c ** d)) ~> ((a' ** c') ** (b' ** d'))
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 ~> a'
a (a ~> a')
-> ((b ** (c ** d)) ~> (c' ** (b' ** d')))
-> (a ** (b ** (c ** d))) ~> (a' ** (c' ** (b' ** d')))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` (Obj c'
-> (b' ~> b')
-> (d' ~> d')
-> ((c' ** b') ** d') ~> (c' ** (b' ** d'))
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator' ((c ~> c') -> Obj c'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt c ~> c'
c) ((b ~> b') -> b' ~> b'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt b ~> b'
b) ((d ~> d') -> d' ~> d'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt d ~> d'
d) (((c' ** b') ** d') ~> (c' ** (b' ** d')))
-> ((b ** (c ** d)) ~> ((c' ** b') ** d'))
-> (b ** (c ** d)) ~> (c' ** (b' ** d'))
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
. ((b ~> b') -> (c ~> c') -> (b ** c) ~> (c' ** b')
forall {k} (a :: k) (a' :: k) (b :: k) (b' :: k).
SymMonoidal k =>
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' b ~> b'
b c ~> c'
c ((b ** c) ~> (c' ** b'))
-> (d ~> d') -> ((b ** c) ** d) ~> ((c' ** b') ** d')
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` d ~> d'
d) (((b ** c) ** d) ~> ((c' ** b') ** d'))
-> ((b ** (c ** d)) ~> ((b ** c) ** d))
-> (b ** (c ** d)) ~> ((c' ** b') ** d')
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
. Obj b -> Obj c -> Obj d -> (b ** (c ** d)) ~> ((b ** c) ** d)
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv' ((b ~> b') -> Obj b
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src b ~> b'
b) ((c ~> c') -> Obj c
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src c ~> c'
c) ((d ~> d') -> Obj d
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src d ~> d'
d)))
    ((a ** (b ** (c ** d))) ~> (a' ** (c' ** (b' ** d'))))
-> (((a ** b) ** (c ** d)) ~> (a ** (b ** (c ** d))))
-> ((a ** b) ** (c ** d)) ~> (a' ** (c' ** (b' ** d')))
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
. Obj a
-> Obj b
-> Obj (c ** d)
-> ((a ** b) ** (c ** d)) ~> (a ** (b ** (c ** d)))
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator' ((a ~> a') -> Obj a
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src a ~> a'
a) ((b ~> b') -> Obj b
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src b ~> b'
b) ((c ~> c') -> Obj c
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src c ~> c'
c Obj c -> Obj d -> Obj (c ** d)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` (d ~> d') -> Obj d
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src d ~> d'
d)

swapInner
  :: forall {k} a b c d. (SymMonoidal k, Ob (a :: k), Ob b, Ob c, Ob d) => ((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
swapInner :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
swapInner =
  forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @b @d ((Ob (b ** d) => ((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d)))
 -> ((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d)))
-> (Ob (b ** d) =>
    ((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d)))
-> ((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
forall a b. (a -> b) -> a -> b
$
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @c @d ((Ob (c ** d) => ((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d)))
 -> ((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d)))
-> (Ob (c ** d) =>
    ((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d)))
-> ((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
forall a b. (a -> b) -> a -> b
$
      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 @c @(b ** d)
        ((a ** (c ** (b ** d))) ~> ((a ** c) ** (b ** d)))
-> (((a ** b) ** (c ** d)) ~> (a ** (c ** (b ** d))))
-> ((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
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 (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a
-> ((b ** (c ** d)) ~> (c ** (b ** d)))
-> (a ** (b ** (c ** d))) ~> (a ** (c ** (b ** d)))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @c @b @d (((c ** b) ** d) ~> (c ** (b ** d)))
-> ((b ** (c ** d)) ~> ((c ** b) ** d))
-> (b ** (c ** d)) ~> (c ** (b ** d))
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 k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @b @c ((b ** c) ~> (c ** b))
-> (d ~> d) -> ((b ** c) ** d) ~> ((c ** b) ** d)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @d) (((b ** c) ** d) ~> ((c ** b) ** d))
-> ((b ** (c ** d)) ~> ((b ** c) ** d))
-> (b ** (c ** d)) ~> ((c ** b) ** d)
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 k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @b @c @d))
        ((a ** (b ** (c ** d))) ~> (a ** (c ** (b ** d))))
-> (((a ** b) ** (c ** d)) ~> (a ** (b ** (c ** d))))
-> ((a ** b) ** (c ** d)) ~> (a ** (c ** (b ** d)))
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 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 @(c ** d)

swapFst
  :: forall {k} (a :: k) b c d. (SymMonoidal k, Ob a, Ob b, Ob c, Ob d) => (a ** b) ** (c ** d) ~> (c ** b) ** (a ** d)
swapFst :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((c ** b) ** (a ** d))
swapFst = (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @b @c ((b ** c) ~> (c ** b))
-> ((a ** d) ~> (a ** d))
-> ((b ** c) ** (a ** d)) ~> ((c ** b) ** (a ** d))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` forall (a :: k) (b :: k). (Monoidal k, Ob a, Ob b) => Obj (a ** b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
obj2 @a @d) (((b ** c) ** (a ** d)) ~> ((c ** b) ** (a ** d)))
-> (((a ** b) ** (c ** d)) ~> ((b ** c) ** (a ** d)))
-> ((a ** b) ** (c ** d)) ~> ((c ** b) ** (a ** d))
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 (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
swapInner @b @a @c @d (((b ** a) ** (c ** d)) ~> ((b ** c) ** (a ** d)))
-> (((a ** b) ** (c ** d)) ~> ((b ** a) ** (c ** d)))
-> ((a ** b) ** (c ** d)) ~> ((b ** c) ** (a ** d))
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 k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @a @b ((a ** b) ~> (b ** a))
-> ((c ** d) ~> (c ** d))
-> ((a ** b) ** (c ** d)) ~> ((b ** a) ** (c ** d))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` forall (a :: k) (b :: k). (Monoidal k, Ob a, Ob b) => Obj (a ** b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
obj2 @c @d)

swapSnd
  :: forall {k} a (b :: k) c d. (SymMonoidal k, Ob a, Ob b, Ob c, Ob d) => (a ** b) ** (c ** d) ~> (a ** d) ** (c ** b)
swapSnd :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** d) ** (c ** b))
swapSnd = (forall (a :: k) (b :: k). (Monoidal k, Ob a, Ob b) => Obj (a ** b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
obj2 @a @d Obj (a ** d)
-> ((b ** c) ~> (c ** b))
-> ((a ** d) ** (b ** c)) ~> ((a ** d) ** (c ** b))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @b @c) (((a ** d) ** (b ** c)) ~> ((a ** d) ** (c ** b)))
-> (((a ** b) ** (c ** d)) ~> ((a ** d) ** (b ** c)))
-> ((a ** b) ** (c ** d)) ~> ((a ** d) ** (c ** 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 (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
swapInner @a @b @d @c (((a ** b) ** (d ** c)) ~> ((a ** d) ** (b ** c)))
-> (((a ** b) ** (c ** d)) ~> ((a ** b) ** (d ** c)))
-> ((a ** b) ** (c ** d)) ~> ((a ** d) ** (b ** 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 (a :: k) (b :: k). (Monoidal k, Ob a, Ob b) => Obj (a ** b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
obj2 @a @b Obj (a ** b)
-> ((c ** d) ~> (d ** c))
-> ((a ** b) ** (c ** d)) ~> ((a ** b) ** (d ** c))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @c @d)

swapOuter
  :: forall {k} a b c d. (SymMonoidal k, Ob (a :: k), Ob b, Ob c, Ob d) => ((a ** b) ** (c ** d)) ~> ((d ** b) ** (c ** a))
swapOuter :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((d ** b) ** (c ** a))
swapOuter = (forall (a :: k) (b :: k). (Monoidal k, Ob a, Ob b) => Obj (a ** b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
obj2 @d @b Obj (d ** b)
-> ((a ** c) ~> (c ** a))
-> ((d ** b) ** (a ** c)) ~> ((d ** b) ** (c ** a))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @a @c) (((d ** b) ** (a ** c)) ~> ((d ** b) ** (c ** a)))
-> (((a ** b) ** (c ** d)) ~> ((d ** b) ** (a ** c)))
-> ((a ** b) ** (c ** d)) ~> ((d ** b) ** (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 (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((c ** b) ** (a ** d))
forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((c ** b) ** (a ** d))
swapFst @a @b @d @c (((a ** b) ** (d ** c)) ~> ((d ** b) ** (a ** c)))
-> (((a ** b) ** (c ** d)) ~> ((a ** b) ** (d ** c)))
-> ((a ** b) ** (c ** d)) ~> ((d ** b) ** (a ** 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 (a :: k) (b :: k). (Monoidal k, Ob a, Ob b) => Obj (a ** b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
obj2 @a @b Obj (a ** b)
-> ((c ** d) ~> (d ** c))
-> ((a ** b) ** (c ** d)) ~> ((a ** b) ** (d ** c))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @c @d)

data UnitRep :: () +-> k
instance (Monoidal k) => FunctorForRep (UnitRep :: () +-> k) where
  type UnitRep @ '() = Unit
  fmap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (UnitRep @ a) ~> (UnitRep @ b)
fmap a ~> b
Unit a b
U.Unit = (UnitRep @ a) ~> (UnitRep @ b)
Obj Unit
forall k. Monoidal k => Obj Unit
unitObj
data MultRep :: (k, k) +-> k
instance (Monoidal k) => FunctorForRep (MultRep :: (k, k) +-> k) where
  type MultRep @ '(a, b) = a ** b
  fmap :: forall (a :: (k, k)) (b :: (k, k)).
(a ~> b) -> (MultRep @ a) ~> (MultRep @ b)
fmap (a1 ~> b1
f :**: a2 ~> b2
g) = a1 ~> b1
f (a1 ~> b1) -> (a2 ~> b2) -> (a1 ** a2) ~> (b1 ** b2)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(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` a2 ~> b2
g