{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Monoidal categories, as kinds with a tensor: 'Monoidal' provides 'Unit', the tensor @('**')@,
-- and the unitor and associator isomorphisms; 'SymMonoidal' adds the symmetry 'swap'. A
-- 'MonoidalProfunctor' is a lax monoidal profunctor with 'one' and a value-level @('**')@, and a
-- category is 'Monoidal' if and only if its hom-profunctor is.
module Proarrow.Category.Monoidal where

import Data.Kind (Constraint)
import Data.Type.Nat (Nat (..), SNat (..), SNatI, snat)
import Prelude (Show, ($), type (~))
import Prelude qualified as P

import Proarrow.Category.Instance.Free
  ( Elem (..)
  , Elems
  , FREE (..)
  , Free (..)
  , HasStructure (..)
  , IsFreeOb (..)
  , Lower
  , WithShow
  , withLowerOb
  )
import Proarrow.Category.Instance.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Category.Instance.Product (Fst, Snd, (:**:) (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Kind
  , Obj
  , Profunctor (..)
  , Promonad (..)
  , UN
  , obj
  , src
  , tgt
  , type (+->)
  )
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Optic (PIso, iso)
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), corepUniv)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Identity qualified as Id
import Proarrow.Profunctor.Representable (CorepStar, Rep, RepCostar, Representable (..), repUniv)
import Proarrow.Tools.Laws (Inverses (..), Law (..), Laws (..), ProLaw (..), ProLaws (..), inverses, (=:=), (===))

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
  one :: p Unit Unit
  (**) :: p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)

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

instance (MonoidalProfunctor p, MonoidalProfunctor q) => MonoidalProfunctor (p :**: q) where
  one :: (:**:) p q Unit Unit
one = p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one 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
one
  (p a1 b1
f1 :**: q a2 b2
f2) ** :: 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)
** (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)
** 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)
** q a2 b2
g2)

instance (Monoidal k) => MonoidalProfunctor (Id.Id :: k +-> k) where
  one :: Id Unit Unit
one = (Unit ~> Unit) -> Id Unit Unit
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id.Id Unit ~> Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one
  Id.Id x1 ~> x2
f ** :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
Id x1 x2 -> Id y1 y2 -> Id (x1 ** y1) (x2 ** y2)
** Id.Id y1 ~> y2
g = ((x1 ** y1) ~> (x2 ** y2)) -> Id (x1 ** y1) (x2 ** y2)
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id.Id (x1 ~> x2
f (x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
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)
** y1 ~> y2
g)

instance (MonoidalProfunctor p, MonoidalProfunctor q) => MonoidalProfunctor (p :.: q) where
  one :: (:.:) p q Unit Unit
one = p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one p Unit Unit -> q Unit Unit -> (:.:) p q Unit Unit
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: q Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one
  (p x1 b
p :.: q b x2
q) ** :: forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
(:.:) p q x1 x2
-> (:.:) p q y1 y2 -> (:.:) p q (x1 ** y1) (x2 ** y2)
** (p y1 b
r :.: q b y2
s) = (p x1 b
p p x1 b -> p y1 b -> p (x1 ** y1) (b ** b)
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)
** p y1 b
r) p (x1 ** y1) (b ** b)
-> q (b ** b) (x2 ** y2) -> (:.:) p q (x1 ** y1) (x2 ** y2)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: (q b x2
q q b x2 -> q b y2 -> q (b ** b) (x2 ** y2)
forall (x1 :: j) (x2 :: j) (y1 :: j) (y2 :: j).
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)
** q b y2
s)

-- | A representable profunctor that is a 'MonoidalProfunctor': its functor @p '%'@ is /lax/
-- monoidal, splitting as 'par0Rep' and 'parRep'.
type LaxMonoidal p = (MonoidalProfunctor p, Representable p)

par0Rep :: (LaxMonoidal p) => Unit ~> p % Unit
par0Rep :: forall {j} {k} (p :: j +-> k). LaxMonoidal 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
one

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

-- | A corepresentable profunctor that is a 'MonoidalProfunctor': its functor @p '%%'@ is /oplax/
-- monoidal, splitting as 'unpar0Corep' and 'unparCorep'.
type OplaxMonoidal p = (MonoidalProfunctor p, Corepresentable p)

unpar0Corep :: (OplaxMonoidal p) => p %% Unit ~> Unit
unpar0Corep :: forall {k} {k} (p :: k +-> k).
OplaxMonoidal 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
one

unparCorep :: (OplaxMonoidal p, Ob x, Ob y) => p %% (x ** y) ~> (p %% x) ** (p %% y)
unparCorep :: forall {j} {k} (p :: j +-> k) (x :: k) (y :: k).
(OplaxMonoidal 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)
corepUniv @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)
** 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)
corepUniv @p @y)

