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

-- | Star-autonomous categories: symmetric closed categories with a dualizing functor 'Dual', where
-- morphisms @a ** b ~> Dual c@ correspond to @a ~> Dual (b ** c)@ ('linDist'). This gives
-- double-negation elimination ('doubleNeg') and an internal hom @'ExpSA' a b = 'Dual' (a ** Dual b)@
-- Star-autonomous categories are the categorical semantics of multiplicative linear logic.
module Proarrow.Category.Monoidal.StarAutonomous where

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

import Proarrow.Category.Instance.Bool (BOOL (..), Booleans (..), Not)
import Proarrow.Category.Instance.Free
  ( Elem (..)
  , Elems
  , FREE (..)
  , Free (..)
  , HasStructure (..)
  , IsFreeOb (..)
  , Lower
  , WithShow
  , withLowerOb
  )
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..), swap, type (**!))
import Proarrow.Category.Monoidal.Closed (Closed (..))
import Proarrow.Category.Monoidal.Strictified (Strictified (..), obj1, singleton)
import Proarrow.Core (CAT, CategoryOf (..), Kind, Obj, Profunctor (..), Promonad (..), obj)
import Proarrow.Optic (PIso, iso)
import Proarrow.Tools.Laws
  ( Bijection (..)
  , Inverses (..)
  , Law (..)
  , Laws (..)
  , bijection
  , inverses
  , (===)
  )

