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

module Proarrow.Category.Monoidal.StarAutonomous where

import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..), swap)
import Proarrow.Category.Monoidal.Closed (Closed (..))
import Proarrow.Category.Monoidal.Strictified (Strictified (..))
import Proarrow.Core (CategoryOf (..), Obj, Profunctor (..), Promonad (..), obj)
import Proarrow.Optic (Iso, iso)

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

class (SymMonoidal k, Closed k, Ob (Unit :: k), forall (a :: k). (Ob a) => ObDual a) => 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)) ((Ob (Dual (Dual a)), Ob (Dual (Dual a))) => Dual (Dual a) ~> a)
-> (Dual (Dual a) ~> Dual (Dual a)) -> Dual (Dual a) ~> 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
\\ forall (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
dualObj @(Dual a) ((Ob (Dual a), Ob (Dual a)) => Dual (Dual a) ~> a)
-> (Dual a ~> Dual a) -> Dual (Dual a) ~> 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
\\ forall (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
dualObj @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 k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @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 :: 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 :: 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
    ((Ob (Dual a), Ob (Dual a)) => a ~> Dual (Dual a))
-> (Dual a ~> Dual a) -> a ~> Dual (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
\\ forall (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => Obj (Dual a)
dualObj @a

doubleNegIso
  :: forall {k} (a :: k) (a' :: k). (StarAutonomous k, Ob a, Ob a') => Iso a a' (Dual (Dual a)) (Dual (Dual a'))
doubleNegIso :: forall {k} (a :: k) (a' :: k).
(StarAutonomous k, Ob a, Ob a') =>
Iso a a' (Dual (Dual a)) (Dual (Dual a'))
doubleNegIso = (a ~> Dual (Dual a))
-> (Dual (Dual a') ~> a')
-> Optic_ (OPT (Dual (Dual a)) (Dual (Dual a'))) (OPT a a')
forall {j} {k} (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k) =>
(s ~> a) -> (b ~> t) -> Iso s t a b
iso a ~> Dual (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
doubleNegInv Dual (Dual a') ~> a'
forall {k} (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
doubleNeg

linDistS
  :: forall {k} (a :: k) (b :: k) c. (StarAutonomous k, Ob c) => '[a, b] ~> '[Dual c] -> '[a] ~> '[Dual (b ** c)]
linDistS :: forall {k} (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob c) =>
('[a, b] ~> '[Dual c]) -> '[a] ~> '[Dual (b ** c)]
linDistS f :: '[a, b] ~> '[Dual c]
f@Str{} = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @b @c ((Fold '[a] ~> Fold '[Dual (b ** c)])
-> Strictified '[a] '[Dual (b ** c)]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str (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 @c (Strictified '[a, b] '[Dual c] -> Fold '[a, b] ~> Fold '[Dual c]
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
unStr '[a, b] ~> '[Dual c]
Strictified '[a, b] '[Dual c]
f)))

linDistInvS
  :: forall {k} (a :: k) (b :: k) c. (StarAutonomous k, Ob b, Ob c) => '[a] ~> '[Dual (b ** c)] -> '[a, b] ~> '[Dual c]
linDistInvS :: forall {k} (a :: k) (b :: k) (c :: k).
(StarAutonomous k, Ob b, Ob c) =>
('[a] ~> '[Dual (b ** c)]) -> '[a, b] ~> '[Dual c]
linDistInvS f :: '[a] ~> '[Dual (b ** c)]
f@Str{} = (Fold '[a, b] ~> Fold '[Dual c]) -> Strictified '[a, b] '[Dual c]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str (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 @c (Strictified '[a] '[Dual (b ** c)]
-> Fold '[a] ~> Fold '[Dual (b ** c)]
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
unStr '[a] ~> '[Dual (b ** c)]
Strictified '[a] '[Dual (b ** c)]
f))

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 :: 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 :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (a ** b) ~> c
f ((Ob (Dual c), Ob (Dual (a ** b))) => a ~> Dual (b ** Dual c))
-> (Dual c ~> Dual (a ** b)) -> a ~> Dual (b ** Dual c)
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
\\ ((a ** b) ~> c) -> Dual c ~> Dual (a ** 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 (a ** b) ~> c
f

applySA :: forall {k} (b :: k) c. (StarAutonomous k, Ob b, Ob c) => ExpSA b c ** b ~> c
applySA :: forall {k} (b :: k) (c :: k).
(StarAutonomous k, Ob b, Ob c) =>
(ExpSA b c ** b) ~> c
applySA =
  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)
-> ((Dual (b ** Dual c) ** b) ~> Dual (Dual c))
-> (Dual (b ** Dual c) ** b) ~> c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @b @(Dual 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 @(ExpSA b c) @b @(Dual c) Dual (b ** Dual c) ~> Dual (b ** Dual c)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id ((Ob (Dual (b ** Dual c)), Ob (Dual (b ** Dual c))) =>
 (Dual (b ** Dual c) ** b) ~> Dual (Dual c))
-> (Dual (b ** Dual c) ~> Dual (b ** Dual c))
-> (Dual (b ** Dual c) ** b) ~> Dual (Dual c)
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 @(b ** Dual c))
    ((Ob (Dual c), Ob (Dual c)) => (Dual (b ** Dual c) ** b) ~> c)
-> (Dual c ~> Dual c) -> (Dual (b ** Dual c) ** b) ~> c
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 @c

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

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)) ((Ob (Dual a), Ob (Dual a)) => (Dual a ** a) ~> Dual Unit)
-> (Dual a ~> Dual a) -> (Dual a ** a) ~> 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 @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