-- | A __representable__ profunctor whose functor @p '%'@ is /oplax/ monoidal. Stating the oplax
-- structure of a representable functor means naming that same functor in its other variance, as
-- 'RepCostar' does. So the postfix here says which presentation @p@ is in, not which structure it
-- carries. Weaker than 'StrongMonoidalRep', which additionally asks @p@ itself to be
-- 'LaxMonoidal'.
type OplaxMonoidalRep p = (Representable p, OplaxMonoidal (RepCostar p))

unpar0Rep :: (OplaxMonoidalRep p) => p % Unit ~> Unit
unpar0Rep :: forall {j} {k} (p :: j +-> k).
OplaxMonoidalRep p =>
(p % Unit) ~> Unit
unpar0Rep @p = forall {k} {k} (p :: k +-> k).
OplaxMonoidal p =>
(p %% Unit) ~> Unit
forall (p :: k +-> j). OplaxMonoidal p => (p %% Unit) ~> Unit
unpar0Corep @(RepCostar p)

unparRep :: (OplaxMonoidalRep p, Ob x, Ob y) => p % (x ** y) ~> (p % x) ** (p % y)
unparRep :: forall {j} {k} (p :: j +-> k) (x :: j) (y :: j).
(OplaxMonoidalRep 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).
(OplaxMonoidal p, Ob x, Ob y) =>
(p %% (x ** y)) ~> ((p %% x) ** (p %% y))
forall (p :: k +-> j) (x :: j) (y :: j).
(OplaxMonoidal p, Ob x, Ob y) =>
(p %% (x ** y)) ~> ((p %% x) ** (p %% y))
unparCorep @(RepCostar p) @x @y

-- | A __corepresentable__ profunctor whose functor @p '%%'@ is /lax/ monoidal, dually through
-- 'CorepStar'.
type LaxMonoidalCorep p = (Corepresentable p, LaxMonoidal (CorepStar p))

par0Corep :: (LaxMonoidalCorep p) => Unit ~> p %% Unit
par0Corep :: forall {k} {k} (p :: k +-> k).
LaxMonoidalCorep p =>
Unit ~> (p %% Unit)
par0Corep @p = forall {j} {k} (p :: j +-> k). LaxMonoidal p => Unit ~> (p % Unit)
forall (p :: k +-> k). LaxMonoidal p => Unit ~> (p % Unit)
par0Rep @(CorepStar p)

parCorep :: (LaxMonoidalCorep p, Ob x, Ob y) => (p %% x) ** (p %% y) ~> p %% (x ** y)
parCorep :: forall {j} {k} (p :: j +-> k) (x :: k) (y :: k).
(LaxMonoidalCorep 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).
(LaxMonoidal p, Ob x, Ob y) =>
((p % x) ** (p % y)) ~> (p % (x ** y))
forall (p :: k +-> j) (x :: k) (y :: k).
(LaxMonoidal p, Ob x, Ob y) =>
((p % x) ** (p % y)) ~> (p % (x ** y))
parRep @(CorepStar p) @x @y

-- | A representable profunctor whose functor is /strong/ monoidal: lax as it stands, and oplax in
-- its other variance.
type StrongMonoidalRep p = (LaxMonoidal p, OplaxMonoidalRep p)

-- | A corepresentable profunctor whose functor is /strong/ monoidal, dually.
type StrongMonoidalCorep p = (OplaxMonoidal p, LaxMonoidalCorep p)

-- | A monoidal category: a tensor @'**'@ with a 'Unit', associative and unital up to the coherent
-- isomorphisms below. The tensor's action on arrows is the 'MonoidalProfunctor' method @**@ at
-- @('~>')@, which the superclass supplies.
--
-- __Laws:__
--
-- The three isomorphisms must be mutually inverse:
--
-- * @'leftUnitor' . 'leftUnitorInv' = 'id'@ and @'leftUnitorInv' . 'leftUnitor' = 'id'@
-- * @'rightUnitor' . 'rightUnitorInv' = 'id'@ and @'rightUnitorInv' . 'rightUnitor' = 'id'@
-- * @'associator' . 'associatorInv' = 'id'@ and @'associatorInv' . 'associator' = 'id'@
--
-- and natural in every argument:
--
-- * @'leftUnitor' . ('id' '**' f) = f . 'leftUnitor'@
-- * @'rightUnitor' . (f '**' 'id') = f . 'rightUnitor'@
-- * @'associator' . ((f '**' g) '**' h) = (f '**' (g '**' h)) . 'associator'@
--
-- subject to the two coherence conditions:
--
-- * Triangle: @('id' '**' 'leftUnitor') . 'associator' = 'rightUnitor' '**' 'id'@
-- * Pentagon: @('id' '**' 'associator') . 'associator' . ('associator' '**' 'id')
--   = 'associator' . 'associator'@
--
-- Checked by 'Proarrow.Testing.Laws.testMonoidal'.
type Monoidal :: Kind -> Constraint
class (CategoryOf k, MonoidalProfunctor ((~>) :: CAT k), Ob (Unit :: k)) => Monoidal k where
  -- | The tensor unit.
  type Unit :: k

  -- | The tensor product of two objects.
  type (a :: k) ** (b :: k) :: k

  -- | Recovers @'Ob' (a '**' b)@ from the objecthood of the factors.
  withOb2 :: (Ob (a :: k), Ob b) => ((Ob (a ** b)) => r) -> r

  -- | Cancels a 'Unit' on the left.
  leftUnitor :: (Ob (a :: k)) => Unit ** a ~> a
  default leftUnitor :: (Ob (a :: k), (Unit ** a) ~ a) => Unit ** a ~> a
  leftUnitor = a ~> a
