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

-- | Compact closed categories: star-autonomous categories whose dual distributes over the tensor
-- ('distribDual', 'dualUnit'), so that every object has a duality unit and counit ('dualityUnit',
-- 'dualityCounit') and every morphism @x ** u ~> y ** u@ has a trace ('traceCC').
module Proarrow.Category.Monoidal.CompactClosed where

import Data.Kind (Constraint)
import Prelude (($))
import Prelude qualified as P

import Proarrow.Category.Instance.Free (Elems, FREE (..), Free (..), HasStructure (..), Lower, withLowerOb)
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , SymMonoidal (..)
  , UnitF
  , leftUnitorWith
  , swap
  , unitObj
  , type (**!)
  )
import Proarrow.Category.Monoidal.Action (Act, MonoidalAction (..), actHom)
import Proarrow.Category.Monoidal.Closed (Closed)
import Proarrow.Category.Monoidal.StarAutonomous
  ( DualF
  , StarAutonomous (..)
  , doubleNeg
  , dualObj
  , dualityCounitSA
  , dualityUnitSA
  )
import Proarrow.Category.Monoidal.Strictified (Strictified (..), obj1, swap2, (==))
import Proarrow.Core (CAT, CategoryOf (..), Kind, Profunctor (..), Promonad (..), obj, type (+->))
import Proarrow.Tools.Laws (Inverses (..), Labelled (..), Law (..), Laws (..), inverses, (===))

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

  -- | The unit of the duality between @a@ and its dual. 'dualityUnitDefault' gives it from the
  -- *-autonomous structure; an instance with cups of its own can use them. (There is no default
  -- method: @a@ occurs only under type families, so GHC could not instantiate one.)
  dualityUnit :: (Ob (a :: k)) => Unit ~> a ** Dual a

  -- | The counit of the duality between @a@ and its dual; see 'dualityCounitDefault'.
  dualityCounit :: (Ob (a :: k)) => Dual a ** a ~> Unit

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 :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k). (CompactClosed k, Ob a) => Unit ~> (a ** Dual a)
dualityUnit @k @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' from the *-autonomous structure.
dualityUnitDefault :: forall {k} (a :: k). (CompactClosed k, Ob a) => Unit ~> a ** Dual a
dualityUnitDefault :: forall {k} (a :: k).
(CompactClosed k, Ob a) =>
Unit ~> (a ** Dual a)
dualityUnitDefault = 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 k (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
doubleNeg @k @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 :: 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).
(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 :: CAT 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 k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @k @a (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 k (a :: k). (CompactClosed k, Ob a) => Unit ~> (a ** Dual a)
dualityUnit @k @a))

-- | 'dualityCounit' from the *-autonomous structure.
dualityCounitDefault :: forall {k} (a :: k). (CompactClosed k, Ob a) => Dual a ** a ~> Unit
dualityCounitDefault :: forall {k} (a :: k).
(CompactClosed k, Ob a) =>
(Dual a ** a) ~> Unit
dualityCounitDefault = 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 :: CAT 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 k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @k @a (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 k (a :: k). (CompactClosed k, Ob a) => (Dual a ** a) ~> Unit
dualityCounit @k @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) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @k @a ((Ob (Dual a) => (Dual a ** Dual b) ~> Dual (a ** b))
 -> (Dual a ** Dual b) ~> Dual (a ** b))
-> (Ob (Dual a) => (Dual a ** Dual b) ~> Dual (a ** b))
-> (Dual a ** Dual b) ~> Dual (a ** b)
forall a b. (a -> b) -> a -> b
$
    forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @k @b ((Ob (Dual b) => (Dual a ** Dual b) ~> Dual (a ** b))
 -> (Dual a ** Dual b) ~> Dual (a ** b))
-> (Ob (Dual b) => (Dual a ** Dual b) ~> Dual (a ** b))
-> (Dual a ** Dual b) ~> Dual (a ** b)
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 @(Dual a) @(Dual b) ((Ob (Dual a ** Dual b) => (Dual a ** Dual b) ~> Dual (a ** b))
 -> (Dual a ** Dual b) ~> Dual (a ** b))
-> (Ob (Dual a ** Dual b) => (Dual a ** Dual b) ~> Dual (a ** b))
-> (Dual a ** Dual b) ~> Dual (a ** b)
forall a b. (a -> b) -> a -> 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 ((((Dual a ** Dual b) ** a) ~> Dual b)
 -> (Dual a ** Dual b) ~> Dual (a ** b))
