{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Object.Dual where

import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , SymMonoidal (..)
  , associator
  , leftUnitorWith
  , rightUnitorInvWith
  , rightUnitorWith
  , swap
  )
import Proarrow.Core (CategoryOf (..), Obj, Profunctor (..), Promonad (..), obj)
import Proarrow.Object.Exponential (Closed (..))

class (Ob (Dual a)) => ObDual (a :: k)
instance (Ob (Dual a)) => ObDual (a :: k)

class (SymMonoidal k, Closed k, forall (a :: k). (Ob a) => ObDual a, Ob (Unit :: k)) => StarAutonomous k where
  type Dual (a :: k) :: k
  dual :: (a :: k) ~> b -> Dual b ~> Dual a
  dualInv :: (Ob (a :: k), Ob b) => Dual a ~> Dual b -> b ~> a
  linDist :: (Ob (a :: k), Ob b, Ob c) => a ** b ~> Dual c -> a ~> Dual (b ** c)
  linDistInv :: (Ob (a :: k), Ob b, Ob c) => a ~> Dual (b ** c) -> a ** b ~> Dual c

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

doubleNeg :: forall {k} (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
doubleNeg :: forall {k} (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
doubleNeg = forall k (a :: k) (b :: k).
(StarAutonomous k, Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv @k @a (forall (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
doubleNegInv @(Dual a))

doubleNegInv :: forall {k} (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
doubleNegInv :: forall {k} (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
doubleNegInv = forall k (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @k @Unit @a @(Dual a) (((a ** Dual a) ~> (Dual a ** a))
-> Dual (Dual a ** a) ~> Dual (a ** Dual a)
forall (a :: k) (b :: k). (a ~> b) -> Dual b ~> Dual a
forall k (a :: k) (b :: k).
StarAutonomous k =>
(a ~> b) -> Dual b ~> Dual a
dual (forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @a @(Dual a)) (Dual (Dual a ** a) ~> Dual (a ** Dual a))
-> (Unit ~> Dual (Dual a ** a)) -> Unit ~> Dual (a ** Dual a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k).
(StarAutonomous k, Ob a) =>
Unit ~> Dual (Dual a ** a)
forall {k} (a :: k).
(StarAutonomous k, Ob a) =>
Unit ~> Dual (Dual a ** a)
dualityUnitSA @a) ((Unit ** a) ~> Dual (Dual a))
-> (a ~> (Unit ** a)) -> a ~> Dual (Dual a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @k @a

type ExpSA a b = Dual (a ** Dual b)

currySA :: forall {k} (a :: k) b c. (StarAutonomous k, Ob a, Ob b) => a ** b ~> c -> a ~> ExpSA b c
currySA :: forall {k} (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> ExpSA b c
currySA (a ** b) ~> c
f = 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 c) (forall (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
doubleNegInv @c (c ~> Dual (Dual c))
-> ((a ** b) ~> c) -> (a ** b) ~> Dual (Dual c)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ** b) ~> c
f) ((Ob (a ** b), Ob c) => a ~> Dual (b ** Dual c))
-> ((a ** b) ~> c) -> a ~> Dual (b ** Dual c)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (a ** b) ~> c
f

uncurrySA :: forall {k} (a :: k) b c. (StarAutonomous k, Ob b, Ob c) => a ~> ExpSA b c -> a ** b ~> c
uncurrySA :: forall {k} (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob b, Ob c) =>
(a ~> ExpSA b c) -> (a ** b) ~> c
uncurrySA a ~> ExpSA b c
f = forall (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
forall {k} (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
doubleNeg @c (Dual (Dual c) ~> c)
-> ((a ** b) ~> Dual (Dual c)) -> (a ** b) ~> c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @k @a @b @(Dual c) a ~> ExpSA b c
f ((Ob a, Ob (ExpSA b c)) => (a ** b) ~> c)
-> (a ~> ExpSA b c) -> (a ** b) ~> c
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> ExpSA b c
f

expSA :: forall {k} (a :: k) b x y. (StarAutonomous k) => b ~> y -> x ~> a -> ExpSA a b ~> ExpSA x y
expSA :: forall {k} (a :: k) (b :: k) (x :: k) (y :: k).
StarAutonomous k =>
(b ~> y) -> (x ~> a) -> ExpSA a b ~> ExpSA x y
expSA b ~> y
f x ~> a
g = ((x ** Dual y) ~> (a ** Dual b))
-> Dual (a ** Dual b) ~> Dual (x ** Dual y)
forall (a :: k) (b :: k). (a ~> b) -> Dual b ~> Dual a
forall k (a :: k) (b :: k).
StarAutonomous k =>
(a ~> b) -> Dual b ~> Dual a
dual (x ~> a
g (x ~> a) -> (Dual y ~> Dual b) -> (x ** Dual y) ~> (a ** Dual 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 ~> y) -> Dual y ~> Dual b
forall (a :: k) (b :: k). (a ~> b) -> Dual b ~> Dual a
forall k (a :: k) (b :: k).
StarAutonomous k =>
(a ~> b) -> Dual b ~> Dual a
dual b ~> y
f)

dualityUnitSA :: forall {k} (a :: k). (StarAutonomous k, Ob a) => Unit ~> Dual (Dual a ** a)
dualityUnitSA :: forall {k} (a :: k).
(StarAutonomous k, Ob a) =>
Unit ~> Dual (Dual a ** a)
dualityUnitSA = 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 a) @a (Unit ** Dual a) ~> Dual a
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor

dualityCounitSA :: forall {k} (a :: k). (StarAutonomous k, Ob a) => Dual a ** a ~> Dual Unit
dualityCounitSA :: forall {k} (a :: k).
(StarAutonomous k, Ob a) =>
(Dual a ** a) ~> Dual Unit
dualityCounitSA = forall k (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @k @(Dual a) @a @Unit (((a ** Unit) ~> a) -> Dual a ~> Dual (a ** Unit)
forall (a :: k) (b :: k). (a ~> b) -> Dual b ~> Dual a
forall k (a :: k) (b :: k).
StarAutonomous k =>
(a ~> b) -> Dual b ~> Dual a
dual (forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor @k @a))

instance StarAutonomous () where
  type Dual '() = '()
  dual :: forall (a :: ()) (b :: ()). (a ~> b) -> Dual b ~> Dual a
dual a ~> b
Unit a b
U.Unit = Dual b ~> Dual a
Unit '() '()
U.Unit
  dualInv :: forall (a :: ()) (b :: ()).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv Dual a ~> Dual b
Unit '() '()
U.Unit = b ~> a
Unit '() '()
U.Unit
  linDist :: forall (a :: ()) (b :: ()) (c :: ()).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist (a ** b) ~> Dual c
Unit '() '()
U.Unit = a ~> Dual (b ** c)
Unit '() '()
U.Unit
  linDistInv :: forall (a :: ()) (b :: ()) (c :: ()).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv a ~> Dual (b ** c)
Unit '() '()
U.Unit = (a ** b) ~> Dual c
Unit '() '()
U.Unit

instance (StarAutonomous j, StarAutonomous k) => StarAutonomous (j, k) where
  type Dual '(a, b) = '(Dual a, Dual b)
  dual :: forall (a :: (j, k)) (b :: (j, k)). (a ~> b) -> Dual b ~> Dual a
dual (a1 ~> b1
f :**: a2 ~> b2
g) = (a1 ~> b1) -> Dual b1 ~> Dual a1
forall (a :: j) (b :: j). (a ~> b) -> Dual b ~> Dual a
forall k (a :: k) (b :: k).
StarAutonomous k =>
(a ~> b) -> Dual b ~> Dual a
dual a1 ~> b1
f (Dual b1 ~> Dual a1)
-> (Dual b2 ~> Dual a2)
-> (:**:) (~>) (~>) '(Dual b1, Dual b2) '(Dual a1, Dual a2)
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)
:**: (a2 ~> b2) -> Dual b2 ~> Dual a2
forall (a :: k) (b :: k). (a ~> b) -> Dual b ~> Dual a
forall k (a :: k) (b :: k).
StarAutonomous k =>
(a ~> b) -> Dual b ~> Dual a
dual a2 ~> b2
g
  dualInv :: forall (a :: (j, k)) (b :: (j, k)).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv (a1 ~> b1
f :**: a2 ~> b2
g) = (Dual (Fst a) ~> Dual (Fst b)) -> Fst b ~> Fst a
forall (a :: j) (b :: j).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
forall k (a :: k) (b :: k).
(StarAutonomous k, Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv a1 ~> b1
Dual (Fst a) ~> Dual (Fst b)
f (Fst b ~> Fst a)
-> (Snd b ~> Snd a)
-> (:**:) (~>) (~>) '(Fst b, Snd b) '(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)
:**: (Dual (Snd a) ~> Dual (Snd b)) -> Snd b ~> Snd a
forall (a :: k) (b :: k).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
forall k (a :: k) (b :: k).
(StarAutonomous k, Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv a2 ~> b2
Dual (Snd a) ~> Dual (Snd b)
g
  linDist :: forall (a :: (j, k)) (b :: (j, k)) (c :: (j, k)).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @'(a1, a2) @'(b1, b2) @'(c1, c2) (a1 ~> b1
f :**: a2 ~> b2
g) = 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 @j @a1 @b1 @c1 a1 ~> b1
(Fst a ** Fst b) ~> Dual (Fst c)
f (Fst a ~> Dual (Fst b ** Fst c))
-> (Snd a ~> Dual (Snd b ** Snd c))
-> (:**:)
     (~>)
     (~>)
     '(Fst a, Snd a)
     '(Dual (Fst b ** Fst c), Dual (Snd b ** Snd c))
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall k (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @k @a2 @b2 @c2 a2 ~> b2
(Snd a ** Snd b) ~> Dual (Snd c)
g
  linDistInv :: forall (a :: (j, k)) (b :: (j, k)) (c :: (j, k)).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @'(a1, a2) @'(b1, b2) @'(c1, c2) (a1 ~> b1
f :**: a2 ~> b2
g) = forall k (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @j @a1 @b1 @c1 a1 ~> b1
Fst a ~> Dual (Fst b ** Fst c)
f ((Fst a ** Fst b) ~> Dual (Fst c))
-> ((Snd a ** Snd b) ~> Dual (Snd c))
-> (:**:)
     (~>)
     (~>)
     '(Fst a ** Fst b, Snd a ** Snd b)
     '(Dual (Fst c), Dual (Snd c))
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: forall k (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @k @a2 @b2 @c2 a2 ~> b2
Snd a ~> Dual (Snd b ** Snd c)
g

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

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 = (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)
-> (Dual a ~> 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)
`par` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Dual a)) ((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 :: 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 @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 :: PRO 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

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 :: PRO 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

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 :: PRO 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

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) (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 :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @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 :: 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 @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 :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @(Dual a ** Dual b) @a
    )
    ((Ob (Dual a ** Dual b), Ob (Dual a ** Dual b)) =>
 (Dual a ** Dual b) ~> Dual (a ** b))
-> ((Dual a ** Dual b) ~> (Dual a ** Dual b))
-> (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 :: 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 @(Dual a) Obj (Dual a)
-> (Dual b ~> Dual b) -> (Dual a ** Dual b) ~> (Dual a ** Dual 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 @(Dual b)

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 =
  ((u ** Dual u) ~> Unit) -> (y ** (u ** Dual u)) ~> y
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 @u ((Dual u ** u) ~> Unit)
-> ((u ** Dual u) ~> (Dual u ** u)) -> (u ** Dual 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 (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall {k} (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @u @(Dual u))
    ((y ** (u ** Dual u)) ~> y)
-> (x ~> (y ** (u ** Dual u))) -> 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
. 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) ** Dual u) ~> (y ** (u ** Dual u)))
-> (x ~> ((y ** u) ** Dual u)) -> x ~> (y ** (u ** Dual u))
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))
-> (Dual u ~> Dual u)
-> ((x ** u) ** Dual u) ~> ((y ** u) ** Dual u)
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 @(Dual u))
    (((x ** u) ** Dual u) ~> ((y ** u) ** Dual u))
-> (x ~> ((x ** u) ** Dual u)) -> x ~> ((y ** u) ** Dual u)
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 ** Dual u)) ~> ((x ** u) ** Dual u))
-> (x ~> (x ** (u ** Dual u))) -> x ~> ((x ** u) ** Dual u)
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
. (Unit ~> (u ** Dual u)) -> x ~> (x ** (u ** Dual u))
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(Unit ~> b) -> a ~> (a ** b)
rightUnitorInvWith (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)

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