(Unit ** a) ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id

  -- | Introduces a 'Unit' on the left; inverse to 'leftUnitor'.
  leftUnitorInv :: (Ob (a :: k)) => a ~> Unit ** a
  default leftUnitorInv :: (Ob (a :: k), (Unit ** a) ~ a) => a ~> Unit ** a
  leftUnitorInv = a ~> a
a ~> (Unit ** a)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id

  -- | Cancels a 'Unit' on the right.
  rightUnitor :: (Ob (a :: k)) => a ** Unit ~> a
  default rightUnitor :: (Ob (a :: k), (a ** Unit) ~ a) => a ** Unit ~> a
  rightUnitor = a ~> a
(a ** Unit) ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id

  -- | Introduces a 'Unit' on the right; inverse to 'rightUnitor'.
  rightUnitorInv :: (Ob (a :: k)) => a ~> a ** Unit
  default rightUnitorInv :: (Ob (a :: k), (a ** Unit) ~ a) => a ~> a ** Unit
  rightUnitorInv = a ~> a
a ~> (a ** Unit)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id

  -- | Reassociates the tensor to the right.
  associator :: (Ob (a :: k), Ob b, Ob c) => (a ** b) ** c ~> a ** (b ** c)

  -- | Reassociates the tensor to the left; inverse to 'associator'.
  associatorInv :: (Ob (a :: k), Ob b, Ob c) => a ** (b ** c) ~> (a ** b) ** c

