{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Dialogue categories (Melliès): symmetric monoidal categories with a tensorial negation 'Dual',
-- where morphisms @a ** b ~> Dual c@ correspond to @a ~> Dual (b ** c)@ ('linDist'). Unlike in a
-- *-autonomous category, double negation @'Dual' ('Dual' a) ~> a@ need not exist: only its inverse
-- 'doubleNegInv' does, which 'tripleNeg' undoes on a dual. Any closed category with a chosen
-- answer object is one, with @'Dual' a = a ~~> r@, which is why the continuation passing
-- reading of System L in "Proarrow.Tools.SMC" needs no more than this.
--
-- The *-autonomous categories of "Proarrow.Category.Monoidal.StarAutonomous" are the dialogue
-- categories whose double negation is an isomorphism.
module Proarrow.Category.Monoidal.Dialogue 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.Strictified (Strictified (..), obj1, singleton)
import Proarrow.Core (CAT, CategoryOf (..), Kind, Obj, Profunctor (..), Promonad (..), obj)
import Proarrow.Limit.BinaryProduct ()
import Proarrow.Tools.Laws (Bijection (..), Law (..), Laws (..), bijection, (===))

-- | A dialogue category: a symmetric monoidal category with a tensorial negation, so that 'Dual'
-- is a contravariant functor and @Hom(a '**' b, 'Dual' c) ≅ Hom(a, 'Dual' (b '**' c))@.
--
-- __Laws:__
--
-- * 'dual' is a contravariant functor: @'dual' 'id' = 'id'@ and @'dual' (f . g) = 'dual' g . 'dual' f@
-- * 'linDist' and 'linDistInv' are mutually inverse, giving
--   @Hom(a '**' b, 'Dual' c) ≅ Hom(a, 'Dual' (b '**' c))@, natural in all three variables
-- * 'doubleNegInv' is 'doubleNegInvDefault', the one the rest of the structure gives
--
-- Stated as code by the 'Proarrow.Tools.Laws.Laws' instance for 'DialogueStructures', and
-- checked by @Proarrow.Testing.Laws.testDialogue@.
class (SymMonoidal k) => Dialogue 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

  -- | 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 introduction. Defaults to 'doubleNegInvDefault'.
  doubleNegInv :: (Ob (a :: k)) => a ~> Dual (Dual a)
  doubleNegInv @a = forall (a :: k). (Dialogue k, Ob a) => a ~> Dual (Dual a)
forall {k} (a :: k). (Dialogue k, Ob a) => a ~> Dual (Dual a)
doubleNegInvDefault @a

dualObj :: forall {k} (a :: k). (Dialogue k, Ob a) => Obj (Dual a)
dualObj :: forall {k} (a :: k). (Dialogue 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).
Dialogue 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)

-- | 'doubleNegInv' from the rest of the structure, through 'linDistInv' and the duality unit.
doubleNegInvDefault :: forall {k} (a :: k). (Dialogue k, Ob a) => a ~> Dual (Dual a)
doubleNegInvDefault :: forall {k} (a :: k). (Dialogue k, Ob a) => a ~> Dual (Dual a)
doubleNegInvDefault =
  forall k (a :: k) (b :: k) (c :: k).
(Dialogue 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).
Dialogue 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). (Dialogue k, Ob a) => Unit ~> Dual (Dual a ** a)
forall {k} (a :: k).
(Dialogue 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). (Dialogue k, Ob a) => Obj (Dual a)
forall {k} (a :: k). (Dialogue k, Ob a) => Obj (Dual a)
dualObj @a

-- | Triple negation elimination: a dual is a retract of its double negation, with 'doubleNegInv' as
-- the section, @'tripleNeg' . 'doubleNegInv' = 'id'@. For the computations of "Proarrow.Tools.SMC"
-- it runs a computation of a computation into one, like @join@. It is an isomorphism only in a
-- *-autonomous category: in 'Data.Kind.Type' with answer object 'Prelude.Bool', @Dual ()@ has two
-- elements and @Dual (Dual (Dual ()))@ sixteen.
tripleNeg :: forall {k} (a :: k). (Dialogue k, Ob a) => Dual (Dual (Dual a)) ~> Dual a
tripleNeg :: forall {k} (a :: k).
(Dialogue k, Ob a) =>
Dual (Dual (Dual a)) ~> Dual a
tripleNeg = (a ~> Dual (Dual a)) -> Dual (Dual (Dual a)) ~> Dual a
forall (a :: k) (b :: k). (a ~> b) -> Dual b ~> Dual a
forall k (a :: k) (b :: k).
Dialogue k =>
(a ~> b) -> Dual b ~> Dual a
dual (forall k (a :: k). (Dialogue k, Ob a) => a ~> Dual (Dual a)
doubleNegInv @k @a)

