{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Object.Dual where

import Prelude qualified as P

import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , SymMonoidal (..)
  , associator
  , leftUnitor
  , swapInner'
  , unitObj, swapInner, leftUnitor'
  )
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), tgt)
import Proarrow.Object (Obj, obj, src)
import Proarrow.Object.Exponential (Closed (..), eval', mkExponential, curry, eval)

type Dual a = a ~~> Bottom

dual' :: forall {k} (a :: k) a'. (StarAutonomous k) => a ~> a' -> Dual a' ~> Dual a
dual' :: forall {k} (a :: k) (a' :: k).
StarAutonomous k =>
(a ~> a') -> Dual a' ~> Dual a
dual' a ~> a'
a = Obj Bottom
forall k. StarAutonomous k => Obj Bottom
bottomObj Obj Bottom -> (a ~> a') -> (a' ~~> Bottom) ~> (a ~~> Bottom)
forall (b :: k) (y :: k) (x :: k) (a :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (b :: k) (y :: k) (x :: k) (a :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ a ~> a'
a

dual :: forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
dual :: forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
dual = (a ~> a) -> (a ~~> Bottom) ~> (a ~~> Bottom)
forall {k} (a :: k) (a' :: k).
StarAutonomous k =>
(a ~> a') -> Dual a' ~> Dual a
dual' (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a)

class (Closed k) => StarAutonomous k where
  {-# MINIMAL bottomObj, (doubleNeg | doubleNeg') #-}
  type Bottom :: k
  bottomObj :: Obj (Bottom :: k)
  doubleNeg :: forall (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
  doubleNeg = (a ~> a) -> ((a ~~> Bottom) ~~> Bottom) ~> a
forall (a :: k) (a' :: k). (a ~> a') -> Dual (Dual a) ~> a'
forall k (a :: k) (a' :: k).
StarAutonomous k =>
(a ~> a') -> Dual (Dual a) ~> a'
doubleNeg' (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a)
  doubleNeg' :: forall (a :: k) a'. a ~> a' -> Dual (Dual a) ~> a'
  doubleNeg' a ~> a'
a = a ~> a'
a (a ~> a')
-> (((a ~~> Bottom) ~~> Bottom) ~> a)
-> ((a ~~> Bottom) ~~> Bottom) ~> 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).
(StarAutonomous k, StarAutonomous k, Ob a) =>
Dual (Dual a) ~> a
doubleNeg @k @a ((Ob a, Ob a') => ((a ~~> Bottom) ~~> Bottom) ~> a')
-> (a ~> a') -> ((a ~~> Bottom) ~~> Bottom) ~> 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
\\ a ~> a'
a

doubleNegInv' :: (Closed k, SymMonoidal k) => (a :: k) ~> a' -> b ~> b' -> a ~> (a' ~~> b) ~~> b'
doubleNegInv' :: forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
(Closed k, SymMonoidal k) =>
(a ~> a') -> (b ~> b') -> a ~> ((a' ~~> b) ~~> b')
doubleNegInv' a ~> a'
a b ~> b'
b = let a'b :: (a' ~~> b) ~> (a' ~~> b)
a'b = ((b ~> b') -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src b ~> b'
b (b ~> b) -> (a' ~> a') -> (a' ~~> b) ~> (a' ~~> b)
forall (b :: k) (y :: k) (x :: k) (a :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (b :: k) (y :: k) (x :: k) (a :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ (a ~> a') -> a' ~> a'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt a ~> a'
a) in Obj a
-> ((a' ~~> b) ~> (a' ~~> b))
-> ((a ** (a' ~~> b)) ~> b')
-> a ~> ((a' ~~> b) ~~> b')
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
forall k (a :: k) (b :: k) (c :: k).
Closed k =>
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' ((a ~> a') -> Obj a
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src a ~> a'
a) (a' ~~> b) ~> (a' ~~> b)
a'b ((a' ~> a') -> (b ~> b') -> ((a' ~~> b) ** a') ~> b'
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
Closed k =>
(a ~> a') -> (b ~> b') -> ((a' ~~> b) ** a) ~> b'
eval' ((a ~> a') -> a' ~> a'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt a ~> a'
a) b ~> b'
b (((a' ~~> b) ** a') ~> b')
-> ((a ** (a' ~~> b)) ~> ((a' ~~> b) ** a'))
-> (a ** (a' ~~> b)) ~> 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 ~> a')
-> ((a' ~~> b) ~> (a' ~~> b))
-> (a ** (a' ~~> b)) ~> ((a' ~~> b) ** a')
forall (a :: k) (a' :: k) (b :: k) (b' :: k).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
SymMonoidal k =>
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' a ~> a'
a (a' ~~> b) ~> (a' ~~> b)
a'b)

dualityCounit' :: forall {k} a. (StarAutonomous k) => Obj a -> Dual a ** a ~> (Bottom :: k)
dualityCounit' :: forall {k} (a :: k).
StarAutonomous k =>
Obj a -> (Dual a ** a) ~> Bottom
dualityCounit' Obj a
a = Obj a -> (Bottom ~> Bottom) -> ((a ~~> Bottom) ** a) ~> Bottom
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
Closed k =>
(a ~> a') -> (b ~> b') -> ((a' ~~> b) ** a) ~> b'
eval' Obj a
a Bottom ~> Bottom
forall k. StarAutonomous k => Obj Bottom
bottomObj

dualityCounit :: forall {k} a. (SymMonoidal k, StarAutonomous k, Ob a) => Dual a ** a ~> (Bottom :: k)
dualityCounit :: forall {k} (a :: k).
(SymMonoidal k, StarAutonomous k, Ob a) =>
(Dual a ** a) ~> Bottom
dualityCounit = Obj a -> ((a ~~> Bottom) ** a) ~> Bottom
forall {k} (a :: k).
StarAutonomous k =>
Obj a -> (Dual a ** a) ~> Bottom
dualityCounit' (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a)

instance StarAutonomous () where
  type Bottom = '()
  bottomObj :: Obj Bottom
bottomObj = Obj Bottom
Unit '() '()
U.Unit
  doubleNeg :: forall (a :: ()). (StarAutonomous (), Ob a) => Dual (Dual a) ~> a
doubleNeg = ((a ~~> Bottom) ~~> Bottom) ~> a
Unit '() '()
U.Unit

instance (StarAutonomous j, StarAutonomous k) => StarAutonomous (j, k) where
  type Bottom = '(Bottom, Bottom)
  bottomObj :: Obj Bottom
bottomObj = Obj Bottom
forall k. StarAutonomous k => Obj Bottom
bottomObj Obj Bottom
-> (Bottom ~> Bottom)
-> (:**:) (~>) (~>) '(Bottom, Bottom) '(Bottom, Bottom)
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)
:**: Bottom ~> Bottom
forall k. StarAutonomous k => Obj Bottom
bottomObj
  doubleNeg :: forall (a :: (j, k)).
(StarAutonomous (j, k), Ob a) =>
Dual (Dual a) ~> a
doubleNeg = Dual (Dual (Fst a)) ~> Fst a
forall (a :: j). (StarAutonomous j, Ob a) => Dual (Dual a) ~> a
forall k (a :: k).
(StarAutonomous k, StarAutonomous k, Ob a) =>
Dual (Dual a) ~> a
doubleNeg (Dual (Dual (Fst a)) ~> Fst a)
-> (((Snd a ~~> Bottom) ~~> Bottom) ~> Snd a)
-> (:**:)
     (~>)
     (~>)
     '(Dual (Dual (Fst a)), (Snd a ~~> Bottom) ~~> Bottom)
     '(Fst a, Snd a)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: ((Snd a ~~> Bottom) ~~> Bottom) ~> Snd a
forall (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
forall k (a :: k).
(StarAutonomous k, StarAutonomous k, Ob a) =>
Dual (Dual a) ~> a
doubleNeg

class ((Bottom :: k) P.~ Unit, StarAutonomous k, SymMonoidal k) => CompactClosed k where
  {-# MINIMAL (distribDual | distribDual') #-}
  distribDual :: forall (a :: k) b. (Ob a, Ob b) => Dual (a ** b) ~> Dual a ** Dual b
  distribDual = (a ~> a)
-> (b ~> b)
-> ((a ** b) ~~> Bottom) ~> ((a ~~> Bottom) ** (b ~~> Bottom))
forall (a :: k) (a' :: k) (b :: k) (b' :: k).
(a ~> a') -> (b ~> b') -> Dual (a' ** b') ~> (Dual a ** Dual b)
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
CompactClosed k =>
(a ~> a') -> (b ~> b') -> Dual (a' ** b') ~> (Dual a ** Dual b)
distribDual' (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b)
  distribDual' :: forall a a' b b'. (a :: k) ~> a' -> b ~> b' -> Dual (a' ** b') ~> Dual a ** Dual b
  distribDual' a ~> a'
a b ~> b'
b = ((a ~> a') -> Dual a' ~> (a ~~> Bottom)
forall {k} (a :: k) (a' :: k).
StarAutonomous k =>
(a ~> a') -> Dual a' ~> Dual a
dual' a ~> a'
a ((a' ~~> Unit) ~> (a ~~> Unit))
-> ((b' ~~> Unit) ~> (b ~~> Unit))
-> ((a' ~~> Unit) ** (b' ~~> 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` (b ~> b') -> Dual b' ~> (b ~~> Bottom)
forall {k} (a :: k) (a' :: k).
StarAutonomous k =>
(a ~> a') -> Dual a' ~> Dual a
dual' b ~> b'
b) (((a' ~~> Unit) ** (b' ~~> Unit))
 ~> ((a ~~> Unit) ** (b ~~> Unit)))
-> (((a' ** b') ~~> Unit) ~> ((a' ~~> Unit) ** (b' ~~> Unit)))
-> ((a' ** b') ~~> Unit) ~> ((a ~~> Unit) ** (b ~~> 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 k (a :: k) (b :: k).
(CompactClosed k, Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual @_ @a' @b' ((Ob a, Ob a') =>
 ((a' ** b') ~~> Unit) ~> ((a ~~> Unit) ** (b ~~> Unit)))
-> (a ~> a')
-> ((a' ** b') ~~> Unit) ~> ((a ~~> Unit) ** (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 ~> a'
a ((Ob b, Ob b') =>
 ((a' ** b') ~~> Unit) ~> ((a ~~> Unit) ** (b ~~> Unit)))
-> (b ~> b')
-> ((a' ** b') ~~> Unit) ~> ((a ~~> Unit) ** (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
\\ b ~> b'
b

combineDual' :: (CompactClosed k) => (a :: k) ~> a' -> b ~> b' -> Dual a' ** Dual b' ~> Dual (a ** b)
combineDual' :: forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
CompactClosed k =>
(a ~> a') -> (b ~> b') -> (Dual a' ** Dual b') ~> Dual (a ** b)
combineDual' a ~> a'
a b ~> b'
b =
  let dualA :: (a' ~~> Bottom) ~> (a' ~~> Bottom)
dualA = (a' ~> a') -> (a' ~~> Bottom) ~> (a' ~~> Bottom)
forall {k} (a :: k) (a' :: k).
StarAutonomous k =>
(a ~> a') -> Dual a' ~> Dual a
dual' ((a ~> a') -> a' ~> a'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt a ~> a'
a); dualB :: (b' ~~> Bottom) ~> (b' ~~> Bottom)
dualB = (b' ~> b') -> (b' ~~> Bottom) ~> (b' ~~> Bottom)
forall {k} (a :: k) (a' :: k).
StarAutonomous k =>
(a ~> a') -> Dual a' ~> Dual a
dual' ((b ~> b') -> b' ~> b'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt b ~> b'
b)
  in Obj ((a' ~~> Unit) ** (b' ~~> Unit))
-> Obj (a ** b)
-> ((((a' ~~> Unit) ** (b' ~~> Unit)) ** (a ** b)) ~> Unit)
-> ((a' ~~> Unit) ** (b' ~~> Unit)) ~> ((a ** b) ~~> Unit)
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
forall k (a :: k) (b :: k) (c :: k).
Closed k =>
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry'
      ((a' ~~> Unit) ~> (a' ~~> Unit)
(a' ~~> Bottom) ~> (a' ~~> Bottom)
dualA ((a' ~~> Unit) ~> (a' ~~> Unit))
-> ((b' ~~> Unit) ~> (b' ~~> Unit))
-> Obj ((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` (b' ~~> Unit) ~> (b' ~~> Unit)
(b' ~~> Bottom) ~> (b' ~~> Bottom)
dualB)
      ((a ~> a') -> a ~> a
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src a ~> a'
a (a ~> a) -> (b ~> b) -> Obj (a ** b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` (b ~> b') -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src b ~> b'
b)
      ((Unit ~> Unit) -> (Unit ** Unit) ~> Unit
forall k (a :: k) (b :: k).
Monoidal k =>
(a ~> b) -> (Unit ** a) ~> b
leftUnitor' Unit ~> Unit
forall k. Monoidal k => Obj Unit
unitObj ((Unit ** Unit) ~> Unit)
-> ((((a' ~~> Unit) ** (b' ~~> Unit)) ** (a ** b))
    ~> (Unit ** Unit))
-> (((a' ~~> Unit) ** (b' ~~> Unit)) ** (a ** b)) ~> 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
. ((a ~> a') -> (Unit ~> Unit) -> ((a' ~~> Unit) ** a) ~> Unit
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
Closed k =>
(a ~> a') -> (b ~> b') -> ((a' ~~> b) ** a) ~> b'
eval' a ~> a'
a Unit ~> Unit
forall k. Monoidal k => Obj Unit
unitObj (((a' ~~> Unit) ** a) ~> Unit)
-> (((b' ~~> Unit) ** b) ~> Unit)
-> (((a' ~~> Unit) ** a) ** ((b' ~~> Unit) ** b)) ~> (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)
`par` (b ~> b') -> (Unit ~> Unit) -> ((b' ~~> Unit) ** b) ~> Unit
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
Closed k =>
(a ~> a') -> (b ~> b') -> ((a' ~~> b) ** a) ~> b'
eval' b ~> b'
b Unit ~> Unit
forall k. Monoidal k => Obj Unit
unitObj) ((((a' ~~> Unit) ** a) ** ((b' ~~> Unit) ** b)) ~> (Unit ** Unit))
-> ((((a' ~~> Unit) ** (b' ~~> Unit)) ** (a ** b))
    ~> (((a' ~~> Unit) ** a) ** ((b' ~~> Unit) ** b)))
-> (((a' ~~> Unit) ** (b' ~~> Unit)) ** (a ** b)) ~> (Unit ** 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
. ((a' ~~> Unit) ~> (a' ~~> Unit))
-> ((b' ~~> Unit) ~> (b' ~~> Unit))
-> (a ~> a)
-> (b ~> b)
-> (((a' ~~> Unit) ** (b' ~~> Unit)) ** (a ** b))
   ~> (((a' ~~> Unit) ** a) ** ((b' ~~> Unit) ** b))
forall k (a :: k) (a' :: k) (b :: k) (b' :: k) (c :: k) (c' :: k)
       (d :: k) (d' :: k).
SymMonoidal k =>
(a ~> a')
-> (b ~> b')
-> (c ~> c')
-> (d ~> d')
-> ((a ** b) ** (c ** d)) ~> ((a' ** c') ** (b' ** d'))
swapInner' (a' ~~> Unit) ~> (a' ~~> Unit)
(a' ~~> Bottom) ~> (a' ~~> Bottom)
dualA (b' ~~> Unit) ~> (b' ~~> Unit)
(b' ~~> Bottom) ~> (b' ~~> Bottom)
dualB ((a ~> a') -> a ~> a
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src a ~> a'
a) ((b ~> b') -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src b ~> b'
b))

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 (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @_ @(a ** b) @Unit ((Unit ** Unit) ~> Unit
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor ((Unit ** Unit) ~> Unit)
-> ((((a ~~> Unit) ** (b ~~> Unit)) ** (a ** b)) ~> (Unit ** Unit))
-> (((a ~~> Unit) ** (b ~~> Unit)) ** (a ** b)) ~> 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).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
forall {k} (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
eval @a @Unit (((a ~~> Unit) ** a) ~> Unit)
-> (((b ~~> Unit) ** b) ~> Unit)
-> (((a ~~> Unit) ** a) ** ((b ~~> Unit) ** b)) ~> (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)
`par` forall (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
forall {k} (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
eval @b @Unit) ((((a ~~> Unit) ** a) ** ((b ~~> Unit) ** b)) ~> (Unit ** Unit))
-> ((((a ~~> Unit) ** (b ~~> Unit)) ** (a ** b))
    ~> (((a ~~> Unit) ** a) ** ((b ~~> Unit) ** b)))
-> (((a ~~> Unit) ** (b ~~> Unit)) ** (a ** b)) ~> (Unit ** 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) (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 @(Dual a) @(Dual b) @a @b)
  ((Ob Unit, Ob Unit) =>
 ((a ~~> Unit) ** (b ~~> Unit)) ~> ((a ** b) ~~> Unit))
-> (Unit ~> Unit)
-> ((a ~~> Unit) ** (b ~~> Unit)) ~> ((a ** 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
\\ forall k. Monoidal k => Obj Unit
unitObj @k
  ((Ob (a ** b), Ob (a ** b)) =>
 ((a ~~> Unit) ** (b ~~> Unit)) ~> ((a ** b) ~~> Unit))
-> ((a ** b) ~> (a ** b))
-> ((a ~~> Unit) ** (b ~~> Unit)) ~> ((a ** 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
\\ (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (b ~> b) -> (a ** b) ~> (a ** b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b)
  ((Ob ((a ~~> Unit) ** (b ~~> Unit)),
  Ob ((a ~~> Unit) ** (b ~~> Unit))) =>
 ((a ~~> Unit) ** (b ~~> Unit)) ~> ((a ** b) ~~> Unit))
-> (((a ~~> Unit) ** (b ~~> Unit))
    ~> ((a ~~> Unit) ** (b ~~> Unit)))
-> ((a ~~> Unit) ** (b ~~> Unit)) ~> ((a ** 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
\\ (forall (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
dual @a ((a ~~> Unit) ~> (a ~~> Unit))
-> ((b ~~> Unit) ~> (b ~~> Unit))
-> ((a ~~> Unit) ** (b ~~> 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). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
dual @b)
  ((Ob (a ~~> Unit), Ob (a ~~> Unit)) =>
 ((a ~~> Unit) ** (b ~~> Unit)) ~> ((a ** b) ~~> Unit))
-> ((a ~~> Unit) ~> (a ~~> Unit))
-> ((a ~~> Unit) ** (b ~~> Unit)) ~> ((a ** 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
\\ forall (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
dual @a ((Ob (b ~~> Unit), Ob (b ~~> Unit)) =>
 ((a ~~> Unit) ** (b ~~> Unit)) ~> ((a ** b) ~~> Unit))
-> ((b ~~> Unit) ~> (b ~~> Unit))
-> ((a ~~> Unit) ** (b ~~> Unit)) ~> ((a ** 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
\\ forall (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
dual @b

dualityUnit' :: forall {k} a. (CompactClosed k) => Obj a -> (Unit :: k) ~> a ** Dual a
dualityUnit' :: forall {k} (a :: k).
CompactClosed k =>
Obj a -> Unit ~> (a ** Dual a)
dualityUnit' Obj a
a =
  let dualA :: (a ~~> Bottom) ~> (a ~~> Bottom)
dualA = Obj a -> (a ~~> Bottom) ~> (a ~~> Bottom)
forall {k} (a :: k) (a' :: k).
StarAutonomous k =>
(a ~> a') -> Dual a' ~> Dual a
dual' Obj a
a
  in (Obj a -> Dual (a ~~> Bottom) ~> a
forall (a :: k) (a' :: k). (a ~> a') -> Dual (Dual a) ~> a'
forall k (a :: k) (a' :: k).
StarAutonomous k =>
(a ~> a') -> Dual (Dual a) ~> a'
doubleNeg' Obj a
a (((a ~~> Unit) ~~> Unit) ~> a)
-> ((a ~~> Unit) ~> (a ~~> Unit))
-> (((a ~~> Unit) ~~> Unit) ** (a ~~> Unit)) ~> (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)
`par` (a ~~> Unit) ~> (a ~~> Unit)
(a ~~> Bottom) ~> (a ~~> Bottom)
dualA) ((((a ~~> Unit) ~~> Unit) ** (a ~~> Unit)) ~> (a ** (a ~~> Unit)))
-> (Unit ~> (((a ~~> Unit) ~~> Unit) ** (a ~~> Unit)))
-> Unit ~> (a ** (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
. ((a ~~> Unit) ~> (a ~~> Unit))
-> Obj a
-> Dual ((a ~~> Unit) ** a)
   ~> (Dual (a ~~> Unit) ** (a ~~> Bottom))
forall (a :: k) (a' :: k) (b :: k) (b' :: k).
(a ~> a') -> (b ~> b') -> Dual (a' ** b') ~> (Dual a ** Dual b)
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
CompactClosed k =>
(a ~> a') -> (b ~> b') -> Dual (a' ** b') ~> (Dual a ** Dual b)
distribDual' (a ~~> Unit) ~> (a ~~> Unit)
(a ~~> Bottom) ~> (a ~~> Bottom)
dualA Obj a
a ((((a ~~> Unit) ** a) ~~> Unit)
 ~> (((a ~~> Unit) ~~> Unit) ** (a ~~> Unit)))
-> (Unit ~> (((a ~~> Unit) ** a) ~~> Unit))
-> Unit ~> (((a ~~> Unit) ~~> Unit) ** (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
. (Obj Unit
forall k. Monoidal k => Obj Unit
unitObj Obj Unit
-> (((a ~~> Unit) ** a) ~> Unit)
-> (Unit ~~> Unit) ~> (((a ~~> Unit) ** a) ~~> Unit)
forall (b :: k) (y :: k) (x :: k) (a :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (b :: k) (y :: k) (x :: k) (a :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ Obj a -> ((a ~~> Bottom) ** a) ~> Bottom
forall {k} (a :: k).
StarAutonomous k =>
Obj a -> (Dual a ** a) ~> Bottom
dualityCounit' Obj a
a) ((Unit ~~> Unit) ~> (((a ~~> Unit) ** a) ~~> Unit))
-> (Unit ~> (Unit ~~> Unit))
-> Unit ~> (((a ~~> Unit) ** 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
. Obj Unit -> Unit ~> (Unit ~~> Unit)
forall {k} (a :: k) (b :: k).
Closed k =>
(a ~> b) -> Unit ~> (a ~~> b)
mkExponential Obj Unit
forall k. Monoidal k => Obj Unit
unitObj

dualityUnit :: forall {k} a. (CompactClosed k, Ob a) => (Unit :: k) ~> a ** Dual a
dualityUnit :: forall {k} (a :: k).
(CompactClosed k, Ob a) =>
Unit ~> (a ** Dual a)
dualityUnit = Obj a -> Unit ~> (a ** (a ~~> Bottom))
forall {k} (a :: k).
CompactClosed k =>
Obj a -> Unit ~> (a ** Dual a)
dualityUnit' (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a)

compactClosedTrace :: forall {k} u (x :: k) y. (CompactClosed k, Ob x, Ob y, Ob u) => x ** u ~> y ** u -> x ~> y
compactClosedTrace :: forall {k} (u :: k) (x :: k) (y :: k).
(CompactClosed k, Ob x, Ob y, Ob u) =>
((x ** u) ~> (y ** u)) -> x ~> y
compactClosedTrace (x ** u) ~> (y ** u)
f =
  let u :: Obj u
u = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @u; y :: Obj y
y = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @y; x :: Obj x
x = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x; dualU :: Obj (Dual u)
dualU = forall (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
dual @u
  in (y ** Unit) ~> y
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor
      ((y ** Unit) ~> y) -> (x ~> (y ** Unit)) -> x ~> y
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
. (Obj y
y Obj y
-> ((u ** (u ~~> Unit)) ~> Unit)
-> (y ** (u ** (u ~~> Unit))) ~> (y ** 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` (Obj (u ~~> Unit) -> (Dual (u ~~> Unit) ** (u ~~> Unit)) ~> Bottom
forall {k} (a :: k).
StarAutonomous k =>
Obj a -> (Dual a ** a) ~> Bottom
dualityCounit' Obj (u ~~> Unit)
Obj (Dual u)
dualU ((((u ~~> Unit) ~~> Unit) ** (u ~~> Unit)) ~> Unit)
-> ((u ** (u ~~> Unit))
    ~> (((u ~~> Unit) ~~> Unit) ** (u ~~> Unit)))
-> (u ** (u ~~> Unit)) ~> 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
. (Obj u -> (Unit ~> Unit) -> u ~> ((u ~~> Unit) ~~> Unit)
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
(Closed k, SymMonoidal k) =>
(a ~> a') -> (b ~> b') -> a ~> ((a' ~~> b) ~~> b')
doubleNegInv' Obj u
u Unit ~> Unit
forall k. Monoidal k => Obj Unit
unitObj (u ~> ((u ~~> Unit) ~~> Unit))
-> Obj (u ~~> Unit)
-> (u ** (u ~~> Unit)) ~> (((u ~~> Unit) ~~> Unit) ** (u ~~> 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` Obj (u ~~> Unit)
Obj (Dual u)
dualU)))
      ((y ** (u ** (u ~~> Unit))) ~> (y ** Unit))
-> (x ~> (y ** (u ** (u ~~> Unit)))) -> x ~> (y ** 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 k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @y @u @(Dual u)
      (((y ** u) ** (u ~~> Unit)) ~> (y ** (u ** (u ~~> Unit))))
-> (x ~> ((y ** u) ** (u ~~> Unit)))
-> x ~> (y ** (u ** (u ~~> 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
. ((x ** u) ~> (y ** u)
f ((x ** u) ~> (y ** u))
-> Obj (u ~~> Unit)
-> ((x ** u) ** (u ~~> Unit)) ~> ((y ** u) ** (u ~~> 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` Obj (u ~~> Unit)
Obj (Dual u)
dualU)
      (((x ** u) ** (u ~~> Unit)) ~> ((y ** u) ** (u ~~> Unit)))
-> (x ~> ((x ** u) ** (u ~~> Unit)))
-> x ~> ((y ** u) ** (u ~~> 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 k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @x @u @(Dual u)
      ((x ** (u ** (u ~~> Unit))) ~> ((x ** u) ** (u ~~> Unit)))
-> (x ~> (x ** (u ** (u ~~> Unit))))
-> x ~> ((x ** u) ** (u ~~> 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
. (Obj x
x Obj x
-> (Unit ~> (u ** (u ~~> Unit)))
-> (x ** Unit) ~> (x ** (u ** (u ~~> 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). (CompactClosed k, Ob a) => Unit ~> (a ** Dual a)
forall {k} (a :: k).
(CompactClosed k, Ob a) =>
Unit ~> (a ** Dual a)
dualityUnit @u)
      ((x ** Unit) ~> (x ** (u ** (u ~~> Unit))))
-> (x ~> (x ** Unit)) -> x ~> (x ** (u ** (u ~~> 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
. x ~> (x ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv
      ((Ob (u ~~> Unit), Ob (u ~~> Unit)) => x ~> y)
-> Obj (u ~~> Unit) -> x ~> y
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
\\ Obj (u ~~> Unit)
Obj (Dual u)
dualU

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