leftUnitorIso :: (Monoidal k, Ob (a :: k), Ob (a' :: k)) => PIso (Unit ** a) (Unit ** a') a a'
leftUnitorIso :: forall k (a :: k) (a' :: k).
(Monoidal k, Ob a, Ob a') =>
PIso (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} (c :: (j +-> k) -> Constraint) (s :: k) (t :: j)
       (a :: k) (b :: j).
(CategoryOf j, CategoryOf k) =>
(s ~> a) -> (b ~> t) -> Optic c 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)) => PIso (a ** Unit) (a' ** Unit) a a'
rightUnitorIso :: forall k (a :: k) (a' :: k).
(Monoidal k, Ob a, Ob a') =>
PIso (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} (c :: (j +-> k) -> Constraint) (s :: k) (t :: j)
       (a :: k) (b :: j).
(CategoryOf j, CategoryOf k) =>
(s ~> a) -> (b ~> t) -> Optic c 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')
  => PIso ((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') =>
PIso
  ((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} (c :: (j +-> k) -> Constraint) (s :: k) (t :: j)
       (a :: k) (b :: j).
(CategoryOf j, CategoryOf k) =>
(s ~> a) -> (b ~> t) -> Optic c 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')

class (((a ** b) ** c) ~ (a ** (b ** c))) => StrictlyAssoc a b c
instance (((a ** b) ** c) ~ (a ** (b ** c))) => StrictlyAssoc a b c

-- | The @n@-fold tensor power of @x@: @x '**' x '**' … '**' x@, @n@ times, terminated by 'Unit'.
type family NFold (n :: Nat) (x :: k) :: k where
  NFold Z x = Unit
  NFold (S n) x = x ** NFold n x

-- | The 'Proarrow.Category.Monoidal.Strictified.Strictified' counterpart of 'NFold': @n@ copies
-- of @x@ as a list, rather than nested tensors.
type family NFoldS (n :: Nat) (x :: k) :: [k] where
  NFoldS Z x = '[]
  NFoldS (S n) x = x ': NFoldS n x

-- | @'NFold' n a@ is an object whenever @a@ is.
withObNFold :: forall {k} n (a :: k) r. (SNatI n, Ob a, Monoidal k) => ((Ob (NFold n a)) => r) -> r
withObNFold :: forall {k} (n :: Nat) (a :: k) r.
(SNatI n, Ob a, Monoidal k) =>
(Ob (NFold n a) => r) -> r
withObNFold Ob (NFold n a) => r
r = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ -> r
Ob (NFold n a) => r
r
  SS @n' -> forall {k} (n :: Nat) (a :: k) r.
(SNatI n, Ob a, Monoidal k) =>
(Ob (NFold n a) => r) -> r
forall (n :: Nat) (a :: k) r.
(SNatI n, Ob a, Monoidal k) =>
(Ob (NFold n a) => r) -> r
withObNFold @n' @a (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @(NFold n' a) r
Ob (a ** NFold n1 a) => r
Ob (NFold n a) => r
r)

-- | If your monoidal category is a strict monoidal category, add 'Strictly' to your 'Ob' constraint.
-- This will let GHC know that the unitors and associators are strict, so you won't have to provide proof of that.
--
-- The four unitors then default to 'id'. The defaults need only @'Unit' '**' a ~ a@ and
-- @a '**' 'Unit' ~ a@, so they also fire for a strictly unital category such as
-- 'Proarrow.Category.Instance.Mat.MatK' or 'Proarrow.Category.Instance.ZX.ZX'. Both associators
-- can use 'associatorDefault':
--
-- @
-- associator \@a \@b \@c = associatorDefault \@a \@b \@c
-- associatorInv \@a \@b \@c = associatorDefault \@a \@b \@c
-- @
type Strictly :: forall {k}. k -> Constraint
class (a ** Unit ~ a, Unit ** a ~ a, forall b c. (Ob b, Ob c) => StrictlyAssoc a b c) => Strictly (a :: k) where
  associatorDefault :: forall b c. (Monoidal k, Ob a, Ob b, Ob c) => (a ** b) ** c ~> a ** (b ** c)

instance (a ** Unit ~ a, Unit ** a ~ a, forall b c. (Ob b, Ob c) => StrictlyAssoc a b c) => Strictly (a :: k) where
  associatorDefault :: forall (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associatorDefault @b @c = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @b @c (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @(b ** c) (a ** (b ** c)) ~> (a ** (b ** c))
((a ** b) ** c) ~> (a ** (b ** c))
Ob (a ** (b ** c)) => ((a ** b) ** c) ~> (a ** (b ** c))
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id)

instance Monoidal () where
  type Unit = '()

  -- a wildcard, not @'()@, so that @a ** b@ reduces for an abstract @a@, as on pairs
  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)

  -- Through the projections rather than by matching the pair, so that @a ** b@ reduces for an
  -- abstract @a@: the quantified @a ** b ~ a && b@ of 'Proarrow.Category.Monoidal.Cartesian.Cartesian'
  -- needs that.
  type a ** b = '(Fst @ a ** Fst @ b, Snd @ a ** Snd @ b)
  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
  one :: Op p Unit Unit
one = 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
one
  Op p b1 a1
l ** :: 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)
** 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)
** 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)

(==) :: (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 :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
f

-- | The identity on a tensor. It is built from 'withOb2' rather than as @obj \@a '**' obj \@b@,
-- so that an instance's own '**' can use it without calling itself.
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 k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @b (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(a ** 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 :: CAT 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 :: CAT 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 :: CAT 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 :: CAT 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 :: CAT 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)
** 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)
** 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 :: CAT 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 :: CAT 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)
** 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)
** 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 :: CAT 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
one

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)
** 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)
** 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 :: CAT 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)
** 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)
** (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 :: CAT 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)
** (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 :: CAT 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)
** 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 :: CAT 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 :: CAT 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)
** (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 :: CAT 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)
** (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 :: CAT 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)
** 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 :: CAT 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 :: CAT 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)
** 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 :: CAT 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 :: CAT 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)
** 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)
** 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 :: CAT 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 :: CAT 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)
** 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)
** 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 :: CAT 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 :: CAT 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)
** 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)
** a2 ~> b2
g
type Tensor = Rep MultRep

data family UnitF :: k
instance (Monoidal `Elem` cs) => IsFreeOb (UnitF :: FREE cs p) where
  type Lower f UnitF = Unit
  lowerOb :: forall k' (f :: k +-> k') r.
(Representable f, All cs k') =>
(Ob (Lower f UnitF) => r) -> r
lowerOb @k' @_ Ob (Lower f UnitF) => r
r = forall (c :: Type -> Constraint) (cs :: [Type -> Constraint]) k r.
(Elem c cs, All cs k) =>
(c k => r) -> r
fromAll @Monoidal @cs @k' r
Ob (Lower f UnitF) => r
Monoidal k' => r
r
data family (**!) (a :: k) (b :: k) :: k
instance (IsFreeOb (a :: FREE cs p), IsFreeOb b, Monoidal `Elem` cs) => IsFreeOb (a **! b) where
  type Lower f (a **! b) = Lower f a ** Lower f b
  lowerOb :: forall k' (f :: k +-> k') r.
