{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Monoidal where

import Data.Kind (Constraint)
import Prelude (Eq, Show, ($))

import Proarrow.Category.Instance.Free
  ( Elem
  , FREE (..)
  , Free (..)
  , HasStructure (..)
  , IsFreeOb (..)
  , Ok
  , WithEq
  , WithShow
  )
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Core (CAT, CategoryOf (..), Kind, Obj, Profunctor (..), Promonad (..), obj, src, tgt, type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), trivialCorep)
import Proarrow.Profunctor.Representable (CorepStar, RepCostar, Representable (..), trivialRep)

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
  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)
  associatorInv :: (Ob (a :: k), Ob b, Ob c) => a ** (b ** c) ~> (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

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

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 family UnitF :: k
instance (Monoidal `Elem` cs) => IsFreeOb (UnitF :: FREE cs p) where
  type Lower f UnitF = Unit
  withLowerOb :: forall {k} (f :: j +-> k) r.
(Representable f, All cs k) =>
(Ob (Lower f UnitF) => r) -> r
withLowerOb Ob (Lower f UnitF) => r
r = r
Ob (Lower f UnitF) => r
r
data family (**!) (a :: k) (b :: k) :: k
instance (Ob (a :: FREE cs p), Ob b, Monoidal `Elem` cs) => IsFreeOb (a **! b) where
  type Lower f (a **! b) = Lower f a ** Lower f b
  withLowerOb :: forall {k} (f :: j +-> k) r.
(Representable f, All cs k) =>
(Ob (Lower f (a **! b)) => r) -> r
withLowerOb @f Ob (Lower f (a **! b)) => r
r = forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @a @f (forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @b @f (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(Lower f a) @(Lower f b) r
Ob (Lower f (a **! b)) => r
Ob (Lower f a ** Lower f b) => r
r))
instance (Monoidal `Elem` cs) => HasStructure cs p Monoidal where
  data Struct Monoidal i o where
    Par0 :: Struct Monoidal UnitF UnitF
    Par :: a ~> b -> c ~> d -> Struct Monoidal (a **! c) (b **! d)
    LeftUnitor :: (Ob a) => Struct Monoidal (UnitF **! a) a
    LeftUnitorInv :: (Ob a) => Struct Monoidal a (UnitF **! a)
    RightUnitor :: (Ob a) => Struct Monoidal (a **! UnitF) a
    RightUnitorInv :: (Ob a) => Struct Monoidal a (a **! UnitF)
    Associator :: (Ob a, Ob b, Ob c) => Struct Monoidal ((a **! b) **! c) (a **! (b **! c))
    AssociatorInv :: (Ob a, Ob b, Ob c) => Struct Monoidal (a **! (b **! c)) ((a **! b) **! c)
  foldStructure :: forall {k} (f :: j +-> k) (a :: FREE cs p) (b :: FREE cs p).
(All cs k, Representable f) =>
(forall (x :: FREE cs p) (y :: FREE cs p).
 (x ~> y) -> Lower f x ~> Lower f y)
-> Struct Monoidal a b -> Lower f a ~> Lower f b
foldStructure forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ Struct Monoidal a b
R:StructjcspMonoidalio j cs p a b
Par0 = Lower f a ~> Lower f b
Unit ~> Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0
  foldStructure forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go (Par a ~> b
f c ~> d
g) = (a ~> b) -> Lower f a ~> Lower f b
forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go a ~> b
f (Lower f a ~> Lower f b)
-> (Lower f c ~> Lower f d)
-> (Lower f a ** Lower f c) ~> (Lower f b ** Lower f 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` (c ~> d) -> Lower f c ~> Lower f d
forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go c ~> d
g
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (LeftUnitor @a) = forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @a @f (Unit ** Lower f b) ~> Lower f b
Ob (Lower f b) => (Unit ** Lower f b) ~> Lower f b
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (LeftUnitorInv @a) = forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @a @f Lower f a ~> (Unit ** Lower f a)
Ob (Lower f a) => Lower f a ~> (Unit ** Lower f a)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (RightUnitor @a) = forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @a @f (Lower f b ** Unit) ~> Lower f b
Ob (Lower f b) => (Lower f b ** Unit) ~> Lower f b
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (RightUnitorInv @a) = forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @a @f Lower f a ~> (Lower f a ** Unit)
Ob (Lower f a) => Lower f a ~> (Lower f a ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (Associator @a @b @c') = forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @a @f (forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @b @f (forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @c' @f (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @(Lower f a) @(Lower f b) @(Lower f c'))))
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (AssociatorInv @a @b @c') = forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @a @f (forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @b @f (forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @c' @f (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @_ @(Lower f a) @(Lower f b) @(Lower f c'))))
deriving instance (WithEq a) => Eq (Struct Monoidal a b)
deriving instance (WithShow a) => Show (Struct Monoidal a b)
instance (Ok cs p, Monoidal `Elem` cs) => MonoidalProfunctor (Free :: CAT (FREE cs p)) where
  par0 :: Free Unit Unit
par0 = Struct Monoidal UnitF UnitF -> Free UnitF UnitF -> Free UnitF UnitF
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
Str Struct Monoidal UnitF UnitF
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}.
Struct Monoidal UnitF UnitF
Par0 Free UnitF UnitF
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id
  Free x1 x2
f par :: forall (x1 :: FREE cs p) (x2 :: FREE cs p) (y1 :: FREE cs p)
       (y2 :: FREE cs p).
Free x1 x2 -> Free y1 y2 -> Free (x1 ** y1) (x2 ** y2)
`par` Free y1 y2
g = Struct Monoidal (x1 **! y1) (x2 **! y2)
-> Free (x1 **! y1) (x1 **! y1) -> Free (x1 **! y1) (x2 **! y2)
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
Str ((x1 ~> x2) -> (y1 ~> y2) -> Struct Monoidal (x1 **! y1) (x2 **! y2)
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p)
       (d :: FREE cs p).
(a ~> b) -> (c ~> d) -> Struct Monoidal (a **! c) (b **! d)
Par x1 ~> x2
Free x1 x2
f y1 ~> y2
Free y1 y2
g) Free (x1 **! y1) (x1 **! y1)
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id ((Ob x1, Ob x2) => Free (x1 **! y1) (x2 **! y2))
-> Free x1 x2 -> Free (x1 **! y1) (x2 **! y2)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FREE cs p) (b :: FREE cs p) r.
((Ob a, Ob b) => r) -> Free a b -> r
\\ Free x1 x2
f ((Ob y1, Ob y2) => Free (x1 **! y1) (x2 **! y2))
-> Free y1 y2 -> Free (x1 **! y1) (x2 **! y2)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FREE cs p) (b :: FREE cs p) r.
((Ob a, Ob b) => r) -> Free a b -> r
\\ Free y1 y2
g
instance (Ok cs p, Monoidal `Elem` cs) => Monoidal (FREE cs p) where
  type Unit = UnitF
  type a ** b = a **! b
  withOb2 :: forall (a :: FREE cs p) (b :: FREE cs p) 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 :: FREE cs p). Ob a => (Unit ** a) ~> a
leftUnitor = Struct Monoidal (UnitF **! a) a
-> Free (UnitF **! a) (UnitF **! a) -> Free (UnitF **! a) a
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
Str Struct Monoidal (UnitF **! a) a
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Struct Monoidal (UnitF **! a) a
LeftUnitor Free (UnitF **! a) (UnitF **! a)
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id
  leftUnitorInv :: forall (a :: FREE cs p). Ob a => a ~> (Unit ** a)
leftUnitorInv = Struct Monoidal a (UnitF **! a) -> Free a a -> Free a (UnitF **! a)
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
Str Struct Monoidal a (UnitF **! a)
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Struct Monoidal a (UnitF **! a)
LeftUnitorInv Free a a
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id
  rightUnitor :: forall (a :: FREE cs p). Ob a => (a ** Unit) ~> a
rightUnitor = Struct Monoidal (a **! UnitF) a
-> Free (a **! UnitF) (a **! UnitF) -> Free (a **! UnitF) a
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
Str Struct Monoidal (a **! UnitF) a
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Struct Monoidal (a **! UnitF) a
RightUnitor Free (a **! UnitF) (a **! UnitF)
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id
  rightUnitorInv :: forall (a :: FREE cs p). Ob a => a ~> (a ** Unit)
rightUnitorInv = Struct Monoidal a (a **! UnitF) -> Free a a -> Free a (a **! UnitF)
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
Str Struct Monoidal a (a **! UnitF)
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Struct Monoidal a (a **! UnitF)
RightUnitorInv Free a a
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id
  associator :: forall (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = Struct Monoidal ((a **! b) **! c) (a **! (b **! c))
-> Free ((a **! b) **! c) ((a **! b) **! c)
-> Free ((a **! b) **! c) (a **! (b **! c))
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
Str Struct Monoidal ((a **! b) **! c) (a **! (b **! c))
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p).
(Ob a, Ob b, Ob c) =>
Struct Monoidal ((a **! b) **! c) (a **! (b **! c))
Associator Free ((a **! b) **! c) ((a **! b) **! c)
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id
  associatorInv :: forall (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = Struct Monoidal (a **! (b **! c)) ((a **! b) **! c)
-> Free (a **! (b **! c)) (a **! (b **! c))
-> Free (a **! (b **! c)) ((a **! b) **! c)
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
Str Struct Monoidal (a **! (b **! c)) ((a **! b) **! c)
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p).
(Ob a, Ob b, Ob c) =>
Struct Monoidal (a **! (b **! c)) ((a **! b) **! c)
AssociatorInv Free (a **! (b **! c)) (a **! (b **! c))
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id

instance (SymMonoidal `Elem` cs) => HasStructure cs p SymMonoidal where
  data Struct SymMonoidal i o where
    Swap :: (Ob a, Ob b) => Struct SymMonoidal (a **! b) (b **! a)
  foldStructure :: forall {k} (f :: j +-> k) (a :: FREE cs p) (b :: FREE cs p).
(All cs k, Representable f) =>
(forall (x :: FREE cs p) (y :: FREE cs p).
 (x ~> y) -> Lower f x ~> Lower f y)
-> Struct SymMonoidal a b -> Lower f a ~> Lower f b
foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (Swap @a @b) = forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @a @f (forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @b @f (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @(Lower f a) @(Lower f b)))
deriving instance (WithEq a) => Eq (Struct SymMonoidal a b)
deriving instance (WithShow a) => Show (Struct SymMonoidal a b)
instance (Ok cs p, SymMonoidal `Elem` cs, Monoidal `Elem` cs) => SymMonoidal (FREE cs p) where
  swap :: forall (a :: FREE cs p) (b :: FREE cs p).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap = Struct SymMonoidal (a **! b) (b **! a)
-> Free (a **! b) (a **! b) -> Free (a **! b) (b **! a)
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
Str Struct SymMonoidal (a **! b) (b **! a)
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) (b :: FREE cs p).
(Ob a, Ob b) =>
Struct SymMonoidal (a **! b) (b **! a)
Swap Free (a **! b) (a **! b)
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id

data UnitFtor :: () +-> k
instance (Monoidal k) => FunctorForRep (UnitFtor :: () +-> k) where
  type UnitFtor @ '() = Unit
  fmap :: forall (a :: ()) (b :: ()).
(a ~> b) -> (UnitFtor @ a) ~> (UnitFtor @ b)
fmap a ~> b
Unit a b
U.Unit = (UnitFtor @ a) ~> (UnitFtor @ b)
Obj Unit
forall k. Monoidal k => Obj Unit
unitObj
data MultFtor :: (k, k) +-> k
instance (Monoidal k) => FunctorForRep (MultFtor :: (k, k) +-> k) where
  type MultFtor @ '(a, b) = a ** b
  fmap :: forall (a :: (k, k)) (b :: (k, k)).
(a ~> b) -> (MultFtor @ a) ~> (MultFtor @ 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