-- | A *-autonomous category: a symmetric monoidal closed category with a dualizing object, so
-- that 'Dual' is a contravariant involution and @Hom(a '**' b, 'Dual' c)@ is symmetric in its three
-- arguments.
--
-- __Laws:__
--
-- * 'dual' is a contravariant functor: @'dual' 'id' = 'id'@ and @'dual' (f . g) = 'dual' g . 'dual' f@
-- * 'dual' and 'dualInv' are mutually inverse bijections on hom-sets:
--   @'dualInv' ('dual' f) = f@ and @'dual' ('dualInv' g) = g@
-- * 'linDist' and 'linDistInv' are mutually inverse, giving
--   @Hom(a '**' b, 'Dual' c) ≅ Hom(a, 'Dual' (b '**' c))@, natural in all three variables
-- * 'doubleNeg' and 'doubleNegInv' are mutually inverse, so @'Dual' ('Dual' a) ≅ a@, and
--   'doubleNegInv' is 'doubleNegInvDefault', the one the rest of the structure gives
--
-- Stated as code by the 'Proarrow.Tools.Laws.Laws' instance for 'StarAutonomousStructures', and
-- checked by @Proarrow.Testing.Laws.testStarAutonomous@.
class (SymMonoidal k, Closed k, Ob (Unit :: k)) => StarAutonomous k where
  -- | The dual of an object.
  type Dual (a :: k) :: k

  -- | Recovers @'Ob' ('Dual' a)@ from the objecthood of @a@.
  withObDual :: (Ob (a :: k)) => ((Ob (Dual a)) => r) -> r

  -- | 'Dual'\'s contravariant action on arrows.
  dual :: (a :: k) ~> b -> Dual b ~> Dual a

  -- | Inverse to 'dual' on hom-sets: recovers the undualized arrow.
  dualInv :: (Ob (a :: k), Ob b) => Dual a ~> Dual b -> b ~> a

  -- | Linear distribution: transposes a tensor factor across the dual.
  linDist :: (Ob (a :: k), Ob b, Ob c) => a ** b ~> Dual c -> a ~> Dual (b ** c)

  -- | Inverse to 'linDist'.
  linDistInv :: (Ob (a :: k), Ob b, Ob c) => a ~> Dual (b ** c) -> a ** b ~> Dual c

  -- | Double-negation elimination. Defaults to 'doubleNegDefault'; an instance whose double dual
  -- is the object itself can say so directly.
  doubleNeg :: (Ob (a :: k)) => Dual (Dual a) ~> a
  doubleNeg @a = forall (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
forall {k} (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
doubleNegDefault @a

  -- | Double-negation introduction, inverse to 'doubleNeg'. Defaults to 'doubleNegInvDefault'.
  doubleNegInv :: (Ob (a :: k)) => a ~> Dual (Dual a)
  doubleNegInv @a = forall (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
doubleNegInvDefault @a

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' from the rest of the structure: 'dualInv' of 'doubleNegInv' at the dual.
doubleNegDefault :: forall {k} (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
doubleNegDefault :: forall {k} (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
doubleNegDefault = forall k (a :: k) (b :: k).
(StarAutonomous k, Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv @k @a (forall k (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
doubleNegInv @k @(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' from the rest of the structure, through 'linDistInv' and the duality unit.
doubleNegInvDefault :: forall {k} (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
doubleNegInvDefault :: forall {k} (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
doubleNegInvDefault =
  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 :: 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) ((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 :: 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 @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') => PIso a a' (Dual (Dual a)) (Dual (Dual a'))
doubleNegIso :: forall {k} (a :: k) (a' :: k).
(StarAutonomous k, Ob a, Ob a') =>
PIso 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} (c :: (j +-> k) -> Constraint) (s :: k) (t :: j)
       (a :: k) (b :: j).
(CategoryOf j, CategoryOf k) =>
(s ~> a) -> (b ~> t) -> Optic c s t a b
iso a ~> Dual (Dual a)
forall (a :: k). Ob a => a ~> Dual (Dual a)
forall k (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
doubleNegInv Dual (Dual a') ~> a'
forall (a :: k). Ob a => 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{} = (a ~> Dual (b ** c)) -> '[a] ~> '[Dual (b ** c)]
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> '[a] ~> '[b]
singleton (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{} = forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @k @c ((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)) ((Ob '[Dual c], Ob '[Dual c]) => Strictified '[a, b] '[Dual c])
-> Strictified '[Dual c] '[Dual c] -> Strictified '[a, b] '[Dual c]
forall (a :: [k]) (b :: [k]) r.
((Ob a, Ob b) => r) -> Strictified 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). (Monoidal k, Ob a) => Obj '[a]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 @(Dual c))

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 k (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
doubleNegInv @k @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 :: CAT 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 k (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
doubleNeg @k @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 :: 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) 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 :: CAT 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 '() = '()
  withObDual :: forall (a :: ()) r. Ob a => (Ob (Dual a) => r) -> r
withObDual Ob (Dual a) => r
r = r
Ob (Dual a) => r
r
  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
  doubleNeg :: forall (a :: ()). Ob a => Dual (Dual a) ~> a
doubleNeg = Dual (Dual a) ~> a
Unit '() '()
U.Unit
  doubleNegInv :: forall (a :: ()). Ob a => a ~> Dual (Dual a)
doubleNegInv = a ~> Dual (Dual a)
Unit '() '()
U.Unit

instance StarAutonomous BOOL where
  type Dual (a :: BOOL) = Not a
  withObDual :: forall (a :: BOOL) r. Ob a => (Ob (Dual a) => r) -> r
withObDual Ob (Dual a) => r
r = r
Ob (Dual a) => r
r
  dual :: forall (a :: BOOL) (b :: BOOL). (a ~> b) -> Dual b ~> Dual a
dual a ~> b
Booleans a b
Fls = Dual b ~> Dual a
Booleans 'TRU 'TRU
Tru
  dual a ~> b
Booleans a b
F2T = Dual b ~> Dual a
Booleans 'FLS 'TRU
F2T
  dual a ~> b
Booleans a b
Tru = Dual b ~> Dual a
Booleans 'FLS 'FLS
Fls
  dualInv :: forall (a :: BOOL) (b :: BOOL).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv @a @b Dual a ~> Dual b
f = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @b, Dual a ~> Dual b
Booleans (Not a) (Not b)
f) of
    (Booleans a a
Fls, Booleans b b
Fls, Booleans 'TRU 'TRU
Booleans (Not a) (Not b)
Tru) -> b ~> a
Booleans 'FLS 'FLS
Fls
    (Booleans a a
Tru, Booleans b b
Fls, Booleans 'FLS 'TRU
Booleans (Not a) (Not b)
F2T) -> b ~> a
Booleans 'FLS 'TRU
F2T
    (Booleans a a
Tru, Booleans b b
Tru, Booleans 'FLS 'FLS
Booleans (Not a) (Not b)
Fls) -> b ~> a
Booleans 'TRU 'TRU
Tru
    (Booleans a a
Fls, Booleans b b
Tru, Booleans (Not a) (Not b)
f') -> case Booleans (Not a) (Not b)
f' of {}
  linDist :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @a @b (a ** b) ~> Dual c
f = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @b) of
    (Booleans a a
Fls, Booleans b b
Fls) -> a ~> Dual (b ** c)
Booleans 'FLS 'TRU
F2T
    (Booleans a a
Tru, Booleans b b
Fls) -> a ~> Dual (b ** c)
Booleans 'TRU 'TRU
Tru
    (Booleans a a
_, Booleans b b
Tru) -> a ~> Dual (b ** c)
(a ** b) ~> Dual c
f
  linDistInv :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @_ @b @c a ~> Dual (b ** c)
f = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @b, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @c) of
    (Booleans b b
Fls, Booleans c c
Fls) -> (a ** b) ~> Dual c
Booleans 'FLS 'TRU
F2T
    (Booleans b b
Fls, Booleans c c
Tru) -> (a ** b) ~> Dual c
Booleans 'FLS 'FLS
Fls
    (Booleans b b
Tru, Booleans c c
_) -> a ~> Dual (b ** c)
(a ** b) ~> Dual c
f
  doubleNeg :: forall (a :: BOOL). Ob a => Dual (Dual a) ~> a
doubleNeg @a = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a of Obj a
Booleans a a
Fls -> Dual (Dual a) ~> a
Booleans 'FLS 'FLS
Fls; Obj a
Booleans a a
Tru -> Dual (Dual a) ~> a
Booleans 'TRU 'TRU
Tru
  doubleNegInv :: forall (a :: BOOL). Ob a => a ~> Dual (Dual a)
doubleNegInv @a = case forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a of Obj a
Booleans a a
Fls -> a ~> Dual (Dual a)
Booleans 'FLS 'FLS
Fls; Obj a
Booleans a a
Tru -> a ~> Dual (Dual a)
Booleans 'TRU 'TRU
Tru

-- BOOL is not CompactClosed

instance (StarAutonomous j, StarAutonomous k) => StarAutonomous (j, k) where
  type Dual '(a, b) = '(Dual a, Dual b)
  withObDual :: forall (a :: (j, k)) r. Ob a => (Ob (Dual a) => r) -> r
withObDual @'(a, b) Ob (Dual a) => r
r = forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @j @a (forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @k @b r
Ob (Dual (Snd @ a)) => r
Ob (Dual a) => r
r)
  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
  doubleNeg :: forall (a :: (j, k)). Ob a => Dual (Dual a) ~> a
doubleNeg @'(a, b) = forall k (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
doubleNeg @j @a (Dual (Dual (Fst @ a)) ~> (Fst @ a))
-> (Dual (Dual (Snd @ a)) ~> (Snd @ a))
-> (:**:)
     (~>)
     (~>)
     '(Dual (Dual (Fst @ a)), Dual (Dual (Snd @ a)))
     '(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)
:**: forall k (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
doubleNeg @k @b
  doubleNegInv :: forall (a :: (j, k)). Ob a => a ~> Dual (Dual a)
doubleNegInv @'(a, b) = forall k (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
doubleNegInv @j @a ((Fst @ a) ~> Dual (Dual (Fst @ a)))
-> ((Snd @ a) ~> Dual (Dual (Snd @ a)))
-> (:**:)
     (~>)
     (~>)
     '(Fst @ a, Snd @ a)
     '(Dual (Dual (Fst @ a)), Dual (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). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
doubleNegInv @k @b

data family DualF (a :: k) :: k
instance (IsFreeOb (a :: FREE cs p), StarAutonomous `Elem` cs) => IsFreeOb (DualF a) where
  type Lower f (DualF a) = Dual (Lower f a)
  lowerOb :: forall k' (f :: k +-> k') r.
(Representable f, All cs k') =>
(Ob (Lower f (DualF a)) => r) -> r
lowerOb @k' @f Ob (Lower f (DualF a)) => r
r = forall (c :: Type -> Constraint) (cs :: [Type -> Constraint]) k r.
(Elem c cs, All cs k) =>
(c k => r) -> r
fromAll @StarAutonomous @cs @k' (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 (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @k' @(Lower f a) r
Ob (Lower f (DualF a)) => r
Ob (Dual (Lower f a)) => r
r))

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

instance
  (StarAutonomousStructures `Elems` cs)
  => HasStructure cs (p :: CAT k) StarAutonomous
  where
  data Struct StarAutonomous a b where
    Dual :: a ~> b -> Struct StarAutonomous (DualF b) (DualF a)
    DualInv :: (Ob a, Ob b) => DualF a ~> DualF b -> Struct StarAutonomous b a
    LinDist :: (Ob a, Ob b, Ob c) => a **! b ~> DualF c -> Struct StarAutonomous a (DualF (b **! c))
    LinDistInv :: (Ob a, Ob b, Ob c) => a ~> DualF (b **! c) -> Struct StarAutonomous (a **! b) (DualF c)
  foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p).
(StarAutonomous k', All cs k', Representable f) =>
(forall (x :: FREE cs p) (y :: FREE cs p).
 (x ~> y) -> Lower f x ~> Lower f y)
-> Struct StarAutonomous a b -> Lower f a ~> Lower f b
foldStructure forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go (Dual a ~> b
f) = (Lower f a ~> Lower f b) -> Dual (Lower f b) ~> Dual (Lower f 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 ((a ~> b) -> Lower f a ~> Lower f b
forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go a ~> b
f)
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go (DualInv @a @b DualF b ~> DualF a
g) =
    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).
(StarAutonomous k, Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv @_ @(Lower f a) @(Lower f b) ((DualF b ~> DualF a) -> Lower f (DualF b) ~> Lower f (DualF a)
forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go DualF b ~> DualF a
g)))
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go (LinDist @a @b @c (a **! b) ~> DualF c
g) =
    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} {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 @c (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 @_ @(Lower f a) @(Lower f b) @(Lower f c) (((a **! b) ~> DualF c) -> Lower f (a **! b) ~> Lower f (DualF c)
forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go (a **! b) ~> DualF c
g))))
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go (LinDistInv @a @b @c a ~> DualF (b **! c)
g) =
    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} {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 @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 @_ @(Lower f a) @(Lower f b) @(Lower f c) ((a ~> DualF (b **! c)) -> Lower f a ~> Lower f (DualF (b **! c))
forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go a ~> DualF (b **! c)
g))))
instance (WithShow a) => P.Show (Struct StarAutonomous a b) where
  showsPrec :: Int -> Struct StarAutonomous a b -> ShowS
showsPrec Int
d (Dual a ~> b
f) = Bool -> ShowS -> ShowS
P.showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
P.> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
P.$ String -> ShowS
P.showString String
"dual " ShowS -> ShowS -> ShowS
forall b c a. (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
. Int -> Free a b -> ShowS
forall a. Show a => Int -> a -> ShowS
P.showsPrec Int
11 a ~> b
Free a b
f
  showsPrec Int
d (DualInv DualF b ~> DualF a
f) = Bool -> ShowS -> ShowS
P.showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
P.> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
P.$ String -> ShowS
P.showString String
"dualInv " ShowS -> ShowS -> ShowS
forall b c a. (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
. Int -> Free (DualF b) (DualF a) -> ShowS
forall a. Show a => Int -> a -> ShowS
P.showsPrec Int
11 DualF b ~> DualF a
Free (DualF b) (DualF a)
f
  showsPrec Int
d (LinDist (a **! b) ~> DualF c
f) = Bool -> ShowS -> ShowS
P.showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
P.> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
P.$ String -> ShowS
P.showString String
"linDist " ShowS -> ShowS -> ShowS
forall b c a. (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
. Int -> Free (a **! b) (DualF c) -> ShowS
forall a. Show a => Int -> a -> ShowS
P.showsPrec Int
11 (a **! b) ~> DualF c
Free (a **! b) (DualF c)
f
  showsPrec Int
d (LinDistInv a ~> DualF (b **! c)
f) = Bool -> ShowS -> ShowS
P.showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
P.> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
P.$ String -> ShowS
P.showString String
"linDistInv " ShowS -> ShowS -> ShowS
forall b c a. (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
. Int -> Free a (DualF (b **! c)) -> ShowS
forall a. Show a => Int -> a -> ShowS
P.showsPrec Int
11 a ~> DualF (b **! c)
Free a (DualF (b **! c))
f

instance
  (StarAutonomousStructures `Elems` cs)
  => StarAutonomous (FREE cs (p :: CAT k))
  where
  type Dual a = DualF a
  withObDual :: forall (a :: FREE cs p) r. Ob a => (Ob (Dual a) => r) -> r
withObDual Ob (Dual a) => r
r = r
Ob (Dual a) => r
r
  dual :: forall (a :: FREE cs p) (b :: FREE cs p).
(a ~> b) -> Dual b ~> Dual a
dual a ~> b
f = Struct StarAutonomous (DualF b) (DualF a)
-> Free (DualF b) (DualF b) -> Free (DualF b) (DualF a)
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 ((a ~> b) -> Struct StarAutonomous (DualF b) (DualF a)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p) (b :: FREE cs p).
(a ~> b) -> Struct StarAutonomous (DualF b) (DualF a)
Dual a ~> b
f) Free (DualF b) (DualF b)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil ((Ob a, Ob b) => Free (DualF b) (DualF a))
-> Free a b -> Free (DualF b) (DualF a)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FREE cs p) (b :: FREE cs p) r.
((Ob a, Ob b) => r) -> Free a b -> r
\\ a ~> b
Free a b
f
  dualInv :: forall (a :: FREE cs p) (b :: FREE cs p).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv @a @b Dual a ~> Dual b
f = Struct StarAutonomous b a -> Free b b -> Free b a
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) =>
(DualF a ~> DualF b) -> Struct StarAutonomous b a
forall (a :: FREE cs p) (b :: FREE cs p).
(Ob a, Ob b) =>
(DualF a ~> DualF b) -> Struct StarAutonomous b a
DualInv @a @b DualF a ~> DualF b
Dual a ~> Dual b
f) Free b b
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil ((Ob (DualF a), Ob (DualF b)) => Free b a)
-> Free (DualF a) (DualF b) -> Free b a
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FREE cs p) (b :: FREE cs p) r.
((Ob a, Ob b) => r) -> Free a b -> r
\\ Dual a ~> Dual b
Free (DualF a) (DualF b)
f
  linDist :: forall (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @a @b @c (a ** b) ~> Dual c
f = Struct StarAutonomous a (DualF (b **! c))
-> Free a a -> Free a (DualF (b **! c))
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) (a :: FREE cs p) (b :: FREE cs p).
(Ob a, Ob a, Ob b) =>
((a **! a) ~> DualF b) -> Struct StarAutonomous a (DualF (a **! b))
forall (a :: FREE cs p) (a :: FREE cs p) (b :: FREE cs p).
(Ob a, Ob a, Ob b) =>
((a **! a) ~> DualF b) -> Struct StarAutonomous a (DualF (a **! b))
LinDist @a @b @c (a **! b) ~> DualF c
(a ** b) ~> Dual c
f) Free a a
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil ((Ob (a **! b), Ob (DualF c)) => Free a (DualF (b **! c)))
-> Free (a **! b) (DualF c) -> Free a (DualF (b **! c))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FREE cs p) (b :: FREE cs p) r.
((Ob a, Ob b) => r) -> Free a b -> r
\\ (a ** b) ~> Dual c
Free (a **! b) (DualF c)
f
  linDistInv :: forall (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @a @b @c a ~> Dual (b ** c)
f = Struct StarAutonomous (a **! b) (DualF c)
-> Free (a **! b) (a **! b) -> Free (a **! b) (DualF c)
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) (c :: FREE cs p).
(Ob a, Ob b, Ob c) =>
(a ~> DualF (b **! c)) -> Struct StarAutonomous (a **! b) (DualF c)
forall (a :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p).
(Ob a, Ob b, Ob c) =>
(a ~> DualF (b **! c)) -> Struct StarAutonomous (a **! b) (DualF c)
LinDistInv @a @b @c a ~> DualF (b **! c)
a ~> Dual (b ** c)
f) Free (a **! b) (a **! b)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil ((Ob a, Ob (DualF (b **! c))) => Free (a **! b) (DualF c))
-> Free a (DualF (b **! c)) -> Free (a **! b) (DualF c)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FREE cs p) (b :: FREE cs p) r.
((Ob a, Ob b) => r) -> Free a b -> r
\\ a ~> Dual (b ** c)
Free a (DualF (b **! c))
f

-- | 'dual' is a contravariant functor, bijective on hom-sets with inverse 'dualInv'; 'doubleNeg'
-- is an isomorphism; and 'linDist' is a natural bijection
-- @Hom(a ** b, Dual c) ≅ Hom(a, Dual (b ** c))@ with inverse 'linDistInv'.
instance Laws StarAutonomousStructures where
  laws :: [Law StarAutonomousStructures]
laws =
    [ String
-> LawBody StarAutonomousStructures -> Law StarAutonomousStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"dual identity" \ @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 ((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) (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)
    , String
-> LawBody StarAutonomousStructures -> Law StarAutonomousStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"dual composition" \ @a @b @c forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> do
        f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @a @b String
"f"
        g <- mor @b @c "g"
        dual (g . f) === dual f . dual g
    , String
-> LawBody StarAutonomousStructures -> Law StarAutonomousStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"linDist naturality" \ @a @b @c @d @e forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor ->
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @b ((Ob (a ** b) => m (Equation k)) -> m (Equation k))
-> (Ob (a ** b) => m (Equation k)) -> m (Equation k)
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 @_ @d @e ((Ob (d ** e) => m (Equation k)) -> m (Equation k))
-> (Ob (d ** e) => m (Equation k)) -> m (Equation k)
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @_ @c ((Ob (Dual c) => m (Equation k)) -> m (Equation k))
-> (Ob (Dual c) => m (Equation k)) -> m (Equation k)
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @_ @d do
          p <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @(a ** b) @(Dual c) String
"p"
          f <- mor @d @a "f"
          g <- mor @e @b "g"
          h <- mor @d @c "h"
          linDist @_ @d @e @d (dual h . p . (f ** g)) === dual (g ** h) . linDist @_ @a @b @c p . f
    ]
      [Law StarAutonomousStructures]
-> [Law StarAutonomousStructures] -> [Law StarAutonomousStructures]
forall a. [a] -> [a] -> [a]
P.++ String
-> BijectionBody StarAutonomousStructures
-> [Law StarAutonomousStructures]
forall (cs :: [Type -> Constraint]).
String -> BijectionBody cs -> [Law cs]
bijection
        String
"dual"
        ( \ @a @b forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor ->
            forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @_ @a ((Ob (Dual a) => Bijection m k) -> Bijection m k)
-> (Ob (Dual a) => Bijection m k) -> Bijection m k
forall a b. (a -> b) -> a -> b
$
              forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @_ @b ((Ob (Dual b) => Bijection m k) -> Bijection m k)
-> (Ob (Dual b) => Bijection m k) -> Bijection m k
forall a b. (a -> b) -> a -> b
$
                m (a ~> b)
-> m (Dual b ~> Dual a)
-> ((a ~> b) -> Dual b ~> Dual a)
-> ((Dual b ~> Dual a) -> a ~> b)
-> Bijection m k
forall {k} (m :: Type -> Type) (a :: k) (b :: k) (c :: k) (d :: k).
m (a ~> b)
-> m (c ~> d)
-> ((a ~> b) -> c ~> d)
-> ((c ~> d) -> a ~> b)
-> Bijection m k
Bijection (forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @a @b String
"f") (forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @(Dual b) @(Dual a) String
"g") (a ~> b) -> Dual b ~> 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).
(StarAutonomous k, Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv @_ @b @a)
        )
      [Law StarAutonomousStructures]
-> [Law StarAutonomousStructures] -> [Law StarAutonomousStructures]
forall a. [a] -> [a] -> [a]
P.++ String
-> BijectionBody StarAutonomousStructures
-> [Law StarAutonomousStructures]
forall (cs :: [Type -> Constraint]).
String -> BijectionBody cs -> [Law cs]
bijection
        String
"linDist"
        ( \ @a @b @c forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor ->
            forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @b ((Ob (a ** b) => Bijection m k) -> Bijection m k)
-> (Ob (a ** b) => Bijection m k) -> Bijection m k
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 @_ @b @c ((Ob (b ** c) => Bijection m k) -> Bijection m k)
-> (Ob (b ** c) => Bijection m k) -> Bijection m k
forall a b. (a -> b) -> a -> b
$
                forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @_ @c ((Ob (Dual c) => Bijection m k) -> Bijection m k)
-> (Ob (Dual c) => Bijection m k) -> Bijection m k
forall a b. (a -> b) -> a -> b
$
                  forall k (a :: k) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @_ @(b ** c) ((Ob (Dual (b ** c)) => Bijection m k) -> Bijection m k)
-> (Ob (Dual (b ** c)) => Bijection m k) -> Bijection m k
forall a b. (a -> b) -> a -> b
$
                    m ((a ** b) ~> Dual c)
-> m (a ~> Dual (b ** c))
-> (((a ** b) ~> Dual c) -> a ~> Dual (b ** c))
-> ((a ~> Dual (b ** c)) -> (a ** b) ~> Dual c)
-> Bijection m k
forall {k} (m :: Type -> Type) (a :: k) (b :: k) (c :: k) (d :: k).
m (a ~> b)
-> m (c ~> d)
-> ((a ~> b) -> c ~> d)
-> ((c ~> d) -> a ~> b)
-> Bijection m k
Bijection (forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @(a ** b) @(Dual c) String
"p") (forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @a @(Dual (b ** c)) String
"q") (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 @_ @a @b @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 @_ @a @b @c)
        )
      [Law StarAutonomousStructures]
-> [Law StarAutonomousStructures] -> [Law StarAutonomousStructures]
forall a. [a] -> [a] -> [a]
P.++ [ String
-> LawBody StarAutonomousStructures -> Law StarAutonomousStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"doubleNegInv 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 ((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) r.
(StarAutonomous k, Ob a) =>
(Ob (Dual a) => r) -> r
withObDual @_ @(Dual a) (forall k (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
doubleNegInv @_ @a (a ~> Dual (Dual a)) -> (a ~> Dual (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). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
forall {k} (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
doubleNegInvDefault @a)
           ]
      [Law StarAutonomousStructures]
-> [Law StarAutonomousStructures] -> [Law StarAutonomousStructures]
forall a. [a] -> [a] -> [a]
P.++ String
-> PureLawBody StarAutonomousStructures Inverses
-> [Law StarAutonomousStructures]
forall (cs :: [Type -> Constraint]).
String -> PureLawBody cs Inverses -> [Law cs]
inverses String
"doubleNeg" \ @a -> (a ~> Dual (Dual a)) -> (Dual (Dual a) ~> a) -> Inverses k
forall {k} (a :: k) (b :: k). (a ~> b) -> (b ~> a) -> Inverses k
Inverses (forall k (a :: k). (StarAutonomous k, Ob a) => a ~> Dual (Dual a)
doubleNegInv @_ @a) (forall k (a :: k). (StarAutonomous k, Ob a) => Dual (Dual a) ~> a
doubleNeg @_ @a)