(Representable f, All cs k') =>
(Ob (Lower f (a **! b)) => r) -> r
lowerOb @k' @f Ob (Lower f (a **! b)) => r
r = forall (c :: Type -> Constraint) (cs :: [Type -> Constraint]) k r.
(Elem c cs, All cs k) =>
(c k => r) -> r
fromAll @Monoidal @cs @k' (forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @b (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k' @(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 :: CAT k) 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 :: k +-> k') (a :: FREE cs p) (b :: FREE cs p).
(Monoidal k', 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:StructkcspMonoidalio k cs p a b
Par0 = Lower f a ~> Lower f b
Unit ~> Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one
  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)
** (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 {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (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 {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a 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 {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (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 {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a 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 {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @b (forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @c' (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 {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @b (forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @c' (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'))))
instance (WithShow a) => Show (Struct Monoidal a b) where
  showsPrec :: Int -> Struct Monoidal a b -> ShowS
showsPrec Int
_ Struct Monoidal a b
R:StructkcspMonoidalio k cs p a b
Par0 = String -> ShowS
P.showString String
"one"
  showsPrec Int
d (Par a ~> b
f c ~> d
g) = Bool -> ShowS -> ShowS
P.showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
P.> Int
8) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> Free a b -> ShowS
forall a. Show a => Int -> a -> ShowS
P.showsPrec Int
9 a ~> b
Free a b
f ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. String -> ShowS
P.showString String
" ** " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Int -> Free c d -> ShowS
forall a. Show a => Int -> a -> ShowS
P.showsPrec Int
9 c ~> d
Free c d
g
  showsPrec Int
_ Struct Monoidal a b
R:StructkcspMonoidalio k cs p a b
LeftUnitor = String -> ShowS
P.showString String
"leftUnitor"
  showsPrec Int
_ Struct Monoidal a b
R:StructkcspMonoidalio k cs p a b
LeftUnitorInv = String -> ShowS
P.showString String
"leftUnitorInv"
  showsPrec Int
_ Struct Monoidal a b
R:StructkcspMonoidalio k cs p a b
RightUnitor = String -> ShowS
P.showString String
"rightUnitor"
  showsPrec Int
_ Struct Monoidal a b
R:StructkcspMonoidalio k cs p a b
RightUnitorInv = String -> ShowS
P.showString String
"rightUnitorInv"
  showsPrec Int
_ Struct Monoidal a b
R:StructkcspMonoidalio k cs p a b
Associator = String -> ShowS
P.showString String
"associator"
  showsPrec Int
_ Struct Monoidal a b
R:StructkcspMonoidalio k cs p a b
AssociatorInv = String -> ShowS
P.showString String
"associatorInv"

instance (Monoidal `Elem` cs) => MonoidalProfunctor (Free :: CAT (FREE cs (p :: CAT k))) where
  one :: Free Unit Unit
one = Struct Monoidal UnitF UnitF -> Free UnitF UnitF -> Free UnitF UnitF
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (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
St Struct Monoidal UnitF UnitF
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}.
Struct Monoidal UnitF UnitF
Par0 Free UnitF UnitF
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil
  Free x1 x2
f ** :: 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)
** Free y1 y2
g = Struct Monoidal (x1 **! y1) (x2 **! y2)
-> Free (x1 **! y1) (x1 **! y1) -> Free (x1 **! y1) (x2 **! y2)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (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
St ((x1 ~> x2) -> (y1 ~> y2) -> Struct Monoidal (x1 **! y1) (x2 **! y2)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (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 {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil ((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 (Monoidal `Elem` cs) => Monoidal (FREE cs (p :: CAT k)) 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 {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (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
St Struct Monoidal (UnitF **! a) a
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Struct Monoidal (UnitF **! a) a
LeftUnitor Free (UnitF **! a) (UnitF **! a)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil
  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 {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (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
St Struct Monoidal a (UnitF **! a)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Struct Monoidal a (UnitF **! a)
LeftUnitorInv Free a a
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil
  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 {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (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
St Struct Monoidal (a **! UnitF) a
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Struct Monoidal (a **! UnitF) a
RightUnitor Free (a **! UnitF) (a **! UnitF)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil
  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 {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (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
St Struct Monoidal a (a **! UnitF)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Struct Monoidal a (a **! UnitF)
RightUnitorInv Free a a
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil
  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 {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (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
St Struct Monoidal ((a **! b) **! c) (a **! (b **! c))
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (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 {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil
  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 {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (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
St Struct Monoidal (a **! (b **! c)) ((a **! b) **! c)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (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 {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil

-- | The structures the free category needs for 'SymMonoidal', and those its laws are stated for.
type SymMonoidalStructures :: [Kind -> Constraint]
type SymMonoidalStructures = '[Monoidal, SymMonoidal]

instance (SymMonoidalStructures `Elems` cs) => HasStructure cs (p :: CAT k) SymMonoidal where
  data Struct SymMonoidal i o where
    Swap :: (Ob a, Ob b) => Struct SymMonoidal (a **! b) (b **! a)
  foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p).
(SymMonoidal k', 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 {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @b (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @(Lower f a) @(Lower f b)))
instance Show (Struct SymMonoidal a b) where
  showsPrec :: Int -> Struct SymMonoidal a b -> ShowS
showsPrec Int
_ Struct SymMonoidal a b
R:StructkcspSymMonoidalio k cs p a b
Swap = String -> ShowS
P.showString String
"swap"

instance (SymMonoidalStructures `Elems` cs) => SymMonoidal (FREE cs (p :: CAT k)) 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 {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (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
St Struct SymMonoidal (a **! b) (b **! a)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (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 {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil

-- | The tensor is a bifunctor, and the unitors and the associator are natural isomorphisms
-- satisfying the triangle and pentagon identities.
instance Laws '[Monoidal] where
  laws :: [Law '[Monoidal]]
laws =
    String -> PureLawBody '[Monoidal] Inverses -> [Law '[Monoidal]]
forall (cs :: [Type -> Constraint]).
String -> PureLawBody cs Inverses -> [Law cs]
inverses String
"leftUnitor" (\ @a -> ((Unit ** a) ~> a) -> (a ~> (Unit ** a)) -> Inverses k
forall {k} (a :: k) (b :: k). (a ~> b) -> (b ~> a) -> Inverses k
Inverses (forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @_ @a) (forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @_ @a))
      [Law '[Monoidal]] -> [Law '[Monoidal]] -> [Law '[Monoidal]]
forall a. [a] -> [a] -> [a]
P.++ String -> PureLawBody '[Monoidal] Inverses -> [Law '[Monoidal]]
forall (cs :: [Type -> Constraint]).
String -> PureLawBody cs Inverses -> [Law cs]
inverses String
"rightUnitor" (\ @a -> ((a ** Unit) ~> a) -> (a ~> (a ** Unit)) -> Inverses k
forall {k} (a :: k) (b :: k). (a ~> b) -> (b ~> a) -> Inverses k
Inverses (forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor @_ @a) (forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv @_ @a))
      [Law '[Monoidal]] -> [Law '[Monoidal]] -> [Law '[Monoidal]]
forall a. [a] -> [a] -> [a]
P.++ String -> PureLawBody '[Monoidal] Inverses -> [Law '[Monoidal]]
forall (cs :: [Type -> Constraint]).
String -> PureLawBody cs Inverses -> [Law cs]
inverses
        String
"associator"
        (\ @a @b @c -> (((a ** b) ** c) ~> (a ** (b ** c)))
-> ((a ** (b ** c)) ~> ((a ** b) ** c)) -> Inverses k
forall {k} (a :: k) (b :: k). (a ~> b) -> (b ~> a) -> Inverses k
Inverses (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @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 @_ @a @b @c))
      [Law '[Monoidal]] -> [Law '[Monoidal]] -> [Law '[Monoidal]]
forall a. [a] -> [a] -> [a]
P.++ [ String -> LawBody '[Monoidal] -> Law '[Monoidal]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"tensor identity" \ @a @b forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @b (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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b ((a ** b) ~> (a ** b)) -> ((a ** b) ~> (a ** b)) -> m (Equation k)
forall {i} (m :: Type -> Type) r (a :: i) (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== (a ** b) ~> (a ** b)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id)
           , String -> LawBody '[Monoidal] -> Law '[Monoidal]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"tensor interchange" \ @a @b @c @d @e forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> do
               f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @a @b String
"f"
               g <- mor @b @c "g"
               h <- mor @d @e "h"
               i <- mor @e @c "i"
               (g . f) ** (i . h) === (g ** i) . (f ** h)
           , String -> LawBody '[Monoidal] -> Law '[Monoidal]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"leftUnitor naturality" \ @a @b forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> do
               f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @a @b String
"f"
               leftUnitor @_ @b . (one ** f) === f . leftUnitor @_ @a
           , String -> LawBody '[Monoidal] -> Law '[Monoidal]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"leftUnitorInv naturality" \ @a @b forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> do
               f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @a @b String
"f"
               leftUnitorInv @_ @b . f === (one ** f) . leftUnitorInv @_ @a
           , String -> LawBody '[Monoidal] -> Law '[Monoidal]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"rightUnitor naturality" \ @a @b forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> do
               f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @a @b String
"f"
               rightUnitor @_ @b . (f ** one) === f . rightUnitor @_ @a
           , String -> LawBody '[Monoidal] -> Law '[Monoidal]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"rightUnitorInv naturality" \ @a @b forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> do
               f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @a @b String
"f"
               rightUnitorInv @_ @b . f === (f ** one) . rightUnitorInv @_ @a
           , String -> LawBody '[Monoidal] -> Law '[Monoidal]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"associator naturality" \ @a @b @c @d forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> do
               f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @a @b String
"f"
               g <- mor @b @c "g"
               h <- mor @c @d "h"
               associator @_ @b @c @d . ((f ** g) ** h) === (f ** (g ** h)) . associator @_ @a @b @c
           , String -> LawBody '[Monoidal] -> Law '[Monoidal]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"associatorInv naturality" \ @a @b @c @d forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> do
               f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @a @b String
"f"
               g <- mor @b @c "g"
               h <- mor @c @d "h"
               associatorInv @_ @b @c @d . (f ** (g ** h)) === ((f ** g) ** h) . associatorInv @_ @a @b @c
           , String -> LawBody '[Monoidal] -> Law '[Monoidal]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"triangle identity" \ @a @b forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ ->
               (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) ~> b) -> (a ** (Unit ** 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)
** forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @_ @b) ((a ** (Unit ** b)) ~> (a ** b))
-> (((a ** Unit) ** b) ~> (a ** (Unit ** b)))
-> ((a ** Unit) ** b) ~> (a ** b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @a @Unit @b (((a ** Unit) ** b) ~> (a ** b))
-> (((a ** Unit) ** b) ~> (a ** b)) -> m (Equation k)
forall {i} (m :: Type -> Type) r (a :: i) (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor @_ @a ((a ** Unit) ~> a) -> (b ~> b) -> ((a ** Unit) ** 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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b
           , String -> LawBody '[Monoidal] -> Law '[Monoidal]
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"pentagon identity" \ @a @b @c @d forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ ->
               forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @b ((Ob (a ** b) => m (Equation k)) -> m (Equation k))
-> (Ob (a ** b) => m (Equation k)) -> m (Equation k)
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 @_ @b @c ((Ob (b ** c) => m (Equation k)) -> m (Equation k))
-> (Ob (b ** c) => m (Equation k)) -> m (Equation k)
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 @_ @c @d ((Ob (c ** d) => m (Equation k)) -> m (Equation k))
-> (Ob (c ** d) => m (Equation k)) -> m (Equation k)
forall a b. (a -> b) -> a -> b
$
                     (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) ~> (b ** (c ** d)))
-> (a ** ((b ** c) ** d)) ~> (a ** (b ** (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)
** forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @b @c @d)
                       ((a ** ((b ** c) ** d)) ~> (a ** (b ** (c ** d))))
-> ((((a ** b) ** c) ** d) ~> (a ** ((b ** c) ** d)))
-> (((a ** b) ** c) ** d) ~> (a ** (b ** (c ** d)))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @a @(b ** c) @d
                       (((a ** (b ** c)) ** d) ~> (a ** ((b ** c) ** d)))
-> ((((a ** b) ** c) ** d) ~> ((a ** (b ** c)) ** d))
-> (((a ** b) ** c) ** d) ~> (a ** ((b ** c) ** d))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @a @b @c (((a ** b) ** c) ~> (a ** (b ** c)))
-> (d ~> d) -> (((a ** b) ** c) ** d) ~> ((a ** (b ** 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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @d)
                       ((((a ** b) ** c) ** d) ~> (a ** (b ** (c ** d))))
-> ((((a ** b) ** c) ** d) ~> (a ** (b ** (c ** d))))
-> m (Equation k)
forall {i} (m :: Type -> Type) r (a :: i) (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @a @b @(c ** d)
                         (((a ** b) ** (c ** d)) ~> (a ** (b ** (c ** d))))
-> ((((a ** b) ** c) ** d) ~> ((a ** b) ** (c ** d)))
-> (((a ** b) ** c) ** d) ~> (a ** (b ** (c ** d)))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @(a ** b) @c @d
           ]

-- | 'swap' is a natural self-inverse satisfying the hexagon identity.
instance Laws SymMonoidalStructures where
  laws :: [Law SymMonoidalStructures]
laws =
    [ String
-> LawBody SymMonoidalStructures -> Law SymMonoidalStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"swap self-inverse" \ @a @b forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ -> (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @b @a ((b ** a) ~> (a ** b))
-> ((a ** b) ~> (b ** a)) -> (a ** b) ~> (a ** b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @a @b ((a ** b) ~> (a ** b)) -> ((a ** b) ~> (a ** b)) -> m (Equation k)
forall {i} (m :: Type -> Type) r (a :: i) (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== (a ** b) ~> (a ** b)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id) ((Ob (a ** b), Ob (b ** a)) => m (Equation k))
-> ((a ** b) ~> (b ** a)) -> m (Equation k)
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
\\ forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @a @b
    , String
-> LawBody SymMonoidalStructures -> Law SymMonoidalStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"swap naturality" \ @a @b @c @d forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> do
        f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @a @c String
"f"
        g <- mor @b @d "g"
        swap @_ @c @d . (f ** g) === (g ** f) . swap @_ @a @b
    , String
-> LawBody SymMonoidalStructures -> Law SymMonoidalStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"hexagon identity" \ @a @b @c forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ ->
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @b @c ((Ob (b ** c) => m (Equation k)) -> m (Equation k))
-> (Ob (b ** c) => m (Equation k)) -> m (Equation k)
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))
associator @_ @b @c @a
            (((b ** c) ** a) ~> (b ** (c ** a)))
-> (((a ** b) ** c) ~> ((b ** c) ** a))
-> ((a ** b) ** c) ~> (b ** (c ** a))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @a @(b ** c)
            ((a ** (b ** c)) ~> ((b ** c) ** a))
-> (((a ** b) ** c) ~> (a ** (b ** c)))
-> ((a ** b) ** c) ~> ((b ** c) ** a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @a @b @c
            (((a ** b) ** c) ~> (b ** (c ** a)))
-> (((a ** b) ** c) ~> (b ** (c ** a))) -> m (Equation k)
forall {i} (m :: Type -> Type) r (a :: i) (b :: i).
(Applicative m, ArrowEquation i r) =>
(a ~> b) -> (a ~> b) -> m r
=== (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b Obj b
-> ((a ** c) ~> (c ** a)) -> (b ** (a ** c)) ~> (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)
** forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @a @c)
              ((b ** (a ** c)) ~> (b ** (c ** a)))
-> (((a ** b) ** c) ~> (b ** (a ** c)))
-> ((a ** b) ** c) ~> (b ** (c ** a))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @b @a @c
              (((b ** a) ** c) ~> (b ** (a ** c)))
-> (((a ** b) ** c) ~> ((b ** a) ** c))
-> ((a ** b) ** c) ~> (b ** (a ** c))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @a @b ((a ** b) ~> (b ** a))
-> (c ~> c) -> ((a ** b) ** c) ~> ((b ** a) ** 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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c)
    ]

-- | 'one' is a unit for '**' up to the unitors, '**' is associative up to the associators, and
-- '**' is natural.
instance ProLaws MonoidalProfunctor where
  proLaws :: [ProLaw MonoidalProfunctor]
proLaws =
    [ String
-> ProLawBody MonoidalProfunctor -> ProLaw MonoidalProfunctor
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"left unit" \ @_ @a @b p a b
p forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> p a b
p p a b -> p a b -> m (ProEquation p)
forall {j} {k} (m :: Type -> Type) (p :: j +-> k) (a :: k)
       (b :: j).
Applicative m =>
p a b -> p a b -> m (ProEquation p)
=:= (a ~> (Unit ** a))
-> ((Unit ** b) ~> b) -> p (Unit ** a) (Unit ** b) -> p a b
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @_ @a) (forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @_ @b) (p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one p Unit Unit -> p a b -> p (Unit ** a) (Unit ** b)
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)
** p a b
p)
    , String
-> ProLawBody MonoidalProfunctor -> ProLaw MonoidalProfunctor
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody c -> ProLaw c
ProLaw String
"right unit" \ @_ @a @b p a b
p forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ -> p a b
p p a b -> p a b -> m (ProEquation p)
forall {j} {k} (m :: Type -> Type) (p :: j +-> k) (a :: k)
       (b :: j).
Applicative m =>
p a b -> p a b -> m (ProEquation p)
=:= (a ~> (a ** Unit))
-> ((b ** Unit) ~> b) -> p (a ** Unit) (b ** Unit) -> p a b
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv @_ @a) (forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor @_ @b) (p a b
p p a b -> p Unit Unit -> p (a ** Unit) (b ** Unit)
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)
** p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one)
    , String
-> ProLawBody3 MonoidalProfunctor -> ProLaw MonoidalProfunctor
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody3 c -> ProLaw c
ProLaw3 String
"associativity" \ @_ @a @b @c @d @e @f p a b
p p c d
p' p e f
p'' forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
_ ->
        (p a b
p p a b -> p c d -> p (a ** c) (b ** d)
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)
** p c d
p') p (a ** c) (b ** d) -> p e f -> p ((a ** c) ** e) ((b ** d) ** f)
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)
** p e f
p'' p ((a ** c) ** e) ((b ** d) ** f)
-> p ((a ** c) ** e) ((b ** d) ** f) -> m (ProEquation p)
forall {j} {k} (m :: Type -> Type) (p :: j +-> k) (a :: k)
       (b :: j).
Applicative m =>
p a b -> p a b -> m (ProEquation p)
=:= (((a ** c) ** e) ~> (a ** (c ** e)))
-> ((b ** (d ** f)) ~> ((b ** d) ** f))
-> p (a ** (c ** e)) (b ** (d ** f))
-> p ((a ** c) ** e) ((b ** d) ** f)
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @a @c @e) (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @_ @b @d @f) (p a b
p p a b -> p (c ** e) (d ** f) -> p (a ** (c ** e)) (b ** (d ** f))
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)
** (p c d
p' p c d -> p e f -> p (c ** e) (d ** f)
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)
** p e f
p''))
    , String
-> ProLawBody3 MonoidalProfunctor -> ProLaw MonoidalProfunctor
forall {j} {k} (c :: (j +-> k) -> Constraint).
String -> ProLawBody3 c -> ProLaw c
ProLaw3 String
"** naturality" \ @_ @a @b @c @d @e @f p a b
p p c d
p' p e f
_ forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
morK forall (x :: j) (y :: j). (Ob x, Ob y) => String -> m (x ~> y)
morJ -> do
        g <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
morK @e @a String
"g"
        g' <- morK @e @c "g'"
        h <- morJ @b @f "h"
        h' <- morJ @d @f "h'"
        dimap (g ** g') (h ** h') (p ** p') =:= dimap g h p ** dimap g' h' p'
    ]