-> (((Dual a ** Dual b) ** a) ~> Dual b)
-> (Dual a ** Dual b) ~> Dual (a ** b)
forall a b. (a -> b) -> 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 k (a :: k). (CompactClosed k, Ob a) => (Dual a ** a) ~> Unit
dualityCounit @k @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 :: 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 @(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 :: 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 @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 :: 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 @(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) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @k @a (forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @k @b (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @b (forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @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)))))

-- | The dimension of @a@: the trace of its identity, as a scalar.
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 @a (Unit ~> Unit
forall k. Monoidal k => Obj Unit
unitObj (Unit ~> Unit) -> (a ~> a) -> (Unit ** 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)

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 k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @k @u ((Ob (Dual u) => '[x] ~> '[y]) -> '[x] ~> '[y])
-> (Ob (Dual u) => '[x] ~> '[y]) -> '[x] ~> '[y]
forall a b. (a -> b) -> a -> b
$
    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 :: CAT 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). (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 :: CAT 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 :: CAT 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 :: CAT 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 :: CAT 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 :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. 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 :: CAT 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
  dualityUnit :: forall (a :: ()). Ob a => Unit ~> (a ** Dual a)
dualityUnit = Unit ~> (a ** Dual a)
Unit '() '()
U.Unit
  dualityCounit :: forall (a :: ()). Ob a => (Dual a ** a) ~> Unit
dualityCounit = (Dual a ** a) ~> 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
  dualityUnit :: forall (a :: (j, k)). Ob a => Unit ~> (a ** Dual a)
dualityUnit @'(a, a') = forall k (a :: k). (CompactClosed k, Ob a) => Unit ~> (a ** Dual a)
dualityUnit @j @a (Unit ~> ((Fst @ a) ** Dual (Fst @ a)))
-> (Unit ~> ((Snd @ a) ** Dual (Snd @ a)))
-> (:**:)
     (~>)
     (~>)
     '(Unit, Unit)
     '((Fst @ a) ** Dual (Fst @ a), (Snd @ a) ** Dual (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). (CompactClosed k, Ob a) => Unit ~> (a ** Dual a)
dualityUnit @k @a'
  dualityCounit :: forall (a :: (j, k)). Ob a => (Dual a ** a) ~> Unit
dualityCounit @'(a, a') = forall k (a :: k). (CompactClosed k, Ob a) => (Dual a ** a) ~> Unit
dualityCounit @j @a ((Dual (Fst @ a) ** (Fst @ a)) ~> Unit)
-> ((Dual (Snd @ a) ** (Snd @ a)) ~> Unit)
-> (:**:)
     (~>)
     (~>)
     '(Dual (Fst @ a) ** (Fst @ a), Dual (Snd @ a) ** (Snd @ a))
     '(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)
:**: forall k (a :: k). (CompactClosed k, Ob a) => (Dual a ** a) ~> Unit
dualityCounit @k @a'

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

instance
  (CompactClosedStructures `Elems` cs)
  => HasStructure cs (p :: CAT k) CompactClosed
  where
  data Struct CompactClosed a b where
    DistribDual :: (Ob a, Ob b) => Struct CompactClosed (DualF (a **! b)) (DualF a **! DualF b)
    DualUnit :: Struct CompactClosed (DualF UnitF) UnitF
  foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p).
(CompactClosed k', All cs k', Representable f) =>
(forall (x :: FREE cs p) (y :: FREE cs p).
 (x ~> y) -> Lower f x ~> Lower f y)