-- | The Kleisli extension of the double negation monad at a dual: a morphism out of @a@ into a dual,
-- extended to double negations of @a@. This is the bind of the continuation reading of System L in
-- "Proarrow.Tools.SMC". It moves @a@ to the other side of the hom, @g ** y ~> Dual a@, and dualizes.
{-# INLINE bindDual #-}
bindDual
  :: forall {k} (g :: k) a y
   . (Dialogue k, Ob g, Ob a, Ob y)
  => g ** a ~> Dual y
  -> Dual (Dual a) ** g ~> Dual y
bindDual :: forall {k} (g :: k) (a :: k) (y :: k).
(Dialogue k, Ob g, Ob a, Ob y) =>
((g ** a) ~> Dual y) -> (Dual (Dual a) ** g) ~> Dual y
bindDual (g ** a) ~> Dual y
f =
  forall k (a :: k) r. (Dialogue k, Ob a) => (Ob (Dual a) => r) -> r
withObDual @k @a ((Ob (Dual a) => (Dual (Dual a) ** g) ~> Dual y)
 -> (Dual (Dual a) ** g) ~> Dual y)
-> (Ob (Dual a) => (Dual (Dual a) ** g) ~> Dual y)
-> (Dual (Dual a) ** g) ~> Dual y
forall a b. (a -> b) -> a -> b
$
    forall k (a :: k) r. (Dialogue k, Ob a) => (Ob (Dual a) => r) -> r
withObDual @k @(Dual a) ((Ob (Dual (Dual a)) => (Dual (Dual a) ** g) ~> Dual y)
 -> (Dual (Dual a) ** g) ~> Dual y)
-> (Ob (Dual (Dual a)) => (Dual (Dual a) ** g) ~> Dual y)
-> (Dual (Dual a) ** g) ~> Dual y
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) (c :: k).
(Dialogue k, Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @k @(Dual (Dual a)) @g @y ((Dual (Dual a) ~> Dual (g ** y))
 -> (Dual (Dual a) ** g) ~> Dual y)
-> (Dual (Dual a) ~> Dual (g ** y))
-> (Dual (Dual a) ** g) ~> Dual y
forall a b. (a -> b) -> a -> b
$
        ((g ** y) ~> Dual a) -> Dual (Dual a) ~> Dual (g ** y)
forall (a :: k) (b :: k). (a ~> b) -> Dual b ~> Dual a
forall k (a :: k) (b :: k).
Dialogue k =>
(a ~> b) -> Dual b ~> Dual a
dual (((g ** y) ~> Dual a) -> Dual (Dual a) ~> Dual (g ** y))
-> ((g ** y) ~> Dual a) -> Dual (Dual a) ~> Dual (g ** y)
forall a b. (a -> b) -> a -> b
$
          forall k (a :: k) (b :: k) (c :: k).
(Dialogue k, Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @k @g @y @a (((y ** a) ~> (a ** y)) -> Dual (a ** y) ~> Dual (y ** a)
forall (a :: k) (b :: k). (a ~> b) -> Dual b ~> Dual a
forall k (a :: k) (b :: k).
Dialogue 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 @y @a) (Dual (a ** y) ~> Dual (y ** a))
-> (g ~> Dual (a ** y)) -> g ~> Dual (y ** a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Dialogue k, Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @k @g @a @y (g ** a) ~> Dual y
f)

linDistS
  :: forall {k} (a :: k) (b :: k) c. (Dialogue k, Ob c) => '[a, b] ~> '[Dual c] -> '[a] ~> '[Dual (b ** c)]
linDistS :: forall {k} (a :: k) (b :: k) (c :: k).
(Dialogue 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).
(Dialogue 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. (Dialogue k, Ob b, Ob c) => '[a] ~> '[Dual (b ** c)] -> '[a, b] ~> '[Dual c]
linDistInvS :: forall {k} (a :: k) (b :: k) (c :: k).
(Dialogue 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. (Dialogue 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).
(Dialogue 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))

-- | Par, the dual of the tensor of the duals.
type Par :: forall {k}. k -> k -> k
type Par a b = Dual (Dual a ** Dual b)

-- | Recovers @'Ob' ('Par' a b)@, and the objecthood of the duals it is made of, from the objecthood
-- of @a@ and @b@.
withObPar
  :: forall {k} (a :: k) b r. (Dialogue k, Ob a, Ob b) => ((Ob (Dual a), Ob (Dual b), Ob (Par a b)) => r) -> r
withObPar :: forall {k} (a :: k) (b :: k) r.
(Dialogue k, Ob a, Ob b) =>
((Ob (Dual a), Ob (Dual b), Ob (Par a b)) => r) -> r
withObPar (Ob (Dual a), Ob (Dual b), Ob (Par a b)) => r
r = forall k (a :: k) r. (Dialogue k, Ob a) => (Ob (Dual a) => r) -> r
withObDual @k @a (forall k (a :: k) r. (Dialogue k, Ob a) => (Ob (Dual a) => r) -> r
withObDual @k @b (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @(Dual a) @(Dual b) (forall k (a :: k) r. (Dialogue k, Ob a) => (Ob (Dual a) => r) -> r
withObDual @k @(Dual a ** Dual b) r
(Ob (Dual a), Ob (Dual b), Ob (Par a b)) => r
Ob (Par a b) => r
r)))

-- | 'Par'\'s action on arrows.
par :: forall {k} (a :: k) b c d. (Dialogue k) => a ~> c -> b ~> d -> Par a b ~> Par c d
par :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
Dialogue k =>
(a ~> c) -> (b ~> d) -> Par a b ~> Par c d
par a ~> c
f b ~> d
g = ((Dual c ** Dual d) ~> (Dual a ** Dual b))
-> Dual (Dual a ** Dual b) ~> Dual (Dual c ** Dual d)
forall (a :: k) (b :: k). (a ~> b) -> Dual b ~> Dual a
forall k (a :: k) (b :: k).
Dialogue k =>
(a ~> b) -> Dual b ~> Dual a
dual ((a ~> c) -> Dual c ~> Dual a
forall (a :: k) (b :: k). (a ~> b) -> Dual b ~> Dual a
forall k (a :: k) (b :: k).
Dialogue k =>
(a ~> b) -> Dual b ~> Dual a
dual a ~> c
f (Dual c ~> Dual a)
-> (Dual d ~> Dual b) -> (Dual c ** Dual d) ~> (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)
** (b ~> d) -> Dual d ~> Dual b
forall (a :: k) (b :: k). (a ~> b) -> Dual b ~> Dual a
forall k (a :: k) (b :: k).
Dialogue k =>
(a ~> b) -> Dual b ~> Dual a
dual b ~> d
g)

-- | The symmetry of 'Par'.
parSwap :: forall {k} (a :: k) b. (Dialogue k, Ob a, Ob b) => Par a b ~> Par b a
parSwap :: forall {k} (a :: k) (b :: k).
(Dialogue k, Ob a, Ob b) =>
Par a b ~> Par b a
parSwap = forall (a :: k) (b :: k) r.
(Dialogue k, Ob a, Ob b) =>
((Ob (Dual a), Ob (Dual b), Ob (Par a b)) => r) -> r
forall {k} (a :: k) (b :: k) r.
(Dialogue k, Ob a, Ob b) =>
((Ob (Dual a), Ob (Dual b), Ob (Par a b)) => r) -> r
withObPar @a @b (((Dual b ** Dual a) ~> (Dual a ** Dual b))
-> Dual (Dual a ** Dual b) ~> Dual (Dual b ** Dual a)
forall (a :: k) (b :: k). (a ~> b) -> Dual b ~> Dual a
forall k (a :: k) (b :: k).
Dialogue 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 @(Dual b) @(Dual a)))

-- | Linear distributivity: the tensor distributes into the left of a 'Par'. Given the dual of
-- @a '**' b@, the @a@ turns it into the dual of @b@, which the 'Par' answers with @c@.
weakDistL :: forall {k} (a :: k) b c. (Dialogue k, Ob a, Ob b, Ob c) => a ** Par b c ~> Par (a ** b) c
weakDistL :: forall {k} (a :: k) (b :: k) (c :: k).
(Dialogue k, Ob a, Ob b, Ob c) =>
(a ** Par b c) ~> Par (a ** b) c
weakDistL =
  forall (a :: k) (b :: k) r.
(Dialogue k, Ob a, Ob b) =>
((Ob (Dual a), Ob (Dual b), Ob (Par a b)) => r) -> r
forall {k} (a :: k) (b :: k) r.
(Dialogue k, Ob a, Ob b) =>
((Ob (Dual a), Ob (Dual b), Ob (Par a b)) => r) -> r
withObPar @b @c
    ( forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @b
        ( forall k (a :: k) r. (Dialogue k, Ob a) => (Ob (Dual a) => r) -> r
withObDual @k @(a ** b)
            ( forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @(Par b c)
                ( forall k (a :: k) (b :: k) (c :: k).
(Dialogue k, Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @k @(a ** Par b c) @(Dual (a ** b)) @(Dual c)
                    ( forall k (a :: k) (b :: k) (c :: k).
(Dialogue k, Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @k @(Par b c) @(Dual b) @(Dual c) Dual (Dual b ** Dual c) ~> Dual (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
                        ((Dual (Dual b ** Dual c) ** Dual b) ~> Dual (Dual c))
-> (((a ** Dual (Dual b ** Dual c)) ** Dual (a ** b))
    ~> (Dual (Dual b ** Dual c) ** Dual b))
-> ((a ** Dual (Dual b ** Dual c)) ** Dual (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
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Par b c) (Dual (Dual b ** Dual c) ~> Dual (Dual b ** Dual c))
-> ((Dual (a ** b) ** a) ~> Dual b)
-> (Dual (Dual b ** Dual c) ** (Dual (a ** b) ** a))
   ~> (Dual (Dual b ** Dual c) ** 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)
** forall k (a :: k) (b :: k) (c :: k).
(Dialogue k, Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @k @(Dual (a ** b)) @a @b Dual (a ** b) ~> Dual (a ** b)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id)
                        ((Dual (Dual b ** Dual c) ** (Dual (a ** b) ** a))
 ~> (Dual (Dual b ** Dual c) ** Dual b))
-> (((a ** Dual (Dual b ** Dual c)) ** Dual (a ** b))
    ~> (Dual (Dual b ** Dual c) ** (Dual (a ** b) ** a)))
-> ((a ** Dual (Dual b ** Dual c)) ** Dual (a ** b))
   ~> (Dual (Dual b ** Dual c) ** Dual b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Par b c) (Dual (Dual b ** Dual c) ~> Dual (Dual b ** Dual c))
-> ((a ** Dual (a ** b)) ~> (Dual (a ** b) ** a))
-> (Dual (Dual b ** Dual c) ** (a ** Dual (a ** b)))
   ~> (Dual (Dual b ** Dual c) ** (Dual (a ** b) ** a))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @a @(Dual (a ** b)))
                        ((Dual (Dual b ** Dual c) ** (a ** Dual (a ** b)))
 ~> (Dual (Dual b ** Dual c) ** (Dual (a ** b) ** a)))
-> (((a ** Dual (Dual b ** Dual c)) ** Dual (a ** b))
    ~> (Dual (Dual b ** Dual c) ** (a ** Dual (a ** b))))
-> ((a ** Dual (Dual b ** Dual c)) ** Dual (a ** b))
   ~> (Dual (Dual b ** Dual c) ** (Dual (a ** b) ** a))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @(Par b c) @a @(Dual (a ** b))
                        (((Dual (Dual b ** Dual c) ** a) ** Dual (a ** b))
 ~> (Dual (Dual b ** Dual c) ** (a ** Dual (a ** b))))
-> (((a ** Dual (Dual b ** Dual c)) ** Dual (a ** b))
    ~> ((Dual (Dual b ** Dual c) ** a) ** Dual (a ** b)))
-> ((a ** Dual (Dual b ** Dual c)) ** Dual (a ** b))
   ~> (Dual (Dual b ** Dual c) ** (a ** Dual (a ** b)))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @a @(Par b c) ((a ** Dual (Dual b ** Dual c)) ~> (Dual (Dual b ** Dual c) ** a))
-> (Dual (a ** b) ~> Dual (a ** b))
-> ((a ** Dual (Dual b ** Dual c)) ** Dual (a ** b))
   ~> ((Dual (Dual b ** Dual c) ** a) ** Dual (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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Dual (a ** b)))
                    )
                )
            )
        )
    )

-- | Linear distributivity on the other side, from 'weakDistL' by symmetry.
weakDistR :: forall {k} (a :: k) b c. (Dialogue k, Ob a, Ob b, Ob c) => Par a b ** c ~> Par a (b ** c)
weakDistR :: forall {k} (a :: k) (b :: k) (c :: k).
(Dialogue k, Ob a, Ob b, Ob c) =>
(Par a b ** c) ~> Par a (b ** c)
weakDistR =
  forall (a :: k) (b :: k) r.
(Dialogue k, Ob a, Ob b) =>
((Ob (Dual a), Ob (Dual b), Ob (Par a b)) => r) -> r
forall {k} (a :: k) (b :: k) r.
(Dialogue k, Ob a, Ob b) =>
((Ob (Dual a), Ob (Dual b), Ob (Par a b)) => r) -> r
withObPar @b @a
    ( forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @c @b
        ( (a ~> a)
-> ((c ** b) ~> (b ** c))
-> Dual (Dual a ** Dual (c ** b)) ~> Dual (Dual a ** Dual (b ** c))
forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
Dialogue k =>
(a ~> c) -> (b ~> d) -> Par a b ~> Par c d
par (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @c @b)
            (Dual (Dual a ** Dual (c ** b)) ~> Dual (Dual a ** Dual (b ** c)))
-> ((Dual (Dual a ** Dual b) ** c)
    ~> Dual (Dual a ** Dual (c ** b)))
-> (Dual (Dual a ** Dual b) ** c) ~> Dual (Dual a ** Dual (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 (a :: k) (b :: k).
(Dialogue k, Ob a, Ob b) =>
Par a b ~> Par b a
forall {k} (a :: k) (b :: k).
(Dialogue k, Ob a, Ob b) =>
Par a b ~> Par b a
parSwap @(c ** b) @a
            (Par (c ** b) a ~> Dual (Dual a ** Dual (c ** b)))
-> ((Dual (Dual a ** Dual b) ** c) ~> Par (c ** b) a)
-> (Dual (Dual a ** Dual b) ** c) ~> Dual (Dual a ** Dual (c ** b))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k) (c :: k).
(Dialogue k, Ob a, Ob b, Ob c) =>
(a ** Par b c) ~> Par (a ** b) c
forall {k} (a :: k) (b :: k) (c :: k).
(Dialogue k, Ob a, Ob b, Ob c) =>
(a ** Par b c) ~> Par (a ** b) c
weakDistL @c @b @a
            ((c ** Par b a) ~> Par (c ** b) a)
-> ((Dual (Dual a ** Dual b) ** c) ~> (c ** Par b a))
-> (Dual (Dual a ** Dual b) ** c) ~> Par (c ** b) a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @(Par b a) @c
            ((Par b a ** c) ~> (c ** Par b a))
-> ((Dual (Dual a ** Dual b) ** c) ~> (Par b a ** c))
-> (Dual (Dual a ** Dual b) ** c) ~> (c ** Par b 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) (b :: k).
(Dialogue k, Ob a, Ob b) =>
Par a b ~> Par b a
forall {k} (a :: k) (b :: k).
(Dialogue k, Ob a, Ob b) =>
Par a b ~> Par b a
parSwap @a @b (Dual (Dual a ** Dual b) ~> Par b a)
-> (c ~> c) -> (Dual (Dual a ** Dual b) ** c) ~> (Par b a ** c)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c)
        )
    )

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

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

instance Dialogue () 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
  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
  doubleNegInv :: forall (a :: ()). Ob a => a ~> Dual (Dual a)
doubleNegInv = a ~> Dual (Dual a)
Unit '() '()
U.Unit

instance Dialogue 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
  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
  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

instance (Dialogue j, Dialogue k) => Dialogue (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. (Dialogue k, Ob a) => (Ob (Dual a) => r) -> r
withObDual @j @a (forall k (a :: k) r. (Dialogue 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).
Dialogue 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).
Dialogue k =>
(a ~> b) -> Dual b ~> Dual a
dual a2 ~> b2
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).
(Dialogue 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).
(Dialogue 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).
(Dialogue 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).
(Dialogue 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
  doubleNegInv :: forall (a :: (j, k)). Ob a => a ~> Dual (Dual a)
doubleNegInv @'(a, b) = forall k (a :: k). (Dialogue 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). (Dialogue k, Ob a) => a ~> Dual (Dual a)
doubleNegInv @k @b

data family DualF (a :: k) :: k
instance (IsFreeOb (a :: FREE cs p), Dialogue `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 @Dialogue @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. (Dialogue 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 'Dialogue', and those its laws are stated for.
type DialogueStructures :: [Kind -> Constraint]
type DialogueStructures = '[Monoidal, SymMonoidal, Dialogue]

instance
  (DialogueStructures `Elems` cs)
  => HasStructure cs (p :: CAT k) Dialogue
  where
  data Struct Dialogue a b where
    Dual :: a ~> b -> Struct Dialogue (DualF b) (DualF a)
    LinDist :: (Ob a, Ob b, Ob c) => a **! b ~> DualF c -> Struct Dialogue a (DualF (b **! c))
    LinDistInv :: (Ob a, Ob b, Ob c) => a ~> DualF (b **! c) -> Struct Dialogue (a **! b) (DualF c)
  foldStructure :: forall {k'} (f :: k +-> k') (a :: FREE cs p) (b :: FREE cs p).
(Dialogue k', All cs k', Representable f) =>
(forall (x :: FREE cs p) (y :: FREE cs p).
 (x ~> y) -> Lower f x ~> Lower f y)
-> Struct Dialogue 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).
Dialogue 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 (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).
(Dialogue 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).
(Dialogue 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 Dialogue a b) where
  showsPrec :: Int -> Struct Dialogue 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 (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
  (DialogueStructures `Elems` cs)
  => Dialogue (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 Dialogue (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 Dialogue (DualF b) (DualF a)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p) (b :: FREE cs p).
(a ~> b) -> Struct Dialogue (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
  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 Dialogue 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 Dialogue 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 Dialogue 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 Dialogue (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 Dialogue (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 Dialogue (a **! b) (DualF c)
LinDistInv @a @b @c a ~> Dual (b ** c)
a ~> DualF (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, 'linDist' is a natural bijection
-- @Hom(a ** b, Dual c) ≅ Hom(a, Dual (b ** c))@ with inverse 'linDistInv', and 'doubleNegInv' is
-- the one they give.
instance Laws DialogueStructures where
  laws :: [Law DialogueStructures]
laws =
    [ String -> LawBody DialogueStructures -> Law DialogueStructures
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. (Dialogue 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).
Dialogue 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 DialogueStructures -> Law DialogueStructures
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 DialogueStructures -> Law DialogueStructures
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. (Dialogue 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. (Dialogue 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 DialogueStructures]
-> [Law DialogueStructures] -> [Law DialogueStructures]
forall a. [a] -> [a] -> [a]
P.++ String
-> BijectionBody DialogueStructures -> [Law DialogueStructures]
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. (Dialogue 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. (Dialogue 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).
(Dialogue 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).
(Dialogue k, Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @_ @a @b @c)
        )
      [Law DialogueStructures]
-> [Law DialogueStructures] -> [Law DialogueStructures]
forall a. [a] -> [a] -> [a]
P.++ [ String -> LawBody DialogueStructures -> Law DialogueStructures
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. (Dialogue 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. (Dialogue k, Ob a) => (Ob (Dual a) => r) -> r
withObDual @_ @(Dual a) (forall k (a :: k). (Dialogue 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). (Dialogue k, Ob a) => a ~> Dual (Dual a)
forall {k} (a :: k). (Dialogue k, Ob a) => a ~> Dual (Dual a)
doubleNegInvDefault @a)
           ]