module Proarrow.Category.Instance.IntConstruction where

import Prelude (type (~))

import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , SymMonoidal (..)
  , TracedMonoidal
  , obj2
  , par
  , swap
  , swapFst
  , swapInner
  , swapOuter
  , swapSnd
  , trace
  )
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault, obj)
import Proarrow.Object.Dual (CompactClosed (..), Dual, ExpSA, StarAutonomous (..), currySA, expSA, uncurrySA)
import Proarrow.Object.Exponential (Closed (..))

data INT k = I k k

type family IntPlus (i :: INT k) :: k where
  IntPlus (I a b) = a
type family IntMinus (i :: INT k) :: k where
  IntMinus (I a b) = b

type IntConstruction :: CAT (INT k)
data IntConstruction a b where
  Int :: (Ob ap, Ob am, Ob bp, Ob bm) => ap ** bm ~> am ** bp -> IntConstruction (I ap am) (I bp bm)

toInt :: forall {k} (a :: k) b. (TracedMonoidal k, Ob (Unit :: k)) => (a ~> b) -> I a Unit ~> I b Unit
toInt :: forall {k} (a :: k) (b :: k).
(TracedMonoidal k, Ob Unit) =>
(a ~> b) -> 'I a Unit ~> 'I b Unit
toInt a ~> b
f = ((a ** Unit) ~> (Unit ** b))
-> IntConstruction ('I a Unit) ('I b Unit)
forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k).
(Ob ap, Ob am, Ob bp, Ob bm) =>
((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)
Int (forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @b @Unit ((b ** Unit) ~> (Unit ** b))
-> ((a ** Unit) ~> (b ** Unit)) -> (a ** Unit) ~> (Unit ** b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ~> b
f (a ~> b) -> (Unit ~> Unit) -> (a ** Unit) ~> (b ** Unit)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @Unit)) ((Ob a, Ob b) => IntConstruction ('I a Unit) ('I b Unit))
-> (a ~> b) -> IntConstruction ('I a Unit) ('I b Unit)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f

isoToInt :: forall {k} (a :: k) b. (TracedMonoidal k) => (a ~> b) -> (b ~> a) -> I a a ~> I b b
isoToInt :: forall {k} (a :: k) (b :: k).
TracedMonoidal k =>
(a ~> b) -> (b ~> a) -> 'I a a ~> 'I b b
isoToInt a ~> b
f b ~> a
g = ((a ** b) ~> (a ** b)) -> IntConstruction ('I a a) ('I b b)
forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k).
(Ob ap, Ob am, Ob bp, Ob bm) =>
((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)
Int (forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
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 :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ~> b
f (a ~> b) -> (b ~> a) -> (a ** b) ~> (b ** a)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` b ~> a
g)) ((Ob a, Ob b) => IntConstruction ('I a a) ('I b b))
-> (a ~> b) -> IntConstruction ('I a a) ('I b b)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f ((Ob b, Ob a) => IntConstruction ('I a a) ('I b b))
-> (b ~> a) -> IntConstruction ('I a a) ('I b b)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b ~> a
g

fromInt :: forall {k} (a :: k) b m. (TracedMonoidal k) => (I a m ~> I b m) -> a ~> b
fromInt :: forall {k} (a :: k) (b :: k) (m :: k).
TracedMonoidal k =>
('I a m ~> 'I b m) -> a ~> b
fromInt (Int (ap ** bm) ~> (am ** bp)
f) = forall {k} (p :: k +-> k) (u :: k) (x :: k) (y :: k).
(TracedMonoidalProfunctor p, Ob x, Ob y, Ob u) =>
p (x ** u) (y ** u) -> p x y
forall (p :: k +-> k) (u :: k) (x :: k) (y :: k).
(TracedMonoidalProfunctor p, Ob x, Ob y, Ob u) =>
p (x ** u) (y ** u) -> p x y
trace @(~>) @m @a @b (forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @m @b ((m ** b) ~> (b ** m))
-> ((a ** m) ~> (m ** b)) -> (a ** m) ~> (b ** m)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ** m) ~> (m ** b)
(ap ** bm) ~> (am ** bp)
f)

instance (TracedMonoidal k) => Profunctor (IntConstruction :: CAT (INT k)) where
  dimap :: forall (c :: INT k) (a :: INT k) (b :: INT k) (d :: INT k).
(c ~> a) -> (b ~> d) -> IntConstruction a b -> IntConstruction c d
dimap = (c ~> a) -> (b ~> d) -> IntConstruction a b -> IntConstruction c d
IntConstruction c a
-> IntConstruction b d
-> IntConstruction a b
-> IntConstruction c d
forall {k} (p :: PRO k k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: INT k) (b :: INT k) r.
((Ob a, Ob b) => r) -> IntConstruction a b -> r
\\ Int{} = r
(Ob a, Ob b) => r
r
instance (TracedMonoidal k) => Promonad (IntConstruction :: CAT (INT k)) where
  id :: forall (a :: INT k). Ob a => IntConstruction a a
id @a = ((IntPlus a ** IntMinus a) ~> (IntMinus a ** IntPlus a))
-> IntConstruction
     ('I (IntPlus a) (IntMinus a)) ('I (IntPlus a) (IntMinus a))
forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k).
(Ob ap, Ob am, Ob bp, Ob bm) =>
((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)
Int (forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @(IntPlus a) @(IntMinus a))
  Int @bp @bm @cp @cm (ap ** bm) ~> (am ** bp)
f . :: forall (b :: INT k) (c :: INT k) (a :: INT k).
IntConstruction b c -> IntConstruction a b -> IntConstruction a c
. Int @ap @am (ap ** bm) ~> (am ** bp)
g =
    ((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)
forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k).
(Ob ap, Ob am, Ob bp, Ob bm) =>
((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)
Int
      ( forall {k} (p :: k +-> k) (u :: k) (x :: k) (y :: k).
(TracedMonoidalProfunctor p, Ob x, Ob y, Ob u) =>
p (x ** u) (y ** u) -> p x y
forall (p :: k +-> k) (u :: k) (x :: k) (y :: k).
(TracedMonoidalProfunctor p, Ob x, Ob y, Ob u) =>
p (x ** u) (y ** u) -> p x y
trace @_ @(bp ** bm) @(ap ** cm) @(am ** cp)
          (forall (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))
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 @bm @cp @bp @am (((am ** bp) ** (ap ** am)) ~> ((am ** bp) ** (ap ** am)))
-> (((ap ** bm) ** (ap ** am)) ~> ((am ** bp) ** (ap ** am)))
-> ((ap ** bm) ** (ap ** am)) ~> ((am ** bp) ** (ap ** am))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((ap ** bm) ~> (am ** bp)
f ((ap ** bm) ~> (am ** bp))
-> ((ap ** am) ~> (ap ** am))
-> ((ap ** bm) ** (ap ** am)) ~> ((am ** bp) ** (ap ** am))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` (forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @am @bp ((am ** ap) ~> (ap ** am))
-> ((ap ** am) ~> (am ** ap)) -> (ap ** am) ~> (ap ** am)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (ap ** am) ~> (am ** ap)
(ap ** bm) ~> (am ** bp)
g)) (((ap ** bm) ** (ap ** am)) ~> ((am ** bp) ** (ap ** am)))
-> (((ap ** bm) ** (ap ** am)) ~> ((ap ** bm) ** (ap ** am)))
-> ((ap ** bm) ** (ap ** am)) ~> ((am ** bp) ** (ap ** am))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((c ** b) ** (a ** d))
forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((c ** b) ** (a ** d))
swapFst @ap @cm @bp @bm)
      )
      ((Ob (ap ** bm), Ob (ap ** bm)) => IntConstruction a c)