-> Struct CompactClosed 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
_ (DistribDual @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).
(CompactClosed k, Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual @_ @(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 CompactClosed a b
R:StructkcspCompactClosedab k cs p a b
DualUnit = Lower f a ~> Lower f b
Dual Unit ~> Unit
forall k. CompactClosed k => Dual Unit ~> Unit
dualUnit
instance P.Show (Struct CompactClosed a b) where
  showsPrec :: Int -> Struct CompactClosed a b -> ShowS
showsPrec Int
_ Struct CompactClosed a b
R:StructkcspCompactClosedab k cs p a b
DistribDual = String -> ShowS
P.showString String
"distribDual"
  showsPrec Int
_ Struct CompactClosed a b
R:StructkcspCompactClosedab k cs p a b
DualUnit = String -> ShowS
P.showString String
"dualUnit"

instance
  (CompactClosedStructures `Elems` cs)
  => CompactClosed (FREE cs (p :: CAT k))
  where
  distribDual :: forall (a :: FREE cs p) (b :: FREE cs p).
(Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual @a @b = Struct CompactClosed (DualF (a **! b)) (DualF a **! DualF b)
-> Free (DualF (a **! b)) (DualF (a **! b))
-> Free (DualF (a **! b)) (DualF a **! DualF b)
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 (forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p) (b :: FREE cs p).
(Ob a, Ob b) =>
Struct CompactClosed (DualF (a **! b)) (DualF a **! DualF b)
forall (a :: FREE cs p) (b :: FREE cs p).
(Ob a, Ob b) =>
Struct CompactClosed (DualF (a **! b)) (DualF a **! DualF b)
DistribDual @a @b) Free (DualF (a **! b)) (DualF (a **! b))
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil
  dualUnit :: Dual Unit ~> Unit
dualUnit = Struct CompactClosed (DualF UnitF) UnitF
-> Free (DualF UnitF) (DualF UnitF) -> Free (DualF 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 CompactClosed (DualF UnitF) UnitF
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}.
Struct CompactClosed (DualF UnitF) UnitF
DualUnit Free (DualF UnitF) (DualF UnitF)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil
  dualityUnit :: forall (a :: FREE cs p). Ob a => Unit ~> (a ** Dual a)
dualityUnit @a = forall {k} (a :: k).
(CompactClosed k, Ob a) =>
Unit ~> (a ** Dual a)
forall (a :: FREE cs p).
(CompactClosed (FREE cs p), Ob a) =>
Unit ~> (a ** Dual a)
dualityUnitDefault @a
  dualityCounit :: forall (a :: FREE cs p). Ob a => (Dual a ** a) ~> Unit
dualityCounit @a = forall {k} (a :: k).
(CompactClosed k, Ob a) =>
(Dual a ** a) ~> Unit
forall (a :: FREE cs p).
(CompactClosed (FREE cs p), Ob a) =>
(Dual a ** a) ~> Unit
dualityCounitDefault @a

-- | 'distribDual' and 'dualUnit' are isomorphisms (so 'Dual' is strong monoidal), and 'dualityUnit'
-- and 'dualityCounit' satisfy the zigzag identities, making @Dual a@ dual to @a@.
instance Laws CompactClosedStructures where
  laws :: [Law CompactClosedStructures]
laws =
    String
-> PureLawBody CompactClosedStructures Inverses
-> [Law CompactClosedStructures]
forall (cs :: [Type -> Constraint]).
String -> PureLawBody cs Inverses -> [Law cs]
inverses String
"distribDual" (\ @a @b -> (Dual (a ** b) ~> (Dual a ** Dual b))
-> ((Dual a ** Dual b) ~> Dual (a ** b)) -> Inverses k
forall {k} (a :: k) (b :: k). (a ~> b) -> (b ~> a) -> Inverses k
Inverses (forall k (a :: k) (b :: k).
(CompactClosed k, Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual @_ @a @b) (String
-> ((Dual a ** Dual b) ~> Dual (a ** b))
-> (Dual a ** Dual b) ~> Dual (a ** b)
forall (a :: k) (b :: k). String -> (a ~> b) -> a ~> b
forall k (a :: k) (b :: k).
Labelled k =>
String -> (a ~> b) -> a ~> b
label String
"combineDual" (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)))
      [Law CompactClosedStructures]
-> [Law CompactClosedStructures] -> [Law CompactClosedStructures]
forall a. [a] -> [a] -> [a]
P.++ String
-> PureLawBody CompactClosedStructures Inverses
-> [Law CompactClosedStructures]
forall (cs :: [Type -> Constraint]).
String -> PureLawBody cs Inverses -> [Law cs]
inverses String
"dualUnit" ((Dual Unit ~> Unit) -> (Unit ~> Dual Unit) -> Inverses k
forall {k} (a :: k) (b :: k). (a ~> b) -> (b ~> a) -> Inverses k
Inverses Dual Unit ~> Unit
forall k. CompactClosed k => Dual Unit ~> Unit
dualUnit (String -> (Unit ~> Dual Unit) -> Unit ~> Dual Unit
forall (a :: k) (b :: k). String -> (a ~> b) -> a ~> b
forall k (a :: k) (b :: k).
Labelled k =>
String -> (a ~> b) -> a ~> b
label String
"dualUnitInv" Unit ~> Dual Unit
forall {k}. CompactClosed k => Unit ~> Dual Unit
dualUnitInv))
      [Law CompactClosedStructures]
-> [Law CompactClosedStructures] -> [Law CompactClosedStructures]
forall a. [a] -> [a] -> [a]
P.++ [ String
-> LawBody CompactClosedStructures -> Law CompactClosedStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"dualityUnit definition" \ @a forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ -> forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @_ @a (forall k (a :: k). (CompactClosed k, Ob a) => Unit ~> (a ** Dual a)
dualityUnit @_ @a (Unit ~> (a ** Dual a))
-> (Unit ~> (a ** Dual 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). (CompactClosed k, Ob a) => Unit ~> (a ** Dual a)
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
Unit ~> (a ** Dual a)
dualityUnitDefault @a)
           , String
-> LawBody CompactClosedStructures -> Law CompactClosedStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"dualityCounit definition" \ @a forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ -> forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @_ @a (forall k (a :: k). (CompactClosed k, Ob a) => (Dual a ** a) ~> Unit
dualityCounit @_ @a ((Dual a ** a) ~> Unit)
-> ((Dual a ** a) ~> Unit) -> 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). (CompactClosed k, Ob a) => (Dual a ** a) ~> Unit
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
(Dual a ** a) ~> Unit
dualityCounitDefault @a)
           , String
-> LawBody CompactClosedStructures -> Law CompactClosedStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law
               String
"zigzag (a)"
               \ @a forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ ->
                 forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @_ @a ((Ob (Dual a) => m (Equation k)) -> m (Equation k))
-> (Ob (Dual a) => m (Equation k)) -> m (Equation k)
forall a b. (a -> b) -> a -> b
$
                   ( forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor @_ @a
                       ((a ** Unit) ~> a) -> (a ~> (a ** Unit)) -> 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
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a (a ~> a)
-> ((Dual a ** a) ~> Unit) -> (a ** (Dual a ** a)) ~> (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)
** forall k (a :: k). (CompactClosed k, Ob a) => (Dual a ** a) ~> Unit
dualityCounit @_ @a)
                       ((a ** (Dual a ** a)) ~> (a ** Unit))
-> (a ~> (a ** (Dual a ** a))) -> a ~> (a ** 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
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @a @(Dual a) @a
                       (((a ** Dual a) ** a) ~> (a ** (Dual a ** a)))
-> (a ~> ((a ** Dual a) ** a)) -> a ~> (a ** (Dual 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
. (forall k (a :: k). (CompactClosed k, Ob a) => Unit ~> (a ** Dual a)
dualityUnit @_ @a (Unit ~> (a ** Dual a))
-> (a ~> a) -> (Unit ** a) ~> ((a ** Dual a) ** 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) ~> ((a ** Dual a) ** a))
-> (a ~> (Unit ** a)) -> a ~> ((a ** Dual 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
. forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @_ @a
                   )
                     (a ~> a) -> (a ~> 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
=== a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
           , String
-> LawBody CompactClosedStructures -> Law CompactClosedStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law
               String
"zigzag (Dual a)"
               \ @a forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
_ ->
                 forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @_ @a ((Ob (Dual a) => m (Equation k)) -> m (Equation k))
-> (Ob (Dual a) => m (Equation k)) -> m (Equation k)
forall a b. (a -> b) -> a -> b
$
                   ( forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @_ @(Dual a)
                       ((Unit ** Dual a) ~> Dual a)
-> (Dual a ~> (Unit ** Dual a)) -> Dual a ~> Dual 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). (CompactClosed k, Ob a) => (Dual a ** a) ~> Unit
dualityCounit @_ @a ((Dual a ** a) ~> Unit)
-> (Dual a ~> Dual a)
-> ((Dual a ** a) ** Dual a) ~> (Unit ** 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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Dual a))
                       (((Dual a ** a) ** Dual a) ~> (Unit ** Dual a))
-> (Dual a ~> ((Dual a ** a) ** Dual a))
-> Dual a ~> (Unit ** Dual 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)
associatorInv @_ @(Dual a) @a @(Dual a)
                       ((Dual a ** (a ** Dual a)) ~> ((Dual a ** a) ** Dual a))
-> (Dual a ~> (Dual a ** (a ** Dual a)))
-> Dual a ~> ((Dual a ** a) ** Dual 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 @(Dual a) (Dual a ~> Dual a)
-> (Unit ~> (a ** Dual a))
-> (Dual a ** Unit) ~> (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)
** forall k (a :: k). (CompactClosed k, Ob a) => Unit ~> (a ** Dual a)
dualityUnit @_ @a)
                       ((Dual a ** Unit) ~> (Dual a ** (a ** Dual a)))
-> (Dual a ~> (Dual a ** Unit))
-> Dual a ~> (Dual a ** (a ** Dual 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). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv @_ @(Dual a)
                   )
                     (Dual a ~> Dual a) -> (Dual a ~> Dual 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
=== Dual a ~> Dual a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
           ]