{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RequiredTypeArguments #-}
{-# OPTIONS_GHC -Wno-unused-foralls #-}

module Proarrow.Category.Monoidal.CompactClosed where

import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , SymMonoidal (..)
  , associator
  , leftUnitorWith
  , rightUnitorWith
  , swap
  , unitObj
  )
import Proarrow.Category.Monoidal.Action (Act, MonoidalAction (..), actHom)
import Proarrow.Category.Monoidal.StarAutonomous
  ( StarAutonomous (..)
  , doubleNeg
  , dualObj
  , dualityCounitSA
  , dualityUnitSA
  )
import Proarrow.Category.Monoidal.Strictified (Strictified (..), obj1, swap2, (==))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj, (//), type (+->))

class (StarAutonomous k, SymMonoidal k) => CompactClosed k where
  distribDual :: forall (a :: k) b. (Ob a, Ob b) => Dual (a ** b) ~> Dual a ** Dual b
  dualUnit :: Dual (Unit :: k) ~> Unit

distribDualInv :: forall {k} (a :: k) b. (CompactClosed k, Ob a, Ob b) => Dual a ** Dual b ~> Dual (a ** b)
distribDualInv :: forall {k} (a :: k) (b :: k).
(CompactClosed k, Ob a, Ob b) =>
(Dual a ** Dual b) ~> Dual (a ** b)
distribDualInv =
  forall (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
dualObj @a Obj (Dual a)
-> ((Ob (Dual a), Ob (Dual a)) =>
    (Dual a ** Dual b) ~> Dual (a ** b))
-> (Dual a ** Dual b) ~> Dual (a ** b)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
    forall (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
dualObj @b Obj (Dual b)
-> ((Ob (Dual b), Ob (Dual b)) =>
    (Dual a ** Dual b) ~> Dual (a ** b))
-> (Dual a ** Dual b) ~> Dual (a ** b)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
      let sw :: (Dual a ** Dual b) ~> (Dual b ** Dual a)
sw = forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @(Dual a) @(Dual b)
      in forall k (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @k @(Dual b ** Dual a) @a @b (((Dual a ** a) ~> Unit) -> (Dual b ** (Dual a ** a)) ~> Dual b
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (a ** b) ~> a
rightUnitorWith (forall (a :: k). (CompactClosed k, Ob a) => (Dual a ** a) ~> Unit
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
(Dual a ** a) ~> Unit
dualityCounit @a) ((Dual b ** (Dual a ** a)) ~> Dual b)
-> (((Dual b ** Dual a) ** a) ~> (Dual b ** (Dual a ** a)))
-> ((Dual b ** Dual a) ** a) ~> Dual b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @(Dual b) @(Dual a) @a) ((Dual b ** Dual a) ~> Dual (a ** b))
-> ((Dual a ** Dual b) ~> (Dual b ** Dual a))
-> (Dual a ** Dual b) ~> Dual (a ** b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Dual a ** Dual b) ~> (Dual b ** Dual a)
sw
           ((Ob (Dual a ** Dual b), Ob (Dual b ** Dual a)) =>
 (Dual a ** Dual b) ~> Dual (a ** b))
-> ((Dual a ** Dual b) ~> (Dual b ** Dual a))
-> (Dual a ** Dual b) ~> Dual (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
\\ (Dual a ** Dual b) ~> (Dual b ** Dual a)
sw

dualUnitInv :: forall {k}. (CompactClosed k) => (Unit :: k) ~> Dual Unit
dualUnitInv :: forall {k}. CompactClosed k => Unit ~> Dual Unit
dualUnitInv = forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @k @(Dual Unit) ((Unit ** Dual Unit) ~> Dual Unit)
-> (Unit ~> (Unit ** Dual Unit)) -> Unit ~> Dual Unit
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k). (CompactClosed k, Ob a) => Unit ~> (a ** Dual a)
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
Unit ~> (a ** Dual a)
dualityUnit @Unit ((Ob (Dual Unit), Ob (Dual Unit)) => Unit ~> Dual Unit)
-> (Dual Unit ~> Dual Unit) -> Unit ~> Dual 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
\\ forall (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
dualObj @(Unit :: k)

dualityUnit :: forall {k} (a :: k). (CompactClosed k, Ob a) => Unit ~> a ** Dual a
dualityUnit :: forall {k} (a :: k).
(CompactClosed k, Ob a) =>
Unit ~> (a ** Dual a)
dualityUnit = let dualA :: Obj (Dual a)
dualA = forall (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
dualObj @a in (forall (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
forall {k} (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
doubleNeg @a (Dual (Dual a) ~> a)
-> Obj (Dual a) -> (Dual (Dual a) ** Dual a) ~> (a ** Dual 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)
** Obj (Dual a)
dualA) ((Dual (Dual a) ** Dual a) ~> (a ** Dual a))
-> (Unit ~> (Dual (Dual a) ** Dual a)) -> Unit ~> (a ** Dual a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(CompactClosed k, Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual @k @(Dual a) @a (Dual (Dual a ** a) ~> (Dual (Dual a) ** Dual a))
-> (Unit ~> Dual (Dual a ** a))
-> Unit ~> (Dual (Dual a) ** Dual a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k).
(StarAutonomous k, Ob a) =>
Unit ~> Dual (Dual a ** a)
forall {k} (a :: k).
(StarAutonomous k, Ob a) =>
Unit ~> Dual (Dual a ** a)
dualityUnitSA @a ((Ob (Dual a), Ob (Dual a)) => Unit ~> (a ** Dual a))
-> Obj (Dual a) -> Unit ~> (a ** Dual 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
\\ Obj (Dual a)
dualA

dualityUnitS :: forall {k} (a :: k). (CompactClosed k, Ob a) => '[] ~> [a, Dual a]
dualityUnitS :: forall {k} (a :: k). (CompactClosed k, Ob a) => '[] ~> '[a, Dual a]
dualityUnitS = forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @'[] @[a, Dual a] (forall (a :: k). (CompactClosed k, Ob a) => Unit ~> (a ** Dual a)
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
Unit ~> (a ** Dual a)
dualityUnit @a)

dualityCounit :: forall {k} (a :: k). (CompactClosed k, Ob a) => Dual a ** a ~> Unit
dualityCounit :: forall {k} (a :: k).
(CompactClosed k, Ob a) =>
(Dual a ** a) ~> Unit
dualityCounit = Dual Unit ~> Unit
forall k. CompactClosed k => Dual Unit ~> Unit
dualUnit (Dual Unit ~> Unit)
-> ((Dual a ** a) ~> Dual Unit) -> (Dual a ** a) ~> Unit
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k).
(StarAutonomous k, Ob a) =>
(Dual a ** a) ~> Dual Unit
forall {k} (a :: k).
(StarAutonomous k, Ob a) =>
(Dual a ** a) ~> Dual Unit
dualityCounitSA @a

dualityCounitS :: forall {k} (a :: k). (CompactClosed k, Ob a) => [Dual a, a] ~> '[]
dualityCounitS :: forall {k} (a :: k). (CompactClosed k, Ob a) => '[Dual a, a] ~> '[]
dualityCounitS = forall (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str @[Dual a, a] @'[] (forall (a :: k). (CompactClosed k, Ob a) => (Dual a ** a) ~> Unit
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
(Dual a ** a) ~> Unit
dualityCounit @a)

combineDual :: forall {k} a b. (CompactClosed k, Ob (a :: k), Ob b) => Dual a ** Dual b ~> Dual (a ** b)
combineDual :: forall {k} (a :: k) (b :: k).
(CompactClosed k, Ob a, Ob b) =>
(Dual a ** Dual b) ~> Dual (a ** b)
combineDual =
  forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @(Dual a) @(Dual b)
    ( forall k (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @k @_ @a @b
        ( ((a ** Dual a) ~> Unit) -> ((a ** Dual a) ** Dual b) ~> Dual b
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (b ** a) ~> a
leftUnitorWith (forall (a :: k). (CompactClosed k, Ob a) => (Dual a ** a) ~> Unit
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
(Dual a ** a) ~> Unit
dualityCounit @a ((Dual a ** a) ~> Unit)
-> ((a ** Dual a) ~> (Dual a ** a)) -> (a ** Dual a) ~> Unit
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @a @(Dual a))
            (((a ** Dual a) ** Dual b) ~> Dual b)
-> (((Dual a ** Dual b) ** a) ~> ((a ** Dual a) ** Dual b))
-> ((Dual a ** Dual b) ** a) ~> Dual b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @a @(Dual a) @(Dual b)
            ((a ** (Dual a ** Dual b)) ~> ((a ** Dual a) ** Dual b))
-> (((Dual a ** Dual b) ** a) ~> (a ** (Dual a ** Dual b)))
-> ((Dual a ** Dual b) ** a) ~> ((a ** Dual a) ** Dual b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @(Dual a ** Dual b) @a
        )
    )

combineDualS :: forall {k} a b. (CompactClosed k, Ob (a :: k), Ob b) => '[Dual a, Dual b] ~> '[Dual (a ** b)]
combineDualS :: forall {k} (a :: k) (b :: k).
(CompactClosed k, Ob a, Ob b) =>
'[Dual a, Dual b] ~> '[Dual (a ** b)]
combineDualS = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @b ((Fold '[Dual a, Dual b] ~> Fold '[Dual (a ** b)])
-> Strictified '[Dual a, Dual b] '[Dual (a ** b)]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str (forall (a :: k) (b :: k).
(CompactClosed k, Ob a, Ob b) =>
(Dual a ** Dual b) ~> Dual (a ** b)
forall {k} (a :: k) (b :: k).
(CompactClosed k, Ob a, Ob b) =>
(Dual a ** Dual b) ~> Dual (a ** b)
combineDual @a @b))

dimension :: forall {k} (a :: k). (CompactClosed k, Ob a) => (Unit :: k) ~> Unit
dimension :: forall {k} (a :: k). (CompactClosed k, Ob a) => Unit ~> Unit
dimension = forall (u :: k) (x :: k) (y :: k).
(CompactClosed k, Ob x, Ob y, Ob u) =>
((x ** u) ~> (y ** u)) -> x ~> y
forall {k} (u :: k) (x :: k) (y :: k).
(CompactClosed k, Ob x, Ob y, Ob u) =>
((x ** u) ~> (y ** u)) -> x ~> y
traceCC @Unit (Unit ~> Unit
forall k. Monoidal k => Obj Unit
unitObj (Unit ~> Unit)
-> (Unit ~> Unit) -> (Unit ** Unit) ~> (Unit ** 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)
** Unit ~> Unit
forall k. Monoidal k => Obj Unit
unitObj)

traceCCS :: forall {k} u (x :: k) y. (CompactClosed k, Ob x, Ob y, Ob u) => [x, u] ~> [y, u] -> '[x] ~> '[y]
traceCCS :: forall {k} (u :: k) (x :: k) (y :: k).
(CompactClosed k, Ob x, Ob y, Ob u) =>
('[x, u] ~> '[y, u]) -> '[x] ~> '[y]
traceCCS '[x, u] ~> '[y, u]
f =
  forall (a :: k). (Monoidal k, Ob a) => Obj '[a]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 @x Strictified '[x] '[x]
-> Strictified '[] '[u, Dual u]
-> Strictified ('[x] ** '[]) ('[x] ** '[u, Dual u])
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (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). (CompactClosed k, Ob a) => '[] ~> '[a, Dual a]
forall {k} (a :: k). (CompactClosed k, Ob a) => '[] ~> '[a, Dual a]
dualityUnitS @u
    ('[x] ~> ('[x] ++ '[u, Dual u]))
-> (('[x] ++ '[u, Dual u]) ~> ('[y, u] ++ '[Dual u]))
-> '[x] ~> ('[y, u] ++ '[Dual u])
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== '[x, u] ~> '[y, u]
Strictified '[x, u] '[y, u]
f Strictified '[x, u] '[y, u]
-> Strictified '[Dual u] '[Dual u]
-> Strictified ('[x, u] ** '[Dual u]) ('[y, u] ** '[Dual u])
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (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). (Monoidal k, Ob a) => Obj '[a]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 @(Dual u)
    ('[x] ~> ('[y, u] ++ '[Dual u]))
-> (('[y, u] ++ '[Dual u]) ~> '[y]) -> '[x] ~> '[y]
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall (a :: k). (Monoidal k, Ob a) => Obj '[a]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 @y Strictified '[y] '[y]
-> Strictified '[u, Dual u] '[]
-> Strictified ('[y] ** '[u, Dual u]) ('[y] ** '[])
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (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).
(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]
swap2 @u @(Dual u) ('[u, Dual u] ~> '[Dual u, u])
-> ('[Dual u, u] ~> '[]) -> '[u, Dual u] ~> '[]
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall (a :: k). (CompactClosed k, Ob a) => '[Dual a, a] ~> '[]
forall {k} (a :: k). (CompactClosed k, Ob a) => '[Dual a, a] ~> '[]
dualityCounitS @u)

traceCC :: forall {k} u (x :: k) y. (CompactClosed k, Ob x, Ob y, Ob u) => x ** u ~> y ** u -> x ~> y
traceCC :: forall {k} (u :: k) (x :: k) (y :: k).
(CompactClosed k, Ob x, Ob y, Ob u) =>
((x ** u) ~> (y ** u)) -> x ~> y
traceCC (x ** u) ~> (y ** u)
f = Strictified '[x] '[y] -> Fold '[x] ~> Fold '[y]
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
unStr (forall (u :: k) (x :: k) (y :: k).
(CompactClosed k, Ob x, Ob y, Ob u) =>
('[x, u] ~> '[y, u]) -> '[x] ~> '[y]
forall {k} (u :: k) (x :: k) (y :: k).
(CompactClosed k, Ob x, Ob y, Ob u) =>
('[x, u] ~> '[y, u]) -> '[x] ~> '[y]
traceCCS @u ((Fold '[x, u] ~> Fold '[y, u]) -> Strictified '[x, u] '[y, u]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str (x ** u) ~> (y ** u)
Fold '[x, u] ~> Fold '[y, u]
f))

coactCC
  :: forall {m} {k} (t :: (m, k) +-> k) (u :: m) (x :: k) (y :: k)
   . (CompactClosed m, MonoidalAction t, Ob x, Ob y, Ob u) => Act t u x ~> Act t u y -> x ~> y
coactCC :: forall {m} {k} (t :: (m, k) +-> k) (u :: m) (x :: k) (y :: k).
(CompactClosed m, MonoidalAction t, Ob x, Ob y, Ob u) =>
(Act t u x ~> Act t u y) -> x ~> y
coactCC Act t u x ~> Act t u y
f =
  forall {m} {k} (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
Act t Unit x ~> x
forall (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
Act t Unit x ~> x
unitor @t @y
    (Act t Unit y ~> y) -> (x ~> Act t Unit y) -> x ~> y
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k)
       (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
forall (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k) (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
actHom @t (forall (a :: m). (CompactClosed m, Ob a) => (Dual a ** a) ~> Unit
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
(Dual a ** a) ~> Unit
dualityCounit @u) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @y)
    ((t % '(Dual u ** u, y)) ~> Act t Unit y)
-> (x ~> (t % '(Dual u ** u, y))) -> x ~> Act t Unit y
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t a (Act t b x) ~> Act t (a ** b) x
forall (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t a (Act t b x) ~> Act t (a ** b) x
multiplicatorInv @t @(Dual u) @u @y
    (Act t (Dual u) (Act t u y) ~> (t % '(Dual u ** u, y)))
-> (x ~> Act t (Dual u) (Act t u y))
-> x ~> (t % '(Dual u ** u, y))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k)
       (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
forall (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k) (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
actHom @t (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Dual u)) Act t u x ~> Act t u y
f
    ((t % '(Dual u, Act t u x)) ~> Act t (Dual u) (Act t u y))
-> (x ~> (t % '(Dual u, Act t u x)))
-> x ~> Act t (Dual u) (Act t u y)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t (a ** b) x ~> Act t a (Act t b x)
forall (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k).
(MonoidalAction t, Ob a, Ob b, Ob x) =>
Act t (a ** b) x ~> Act t a (Act t b x)
multiplicator @t @(Dual u) @u @x
    (Act t (Dual u ** u) x ~> (t % '(Dual u, Act t u x)))
-> (x ~> Act t (Dual u ** u) x) -> x ~> (t % '(Dual u, Act t u x))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k)
       (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
forall (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k) (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
actHom @t (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @m @u @(Dual u) ((u ** Dual u) ~> (Dual u ** u))
-> (Unit ~> (u ** Dual u)) -> Unit ~> (Dual u ** u)
forall (b :: m) (c :: m) (a :: m). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: m). (CompactClosed m, Ob a) => Unit ~> (a ** Dual a)
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
Unit ~> (a ** Dual a)
dualityUnit @u) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x)
    ((t % '(Unit, x)) ~> Act t (Dual u ** u) x)
-> (x ~> (t % '(Unit, x))) -> x ~> Act t (Dual u ** u) x
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {m} {k} (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
x ~> Act t Unit x
forall (t :: (m, k) +-> k) (x :: k).
(MonoidalAction t, Ob x) =>
x ~> Act t Unit x
unitorInv @t @x
    ((Ob (Dual u), Ob (Dual u)) => x ~> y)
-> (Dual u ~> Dual u) -> x ~> y
forall (a :: m) (b :: m) 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 (a :: m). (StarAutonomous m, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
dualObj @u

instance CompactClosed () where
  distribDual :: forall (a :: ()) (b :: ()).
(Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual = Dual (a ** b) ~> (Dual a ** Dual b)
Unit '() '()
U.Unit
  dualUnit :: Dual Unit ~> Unit
dualUnit = Dual Unit ~> Unit
Unit '() '()
U.Unit

instance (CompactClosed j, CompactClosed k) => CompactClosed (j, k) where
  distribDual :: forall (a :: (j, k)) (b :: (j, k)).
(Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual @'(a, a') @'(b, b') = forall k (a :: k) (b :: k).
(CompactClosed k, Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual @j @a @b (Dual ((Fst @ a) ** (Fst @ b))
 ~> (Dual (Fst @ a) ** Dual (Fst @ b)))
-> (Dual ((Snd @ a) ** (Snd @ b))
    ~> (Dual (Snd @ a) ** Dual (Snd @ b)))
-> (:**:)
     (~>)
     (~>)
     '(Dual ((Fst @ a) ** (Fst @ b)), Dual ((Snd @ a) ** (Snd @ b)))
     '(Dual (Fst @ a) ** Dual (Fst @ b),
       Dual (Snd @ a) ** Dual (Snd @ b))
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).
(CompactClosed k, Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual @k @a' @b'
  dualUnit :: Dual Unit ~> Unit
dualUnit = Dual Unit ~> Unit
forall k. CompactClosed k => Dual Unit ~> Unit
dualUnit (Dual Unit ~> Unit)
-> (Dual Unit ~> Unit)
-> (:**:) (~>) (~>) '(Dual Unit, Dual 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)
:**: Dual Unit ~> Unit
forall k. CompactClosed k => Dual Unit ~> Unit
dualUnit