-> ((ap ** bm) ~> (ap ** bm)) -> IntConstruction a c
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ 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 @ap @cm
      ((Ob (am ** bp), Ob (am ** bp)) => IntConstruction a c)
-> ((am ** bp) ~> (am ** bp)) -> IntConstruction a c
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ 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 @am @cp
      ((Ob (ap ** am), Ob (ap ** am)) => IntConstruction a c)
-> ((ap ** am) ~> (ap ** am)) -> IntConstruction a c
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ 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 @bp @bm
instance (TracedMonoidal k) => CategoryOf (INT k) where
  type (~>) = IntConstruction
  type Ob a = (a ~ I (IntPlus a) (IntMinus a), Ob (IntPlus a), Ob (IntMinus a))

instance (TracedMonoidal k, Ob (Unit :: k)) => MonoidalProfunctor (IntConstruction :: CAT (INT k)) where
  par0 :: IntConstruction Unit Unit
par0 = ((Unit ** Unit) ~> (Unit ** Unit))
-> IntConstruction ('I Unit Unit) ('I Unit Unit)
forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k).
(Ob ap, Ob am, Ob bp, Ob bm) =>
((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)
Int (forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @Unit @Unit)
  Int @ap @am @bp @bm (ap ** bm) ~> (am ** bp)
f par :: forall (x1 :: INT k) (x2 :: INT k) (y1 :: INT k) (y2 :: INT k).
IntConstruction x1 x2
-> IntConstruction y1 y2 -> IntConstruction (x1 ** y1) (x2 ** y2)
`par` Int @cp @cm @dp @dm (ap ** bm) ~> (am ** bp)
g =
    (((ap ** ap) ** (bm ** bm)) ~> ((am ** am) ** (bp ** bp)))
-> IntConstruction
     ('I (ap ** ap) (am ** am)) ('I (bp ** bp) (bm ** bm))
forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k).
(Ob ap, Ob am, Ob bp, Ob bm) =>
((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)
Int (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 @am @bp @cm @dp (((am ** bp) ** (am ** bp)) ~> ((am ** am) ** (bp ** bp)))
-> (((ap ** ap) ** (bm ** bm)) ~> ((am ** bp) ** (am ** bp)))
-> ((ap ** ap) ** (bm ** bm)) ~> ((am ** am) ** (bp ** bp))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((ap ** bm) ~> (am ** bp)
f ((ap ** bm) ~> (am ** bp))
-> ((ap ** bm) ~> (am ** bp))
-> ((ap ** bm) ** (ap ** bm)) ~> ((am ** bp) ** (am ** bp))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` (ap ** bm) ~> (am ** bp)
g) (((ap ** bm) ** (ap ** bm)) ~> ((am ** bp) ** (am ** bp)))
-> (((ap ** ap) ** (bm ** bm)) ~> ((ap ** bm) ** (ap ** bm)))
-> ((ap ** ap) ** (bm ** bm)) ~> ((am ** bp) ** (am ** bp))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
swapInner @ap @cp @bm @dm)
      ((Ob ('I (ap ** ap) (am ** am)), Ob ('I (ap ** ap) (am ** am))) =>
 IntConstruction
   ('I (ap ** ap) (am ** am)) ('I (bp ** bp) (bm ** bm)))
-> IntConstruction
     ('I (ap ** ap) (am ** am)) ('I (ap ** ap) (am ** am))
-> IntConstruction
     ('I (ap ** ap) (am ** am)) ('I (bp ** bp) (bm ** bm))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: INT k) (b :: INT k) r.
((Ob a, Ob b) => r) -> IntConstruction a b -> r
\\ forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
forall (a :: INT k) (b :: INT k).
(Monoidal (INT k), Ob a, Ob b) =>
Obj (a ** b)
obj2 @(I ap am) @(I cp cm)
      ((Ob ('I (bp ** bp) (bm ** bm)), Ob ('I (bp ** bp) (bm ** bm))) =>
 IntConstruction
   ('I (ap ** ap) (am ** am)) ('I (bp ** bp) (bm ** bm)))
-> IntConstruction
     ('I (bp ** bp) (bm ** bm)) ('I (bp ** bp) (bm ** bm))
-> IntConstruction
     ('I (ap ** ap) (am ** am)) ('I (bp ** bp) (bm ** bm))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: INT k) (b :: INT k) r.
((Ob a, Ob b) => r) -> IntConstruction a b -> r
\\ forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
forall (a :: INT k) (b :: INT k).
(Monoidal (INT k), Ob a, Ob b) =>
Obj (a ** b)
obj2 @(I bp bm) @(I dp dm)

instance (TracedMonoidal k, Ob (Unit :: k)) => Monoidal (INT k) where
  type Unit = I Unit Unit
  type a ** b = I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b)
  leftUnitor :: forall (a :: INT k). Ob a => (Unit ** a) ~> a
leftUnitor @(I ap am) =
    (((Unit ** IntPlus a) ** IntMinus a)
 ~> ((Unit ** IntMinus a) ** IntPlus a))
-> IntConstruction
     ('I (Unit ** IntPlus a) (Unit ** IntMinus a))
     ('I (IntPlus a) (IntMinus a))
forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k).
(Ob ap, Ob am, Ob bp, Ob bm) =>
((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)
Int ((forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @k @am (IntMinus a ~> (Unit ** IntMinus a))
-> (IntPlus a ~> IntPlus a)
-> (IntMinus a ** IntPlus a) ~> ((Unit ** IntMinus a) ** IntPlus a)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @ap) ((IntMinus a ** IntPlus a) ~> ((Unit ** IntMinus a) ** IntPlus a))
-> (((Unit ** IntPlus a) ** IntMinus a)
    ~> (IntMinus a ** IntPlus a))
-> ((Unit ** IntPlus a) ** IntMinus a)
   ~> ((Unit ** IntMinus a) ** IntPlus a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @ap @am ((IntPlus a ** IntMinus a) ~> (IntMinus a ** IntPlus a))
-> (((Unit ** IntPlus a) ** IntMinus a)
    ~> (IntPlus a ** IntMinus a))
-> ((Unit ** IntPlus a) ** IntMinus a) ~> (IntMinus a ** IntPlus a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @k @ap ((Unit ** IntPlus a) ~> IntPlus a)
-> (IntMinus a ~> IntMinus a)
-> ((Unit ** IntPlus a) ** IntMinus a) ~> (IntPlus a ** IntMinus a)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @am))
      ((Ob (Unit ** IntPlus a), Ob (Unit ** IntPlus a)) =>
 IntConstruction
   ('I (Unit ** IntPlus a) (Unit ** IntMinus a))
   ('I (IntPlus a) (IntMinus a)))
-> ((Unit ** IntPlus a) ~> (Unit ** IntPlus a))
-> IntConstruction
     ('I (Unit ** IntPlus a) (Unit ** IntMinus a))
     ('I (IntPlus a) (IntMinus a))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ 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 @Unit @ap
      ((Ob (Unit ** IntMinus a), Ob (Unit ** IntMinus a)) =>
 IntConstruction
   ('I (Unit ** IntPlus a) (Unit ** IntMinus a))
   ('I (IntPlus a) (IntMinus a)))
-> ((Unit ** IntMinus a) ~> (Unit ** IntMinus a))
-> IntConstruction
     ('I (Unit ** IntPlus a) (Unit ** IntMinus a))
     ('I (IntPlus a) (IntMinus a))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ 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 @Unit @am
  leftUnitorInv :: forall (a :: INT k). Ob a => a ~> (Unit ** a)
leftUnitorInv @(I ap am) =
    ((IntPlus a ** (Unit ** IntMinus a))
 ~> (IntMinus a ** (Unit ** IntPlus a)))
-> IntConstruction
     ('I (IntPlus a) (IntMinus a))
     ('I (Unit ** IntPlus a) (Unit ** IntMinus a))
forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k).
(Ob ap, Ob am, Ob bp, Ob bm) =>
((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)
Int ((forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @am Obj (IntMinus a)
-> (IntPlus a ~> (Unit ** IntPlus a))
-> (IntMinus a ** IntPlus a) ~> (IntMinus a ** (Unit ** IntPlus a))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @k @ap) ((IntMinus a ** IntPlus a) ~> (IntMinus a ** (Unit ** IntPlus a)))
-> ((IntPlus a ** (Unit ** IntMinus a))
    ~> (IntMinus a ** IntPlus a))
-> (IntPlus a ** (Unit ** IntMinus a))
   ~> (IntMinus a ** (Unit ** IntPlus a))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @ap @am ((IntPlus a ** IntMinus a) ~> (IntMinus a ** IntPlus a))
-> ((IntPlus a ** (Unit ** IntMinus a))
    ~> (IntPlus a ** IntMinus a))
-> (IntPlus a ** (Unit ** IntMinus a)) ~> (IntMinus a ** IntPlus a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @ap Obj (IntPlus a)
-> ((Unit ** IntMinus a) ~> IntMinus a)
-> (IntPlus a ** (Unit ** IntMinus a)) ~> (IntPlus a ** IntMinus a)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @k @am))
      ((Ob (Unit ** IntPlus a), Ob (Unit ** IntPlus a)) =>
 IntConstruction
   ('I (IntPlus a) (IntMinus a))
   ('I (Unit ** IntPlus a) (Unit ** IntMinus a)))
-> ((Unit ** IntPlus a) ~> (Unit ** IntPlus a))
-> IntConstruction
     ('I (IntPlus a) (IntMinus a))
     ('I (Unit ** IntPlus a) (Unit ** IntMinus a))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ 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 @Unit @ap
      ((Ob (Unit ** IntMinus a), Ob (Unit ** IntMinus a)) =>
 IntConstruction
   ('I (IntPlus a) (IntMinus a))
   ('I (Unit ** IntPlus a) (Unit ** IntMinus a)))
-> ((Unit ** IntMinus a) ~> (Unit ** IntMinus a))
-> IntConstruction
     ('I (IntPlus a) (IntMinus a))
     ('I (Unit ** IntPlus a) (Unit ** IntMinus a))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ 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 @Unit @am
  rightUnitor :: forall (a :: INT k). Ob a => (a ** Unit) ~> a
rightUnitor @(I ap am) =
    (((IntPlus a ** Unit) ** IntMinus a)
 ~> ((IntMinus a ** Unit) ** IntPlus a))
-> IntConstruction
     ('I (IntPlus a ** Unit) (IntMinus a ** Unit))
     ('I (IntPlus a) (IntMinus a))
forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k).
(Ob ap, Ob am, Ob bp, Ob bm) =>
((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)
Int ((forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv @k @am (IntMinus a ~> (IntMinus a ** Unit))
-> (IntPlus a ~> IntPlus a)
-> (IntMinus a ** IntPlus a) ~> ((IntMinus a ** Unit) ** IntPlus a)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @ap) ((IntMinus a ** IntPlus a) ~> ((IntMinus a ** Unit) ** IntPlus a))
-> (((IntPlus a ** Unit) ** IntMinus a)
    ~> (IntMinus a ** IntPlus a))
-> ((IntPlus a ** Unit) ** IntMinus a)
   ~> ((IntMinus a ** Unit) ** IntPlus a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @ap @am ((IntPlus a ** IntMinus a) ~> (IntMinus a ** IntPlus a))
-> (((IntPlus a ** Unit) ** IntMinus a)
    ~> (IntPlus a ** IntMinus a))
-> ((IntPlus a ** Unit) ** IntMinus a) ~> (IntMinus a ** IntPlus a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor @k @ap ((IntPlus a ** Unit) ~> IntPlus a)
-> (IntMinus a ~> IntMinus a)
-> ((IntPlus a ** Unit) ** IntMinus a) ~> (IntPlus a ** IntMinus a)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @am))
      ((Ob (IntPlus a ** Unit), Ob (IntPlus a ** Unit)) =>
 IntConstruction
   ('I (IntPlus a ** Unit) (IntMinus a ** Unit))
   ('I (IntPlus a) (IntMinus a)))
-> ((IntPlus a ** Unit) ~> (IntPlus a ** Unit))
-> IntConstruction
     ('I (IntPlus a ** Unit) (IntMinus a ** Unit))
     ('I (IntPlus a) (IntMinus a))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ 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 @ap @Unit
      ((Ob (IntMinus a ** Unit), Ob (IntMinus a ** Unit)) =>
 IntConstruction
   ('I (IntPlus a ** Unit) (IntMinus a ** Unit))
   ('I (IntPlus a) (IntMinus a)))
-> ((IntMinus a ** Unit) ~> (IntMinus a ** Unit))
-> IntConstruction
     ('I (IntPlus a ** Unit) (IntMinus a ** Unit))
     ('I (IntPlus a) (IntMinus a))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ 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 @am @Unit
  rightUnitorInv :: forall (a :: INT k). Ob a => a ~> (a ** Unit)
rightUnitorInv @(I ap am) =
    ((IntPlus a ** (IntMinus a ** Unit))
 ~> (IntMinus a ** (IntPlus a ** Unit)))
-> IntConstruction
     ('I (IntPlus a) (IntMinus a))
     ('I (IntPlus a ** Unit) (IntMinus a ** Unit))
forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k).
(Ob ap, Ob am, Ob bp, Ob bm) =>
((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)
Int ((forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @am Obj (IntMinus a)
-> (IntPlus a ~> (IntPlus a ** Unit))
-> (IntMinus a ** IntPlus a) ~> (IntMinus a ** (IntPlus a ** Unit))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv @k @ap) ((IntMinus a ** IntPlus a) ~> (IntMinus a ** (IntPlus a ** Unit)))
-> ((IntPlus a ** (IntMinus a ** Unit))
    ~> (IntMinus a ** IntPlus a))
-> (IntPlus a ** (IntMinus a ** Unit))
   ~> (IntMinus a ** (IntPlus a ** Unit))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @ap @am ((IntPlus a ** IntMinus a) ~> (IntMinus a ** IntPlus a))
-> ((IntPlus a ** (IntMinus a ** Unit))
    ~> (IntPlus a ** IntMinus a))
-> (IntPlus a ** (IntMinus a ** Unit)) ~> (IntMinus a ** IntPlus a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @ap Obj (IntPlus a)
-> ((IntMinus a ** Unit) ~> IntMinus a)
-> (IntPlus a ** (IntMinus a ** Unit)) ~> (IntPlus a ** IntMinus a)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor @k @am))
      ((Ob (IntPlus a ** Unit), Ob (IntPlus a ** Unit)) =>
 IntConstruction
   ('I (IntPlus a) (IntMinus a))
   ('I (IntPlus a ** Unit) (IntMinus a ** Unit)))
-> ((IntPlus a ** Unit) ~> (IntPlus a ** Unit))
-> IntConstruction
     ('I (IntPlus a) (IntMinus a))
     ('I (IntPlus a ** Unit) (IntMinus a ** Unit))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ 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 @ap @Unit
      ((Ob (IntMinus a ** Unit), Ob (IntMinus a ** Unit)) =>
 IntConstruction
   ('I (IntPlus a) (IntMinus a))
   ('I (IntPlus a ** Unit) (IntMinus a ** Unit)))
-> ((IntMinus a ** Unit) ~> (IntMinus a ** Unit))
-> IntConstruction
     ('I (IntPlus a) (IntMinus a))
     ('I (IntPlus a ** Unit) (IntMinus a ** Unit))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ 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 @am @Unit
  associator :: forall (a :: INT k) (b :: INT k) (c :: INT k).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(I ap am) @(I bp bm) @(I cp cm) =
    ((((IntPlus a ** IntPlus b) ** IntPlus c)
  ** (IntMinus a ** (IntMinus b ** IntMinus c)))
 ~> (((IntMinus a ** IntMinus b) ** IntMinus c)
     ** (IntPlus a ** (IntPlus b ** IntPlus c))))
-> IntConstruction
     ('I
        ((IntPlus a ** IntPlus b) ** IntPlus c)
        ((IntMinus a ** IntMinus b) ** IntMinus c))
     ('I
        (IntPlus a ** (IntPlus b ** IntPlus c))
        (IntMinus a ** (IntMinus b ** IntMinus c)))
forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k).
(Ob ap, Ob am, Ob bp, Ob bm) =>
((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)
Int (forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @(ap ** (bp ** cp)) @((am ** bm) ** cm) (((IntPlus a ** (IntPlus b ** IntPlus c))
  ** ((IntMinus a ** IntMinus b) ** IntMinus c))
 ~> (((IntMinus a ** IntMinus b) ** IntMinus c)
     ** (IntPlus a ** (IntPlus b ** IntPlus c))))
-> ((((IntPlus a ** IntPlus b) ** IntPlus c)
     ** (IntMinus a ** (IntMinus b ** IntMinus c)))
    ~> ((IntPlus a ** (IntPlus b ** IntPlus c))
        ** ((IntMinus a ** IntMinus b) ** IntMinus c)))
-> (((IntPlus a ** IntPlus b) ** IntPlus c)
    ** (IntMinus a ** (IntMinus b ** IntMinus c)))
   ~> (((IntMinus a ** IntMinus b) ** IntMinus c)
       ** (IntPlus a ** (IntPlus b ** IntPlus c)))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @ap @bp @cp (((IntPlus a ** IntPlus b) ** IntPlus c)
 ~> (IntPlus a ** (IntPlus b ** IntPlus c)))
-> ((IntMinus a ** (IntMinus b ** IntMinus c))
    ~> ((IntMinus a ** IntMinus b) ** IntMinus c))
-> (((IntPlus a ** IntPlus b) ** IntPlus c)
    ** (IntMinus a ** (IntMinus b ** IntMinus c)))
   ~> ((IntPlus a ** (IntPlus b ** IntPlus c))
       ** ((IntMinus a ** IntMinus b) ** IntMinus c))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @am @bm @cm))
      ((Ob
    ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b)
     ** 'I (IntPlus c) (IntMinus c)),
  Ob
    ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b)
     ** 'I (IntPlus c) (IntMinus c))) =>
 IntConstruction
   ('I
      ((IntPlus a ** IntPlus b) ** IntPlus c)
      ((IntMinus a ** IntMinus b) ** IntMinus c))
   ('I
      (IntPlus a ** (IntPlus b ** IntPlus c))
      (IntMinus a ** (IntMinus b ** IntMinus c))))
-> IntConstruction
     ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b)
      ** 'I (IntPlus c) (IntMinus c))
     ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b)
      ** 'I (IntPlus c) (IntMinus c))
-> IntConstruction
     ('I
        ((IntPlus a ** IntPlus b) ** IntPlus c)
        ((IntMinus a ** IntMinus b) ** IntMinus c))
     ('I
        (IntPlus a ** (IntPlus b ** IntPlus c))
        (IntMinus a ** (IntMinus b ** IntMinus c)))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: INT k) (b :: INT k) r.
((Ob a, Ob b) => r) -> IntConstruction a b -> r
\\ forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
forall (a :: INT k) (b :: INT k).
(Monoidal (INT k), Ob a, Ob b) =>
Obj (a ** b)
obj2 @(I ap am) @(I bp bm) IntConstruction
  ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b))
  ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b))
-> IntConstruction
     ('I (IntPlus c) (IntMinus c)) ('I (IntPlus c) (IntMinus c))
-> IntConstruction
     ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b)
      ** 'I (IntPlus c) (IntMinus c))
     ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b)
      ** 'I (IntPlus c) (IntMinus c))
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 (x1 :: INT k) (x2 :: INT k) (y1 :: INT k) (y2 :: INT k).
IntConstruction x1 x2
-> IntConstruction y1 y2 -> IntConstruction (x1 ** y1) (x2 ** y2)
`par` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: INT k). (CategoryOf (INT k), Ob a) => Obj a
obj @(I cp cm)
      ((Ob
    ('I (IntPlus a) (IntMinus a)
     ** 'I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c)),
  Ob
    ('I (IntPlus a) (IntMinus a)
     ** 'I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c))) =>
 IntConstruction
   ('I
      ((IntPlus a ** IntPlus b) ** IntPlus c)
      ((IntMinus a ** IntMinus b) ** IntMinus c))
   ('I
      (IntPlus a ** (IntPlus b ** IntPlus c))
      (IntMinus a ** (IntMinus b ** IntMinus c))))
-> IntConstruction
     ('I (IntPlus a) (IntMinus a)
      ** 'I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c))
     ('I (IntPlus a) (IntMinus a)
      ** 'I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c))
-> IntConstruction
     ('I
        ((IntPlus a ** IntPlus b) ** IntPlus c)
        ((IntMinus a ** IntMinus b) ** IntMinus c))
     ('I
        (IntPlus a ** (IntPlus b ** IntPlus c))
        (IntMinus a ** (IntMinus b ** IntMinus c)))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: INT k) (b :: INT k) r.
((Ob a, Ob b) => r) -> IntConstruction a b -> r
\\ forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: INT k). (CategoryOf (INT k), Ob a) => Obj a
obj @(I ap am) IntConstruction
  ('I (IntPlus a) (IntMinus a)) ('I (IntPlus a) (IntMinus a))
-> IntConstruction
     ('I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c))
     ('I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c))
-> IntConstruction
     ('I (IntPlus a) (IntMinus a)
      ** 'I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c))
     ('I (IntPlus a) (IntMinus a)
      ** 'I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c))
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 (x1 :: INT k) (x2 :: INT k) (y1 :: INT k) (y2 :: INT k).
IntConstruction x1 x2
-> IntConstruction y1 y2 -> IntConstruction (x1 ** y1) (x2 ** y2)
`par` forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
forall (a :: INT k) (b :: INT k).
(Monoidal (INT k), Ob a, Ob b) =>
Obj (a ** b)
obj2 @(I bp bm) @(I cp cm)
  associatorInv :: forall (a :: INT k) (b :: INT k) (c :: INT k).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(I ap am) @(I bp bm) @(I cp cm) =
    (((IntPlus a ** (IntPlus b ** IntPlus c))
  ** ((IntMinus a ** IntMinus b) ** IntMinus c))
 ~> ((IntMinus a ** (IntMinus b ** IntMinus c))
     ** ((IntPlus a ** IntPlus b) ** IntPlus c)))
-> IntConstruction
     ('I
        (IntPlus a ** (IntPlus b ** IntPlus c))
        (IntMinus a ** (IntMinus b ** IntMinus c)))
     ('I
        ((IntPlus a ** IntPlus b) ** IntPlus c)
        ((IntMinus a ** IntMinus b) ** IntMinus c))
forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k).
(Ob ap, Ob am, Ob bp, Ob bm) =>
((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)
Int (forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @((ap ** bp) ** cp) @(am ** (bm ** cm)) ((((IntPlus a ** IntPlus b) ** IntPlus c)
  ** (IntMinus a ** (IntMinus b ** IntMinus c)))
 ~> ((IntMinus a ** (IntMinus b ** IntMinus c))
     ** ((IntPlus a ** IntPlus b) ** IntPlus c)))
-> (((IntPlus a ** (IntPlus b ** IntPlus c))
     ** ((IntMinus a ** IntMinus b) ** IntMinus c))
    ~> (((IntPlus a ** IntPlus b) ** IntPlus c)
        ** (IntMinus a ** (IntMinus b ** IntMinus c))))
-> ((IntPlus a ** (IntPlus b ** IntPlus c))
    ** ((IntMinus a ** IntMinus b) ** IntMinus c))
   ~> ((IntMinus a ** (IntMinus b ** IntMinus c))
       ** ((IntPlus a ** IntPlus b) ** IntPlus c))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @ap @bp @cp ((IntPlus a ** (IntPlus b ** IntPlus c))
 ~> ((IntPlus a ** IntPlus b) ** IntPlus c))
-> (((IntMinus a ** IntMinus b) ** IntMinus c)
    ~> (IntMinus a ** (IntMinus b ** IntMinus c)))
-> ((IntPlus a ** (IntPlus b ** IntPlus c))
    ** ((IntMinus a ** IntMinus b) ** IntMinus c))
   ~> (((IntPlus a ** IntPlus b) ** IntPlus c)
       ** (IntMinus a ** (IntMinus b ** IntMinus c)))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @am @bm @cm))
      ((Ob
    ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b)
     ** 'I (IntPlus c) (IntMinus c)),
  Ob
    ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b)
     ** 'I (IntPlus c) (IntMinus c))) =>
 IntConstruction
   ('I
      (IntPlus a ** (IntPlus b ** IntPlus c))
      (IntMinus a ** (IntMinus b ** IntMinus c)))
   ('I
      ((IntPlus a ** IntPlus b) ** IntPlus c)
      ((IntMinus a ** IntMinus b) ** IntMinus c)))
-> IntConstruction
     ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b)
      ** 'I (IntPlus c) (IntMinus c))
     ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b)
      ** 'I (IntPlus c) (IntMinus c))
-> IntConstruction
     ('I
        (IntPlus a ** (IntPlus b ** IntPlus c))
        (IntMinus a ** (IntMinus b ** IntMinus c)))
     ('I
        ((IntPlus a ** IntPlus b) ** IntPlus c)
        ((IntMinus a ** IntMinus b) ** IntMinus c))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: INT k) (b :: INT k) r.
((Ob a, Ob b) => r) -> IntConstruction a b -> r
\\ forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
forall (a :: INT k) (b :: INT k).
(Monoidal (INT k), Ob a, Ob b) =>
Obj (a ** b)
obj2 @(I ap am) @(I bp bm) IntConstruction
  ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b))
  ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b))
-> IntConstruction
     ('I (IntPlus c) (IntMinus c)) ('I (IntPlus c) (IntMinus c))
-> IntConstruction
     ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b)
      ** 'I (IntPlus c) (IntMinus c))
     ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b)
      ** 'I (IntPlus c) (IntMinus c))
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 (x1 :: INT k) (x2 :: INT k) (y1 :: INT k) (y2 :: INT k).
IntConstruction x1 x2
-> IntConstruction y1 y2 -> IntConstruction (x1 ** y1) (x2 ** y2)
`par` forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: INT k). (CategoryOf (INT k), Ob a) => Obj a
obj @(I cp cm)
      ((Ob
    ('I (IntPlus a) (IntMinus a)
     ** 'I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c)),
  Ob
    ('I (IntPlus a) (IntMinus a)
     ** 'I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c))) =>
 IntConstruction
   ('I
      (IntPlus a ** (IntPlus b ** IntPlus c))
      (IntMinus a ** (IntMinus b ** IntMinus c)))
   ('I
      ((IntPlus a ** IntPlus b) ** IntPlus c)
      ((IntMinus a ** IntMinus b) ** IntMinus c)))
-> IntConstruction
     ('I (IntPlus a) (IntMinus a)
      ** 'I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c))
     ('I (IntPlus a) (IntMinus a)
      ** 'I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c))
-> IntConstruction
     ('I
        (IntPlus a ** (IntPlus b ** IntPlus c))
        (IntMinus a ** (IntMinus b ** IntMinus c)))
     ('I
        ((IntPlus a ** IntPlus b) ** IntPlus c)
        ((IntMinus a ** IntMinus b) ** IntMinus c))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: INT k) (b :: INT k) r.
((Ob a, Ob b) => r) -> IntConstruction a b -> r
\\ forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: INT k). (CategoryOf (INT k), Ob a) => Obj a
obj @(I ap am) IntConstruction
  ('I (IntPlus a) (IntMinus a)) ('I (IntPlus a) (IntMinus a))
-> IntConstruction
     ('I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c))
     ('I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c))
-> IntConstruction
     ('I (IntPlus a) (IntMinus a)
      ** 'I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c))
     ('I (IntPlus a) (IntMinus a)
      ** 'I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c))
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 (x1 :: INT k) (x2 :: INT k) (y1 :: INT k) (y2 :: INT k).
IntConstruction x1 x2
-> IntConstruction y1 y2 -> IntConstruction (x1 ** y1) (x2 ** y2)
`par` forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
forall (a :: INT k) (b :: INT k).
(Monoidal (INT k), Ob a, Ob b) =>
Obj (a ** b)
obj2 @(I bp bm) @(I cp cm)

instance (TracedMonoidal k, Ob (Unit :: k)) => SymMonoidal (INT k) where
  Int @ap @am @bp @bm (ap ** bm) ~> (am ** bp)
f swap' :: forall (a :: INT k) (a' :: INT k) (b :: INT k) (b' :: INT k).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
`swap'` Int @cp @cm @dp @dm (ap ** bm) ~> (am ** bp)
g =
    (((ap ** ap) ** (bm ** bm)) ~> ((am ** am) ** (bp ** bp)))
-> IntConstruction
     ('I (ap ** ap) (am ** am)) ('I (bp ** bp) (bm ** bm))
forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k).
(Ob ap, Ob am, Ob bp, Ob bm) =>
((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)
Int (forall (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))
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 @am @bp @dp @cm (((am ** bp) ** (bp ** am)) ~> ((am ** am) ** (bp ** bp)))
-> (((ap ** ap) ** (bm ** bm)) ~> ((am ** bp) ** (bp ** am)))
-> ((ap ** ap) ** (bm ** bm)) ~> ((am ** am) ** (bp ** bp))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((ap ** bm) ~> (am ** bp)
f ((ap ** bm) ~> (am ** bp))
-> ((bm ** ap) ~> (bp ** am))
-> ((ap ** bm) ** (bm ** ap)) ~> ((am ** bp) ** (bp ** am))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` (forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @cm @dp ((am ** bp) ~> (bp ** am))
-> ((bm ** ap) ~> (am ** bp)) -> (bm ** ap) ~> (bp ** am)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (ap ** bm) ~> (am ** bp)
g ((ap ** bm) ~> (am ** bp))
-> ((bm ** ap) ~> (ap ** bm)) -> (bm ** ap) ~> (am ** bp)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @dm @cp)) (((ap ** bm) ** (bm ** ap)) ~> ((am ** bp) ** (bp ** am)))
-> (((ap ** ap) ** (bm ** bm)) ~> ((ap ** bm) ** (bm ** ap)))
-> ((ap ** ap) ** (bm ** bm)) ~> ((am ** bp) ** (bp ** am))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** d) ** (c ** b))
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 @ap @cp @dm @bm)
      ((Ob ('I (ap ** ap) (am ** am)), Ob ('I (ap ** ap) (am ** am))) =>
 IntConstruction
   ('I (ap ** ap) (am ** am)) ('I (bp ** bp) (bm ** bm)))
-> IntConstruction
     ('I (ap ** ap) (am ** am)) ('I (ap ** ap) (am ** am))
-> IntConstruction
     ('I (ap ** ap) (am ** am)) ('I (bp ** bp) (bm ** bm))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: INT k) (b :: INT k) r.
((Ob a, Ob b) => r) -> IntConstruction a b -> r
\\ forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
forall (a :: INT k) (b :: INT k).
(Monoidal (INT k), Ob a, Ob b) =>
Obj (a ** b)
obj2 @(I ap am) @(I cp cm)
      ((Ob ('I (bp ** bp) (bm ** bm)), Ob ('I (bp ** bp) (bm ** bm))) =>
 IntConstruction
   ('I (ap ** ap) (am ** am)) ('I (bp ** bp) (bm ** bm)))
-> IntConstruction
     ('I (bp ** bp) (bm ** bm)) ('I (bp ** bp) (bm ** bm))
-> IntConstruction
     ('I (ap ** ap) (am ** am)) ('I (bp ** bp) (bm ** bm))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: INT k) (b :: INT k) r.
((Ob a, Ob b) => r) -> IntConstruction a b -> r
\\ forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
forall (a :: INT k) (b :: INT k).
(Monoidal (INT k), Ob a, Ob b) =>
Obj (a ** b)
obj2 @(I dp dm) @(I bp bm)

instance (TracedMonoidal k, Ob (Unit :: k)) => Closed (INT k) where
  type a ~~> b = ExpSA a b
  curry' :: forall (a :: INT k) (b :: INT k) (c :: INT k).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' @a @b @c Int{} Int{} = forall {k} (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpSA b c
forall (a :: INT k) (b :: INT k) (c :: INT k).
(StarAutonomous (INT k), Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpSA b c
currySA @a @b @c
  uncurry' :: forall (b :: INT k) (c :: INT k) (a :: INT k).
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' @b @c Int{} Int{} = forall {k} (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob b, Ob c) =>
(a ~> ExpSA b c) -> (a ** b) ~> c
forall (a :: INT k) (b :: INT k) (c :: INT k).
(StarAutonomous (INT k), Ob b, Ob c) =>
(a ~> ExpSA b c) -> (a ** b) ~> c
uncurrySA @_ @b @c
  ^^^ :: forall (b :: INT k) (y :: INT k) (x :: INT k) (a :: INT k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
(^^^) = (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
(b ~> y) -> (x ~> a) -> ExpSA a b ~> ExpSA x y
forall {k} (a :: k) (b :: k) (x :: k) (y :: k).
StarAutonomous k =>
(b ~> y) -> (x ~> a) -> ExpSA a b ~> ExpSA x y
expSA

instance (TracedMonoidal k, Ob (Unit :: k)) => StarAutonomous (INT k) where
  type Dual (I p n) = I n p
  dual :: forall (a :: INT k) (b :: INT k). (a ~> b) -> Dual b ~> Dual a
dual (Int @ap @am @bp @bm (ap ** bm) ~> (am ** bp)
f) = ((bm ** ap) ~> (bp ** am)) -> IntConstruction ('I bm bp) ('I am ap)
forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k).
(Ob ap, Ob am, Ob bp, Ob bm) =>
((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)
Int (forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @am @bp ((am ** bp) ~> (bp ** am))
-> ((bm ** ap) ~> (am ** bp)) -> (bm ** ap) ~> (bp ** am)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (ap ** bm) ~> (am ** bp)
f ((ap ** bm) ~> (am ** bp))
-> ((bm ** ap) ~> (ap ** bm)) -> (bm ** ap) ~> (am ** bp)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @bm @ap)
  dualInv :: forall (a :: INT k) (b :: INT k).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv (Int @ap @am @bp @bm (ap ** bm) ~> (am ** bp)
f) = ((IntPlus b ** IntMinus a) ~> (IntMinus b ** IntPlus a))
-> IntConstruction
     ('I (IntPlus b) (IntMinus b)) ('I (IntPlus a) (IntMinus a))
forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k).
(Ob ap, Ob am, Ob bp, Ob bm) =>
((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)
Int (forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @am @bp ((IntPlus a ** IntMinus b) ~> (IntMinus b ** IntPlus a))
-> ((IntPlus b ** IntMinus a) ~> (IntPlus a ** IntMinus b))
-> (IntPlus b ** IntMinus a) ~> (IntMinus b ** IntPlus a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (ap ** bm) ~> (am ** bp)
(IntMinus a ** IntPlus b) ~> (IntPlus a ** IntMinus b)
f ((IntMinus a ** IntPlus b) ~> (IntPlus a ** IntMinus b))
-> ((IntPlus b ** IntMinus a) ~> (IntMinus a ** IntPlus b))
-> (IntPlus b ** IntMinus a) ~> (IntPlus a ** IntMinus b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @bm @ap)
  linDist :: forall (a :: INT k) (b :: INT k) (c :: INT k).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @(I ap am) @(I bp bm) @(I cp cm) (Int (ap ** bm) ~> (am ** bp)
f) = ((IntPlus a ** (IntPlus b ** IntPlus c))
 ~> (IntMinus a ** (IntMinus b ** IntMinus c)))
-> IntConstruction
     ('I (IntPlus a) (IntMinus a))
     ('I (IntMinus b ** IntMinus c) (IntPlus b ** IntPlus c))
forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k).
(Ob ap, Ob am, Ob bp, Ob bm) =>
((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)
Int (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @am @bm @cm ((am ** IntMinus c) ~> (IntMinus a ** (IntMinus b ** IntMinus c)))
-> ((IntPlus a ** (IntPlus b ** IntPlus c)) ~> (am ** IntMinus c))
-> (IntPlus a ** (IntPlus b ** IntPlus c))
   ~> (IntMinus a ** (IntMinus b ** IntMinus c))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (ap ** bm) ~> (am ** bp)
(ap ** IntPlus c) ~> (am ** IntMinus c)
f ((ap ** IntPlus c) ~> (am ** IntMinus c))
-> ((IntPlus a ** (IntPlus b ** IntPlus c)) ~> (ap ** IntPlus c))
-> (IntPlus a ** (IntPlus b ** IntPlus c)) ~> (am ** IntMinus c)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @ap @bp @cp) ((Ob ('I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c)),
  Ob ('I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c))) =>
 IntConstruction
   ('I (IntPlus a) (IntMinus a))
   ('I (IntMinus b ** IntMinus c) (IntPlus b ** IntPlus c)))
-> IntConstruction
     ('I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c))
     ('I (IntPlus b ** IntPlus c) (IntMinus b ** IntMinus c))
-> IntConstruction
     ('I (IntPlus a) (IntMinus a))
     ('I (IntMinus b ** IntMinus c) (IntPlus b ** IntPlus c))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: INT k) (b :: INT k) r.
((Ob a, Ob b) => r) -> IntConstruction a b -> r
\\ forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
forall (a :: INT k) (b :: INT k).
(Monoidal (INT k), Ob a, Ob b) =>
Obj (a ** b)
obj2 @(I bp bm) @(I cp cm)
  linDistInv :: forall (a :: INT k) (b :: INT k) (c :: INT k).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @(I ap am) @(I bp bm) @(I cp cm) (Int (ap ** bm) ~> (am ** bp)
f) = (((IntPlus a ** IntPlus b) ** IntPlus c)
 ~> ((IntMinus a ** IntMinus b) ** IntMinus c))
-> IntConstruction
     ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b))
     ('I (IntMinus c) (IntPlus c))
forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k).
(Ob ap, Ob am, Ob bp, Ob bm) =>
((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)
Int (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @am @bm @cm ((IntMinus a ** bp) ~> ((IntMinus a ** IntMinus b) ** IntMinus c))
-> (((IntPlus a ** IntPlus b) ** IntPlus c) ~> (IntMinus a ** bp))
-> ((IntPlus a ** IntPlus b) ** IntPlus c)
   ~> ((IntMinus a ** IntMinus b) ** IntMinus c)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (ap ** bm) ~> (am ** bp)
(IntPlus a ** bm) ~> (IntMinus a ** bp)
f ((IntPlus a ** bm) ~> (IntMinus a ** bp))
-> (((IntPlus a ** IntPlus b) ** IntPlus c) ~> (IntPlus a ** bm))
-> ((IntPlus a ** IntPlus b) ** IntPlus c) ~> (IntMinus a ** bp)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @ap @bp @cp) ((Ob ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b)),
  Ob ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b))) =>
 IntConstruction
   ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b))
   ('I (IntMinus c) (IntPlus c)))
-> IntConstruction
     ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b))
     ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b))
-> IntConstruction
     ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b))
     ('I (IntMinus c) (IntPlus c))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: INT k) (b :: INT k) r.
((Ob a, Ob b) => r) -> IntConstruction a b -> r
\\ forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
forall (a :: INT k) (b :: INT k).
(Monoidal (INT k), Ob a, Ob b) =>
Obj (a ** b)
obj2 @(I ap am) @(I bp bm)

instance (TracedMonoidal k, Ob (Unit :: k)) => CompactClosed (INT k) where
  distribDual :: forall (a :: INT k) (b :: INT k).
(Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual @(I ap am) @(I bp bm) = (((IntMinus a ** IntMinus b) ** (IntPlus a ** IntPlus b))
 ~> ((IntPlus a ** IntPlus b) ** (IntMinus a ** IntMinus b)))
-> IntConstruction
     ('I (IntMinus a ** IntMinus b) (IntPlus a ** IntPlus b))
     ('I (IntMinus a ** IntMinus b) (IntPlus a ** IntPlus b))
forall {k} (ap :: k) (am :: k) (bp :: k) (bm :: k).
(Ob ap, Ob am, Ob bp, Ob bm) =>
((ap ** bm) ~> (am ** bp)) -> IntConstruction ('I ap am) ('I bp bm)
Int (forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @(am ** bm) @(ap ** bp)) ((Ob ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b)),
  Ob ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b))) =>
 IntConstruction
   ('I (IntMinus a ** IntMinus b) (IntPlus a ** IntPlus b))
   ('I (IntMinus a ** IntMinus b) (IntPlus a ** IntPlus b)))
-> IntConstruction
     ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b))
     ('I (IntPlus a ** IntPlus b) (IntMinus a ** IntMinus b))
-> IntConstruction
     ('I (IntMinus a ** IntMinus b) (IntPlus a ** IntPlus b))
     ('I (IntMinus a ** IntMinus b) (IntPlus a ** IntPlus b))
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: INT k) (b :: INT k) r.
((Ob a, Ob b) => r) -> IntConstruction a b -> r
\\ forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
forall (a :: INT k) (b :: INT k).
(Monoidal (INT k), Ob a, Ob b) =>
Obj (a ** b)
obj2 @(I ap am) @(I bp bm)
  dualUnit :: Dual Unit ~> Unit
dualUnit = Dual Unit ~> Unit
IntConstruction ('I Unit Unit) ('I Unit Unit)
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: INT k). Ob a => IntConstruction a a
id