{-# LANGUAGE AllowAmbiguousTypes #-}

-- | A closed symmetric monoidal category with a chosen answer object @r@ is a dialogue category,
-- with @'Dual' a = a '~~>' r@. 'CPS' wraps the category to say which object. The morphisms are
-- those of the category itself, so with @r@ an object of effects, as @IO ()@ in 'Data.Kind.Type',
-- a morphism is pure and a term of @'Proarrow.Tools.SMC.Up' a@ is a computation
-- @(a -> IO ()) -> IO ()@: call by push value, with the effects in the computations only.
--
-- @CPS r@ is isomix exactly when @r@ is the unit ('answerUnit'), and *-autonomous only in
-- degenerate cases, since @(a ~~> r) ~~> r@ is rarely @a@.
module Proarrow.Category.Instance.Cps (CPS (..), Cps (..), answerUnit) where

import Prelude (type (~))

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Closed (Closed (..), swapClosed, toEl, uncurry)
import Proarrow.Category.Monoidal.Dialogue (Dialogue (..))
import Proarrow.Category.Monoidal.IsoMix (IsoMix (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), UN, WrappedOb, dimapDefault, obj)
import Proarrow.Monoid (CocommutativeComonoid, Comonoid (..))
import Proarrow.Optic (PIso', iso)

type data CPS (r :: k) = C k

-- | The arrows of the category, wrapped as a category on the 'CPS'-wrapped kind.
type Cps :: CAT (CPS r)
data Cps (a :: CPS r) b where
  Cps :: {forall {k} (a :: k) (b :: k) (r :: k). Cps (C a) (C b) -> a ~> b
unCps :: a ~> b} -> Cps (C a :: CPS r) (C b)

instance (CategoryOf k) => Profunctor (Cps :: CAT (CPS (r :: k))) where
  dimap :: forall (c :: CPS r) (a :: CPS r) (b :: CPS r) (d :: CPS r).
(c ~> a) -> (b ~> d) -> Cps a b -> Cps c d
dimap = (c ~> a) -> (b ~> d) -> Cps a b -> Cps c d
Cps c a -> Cps b d -> Cps a b -> Cps c d
forall {k} (p :: CAT k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: CPS r) (b :: CPS r) r.
((Ob a, Ob b) => r) -> Cps a b -> r
\\ Cps a ~> b
f = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
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
f

instance (CategoryOf k) => Promonad (Cps :: CAT (CPS (r :: k))) where
  id :: forall (a :: CPS r). Ob a => Cps a a
id = (UN C a ~> UN C a) -> Cps (C (UN C a)) (C (UN C a))
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps UN C a ~> UN C a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
  Cps a ~> b
f . :: forall (b :: CPS r) (c :: CPS r) (a :: CPS r).
Cps b c -> Cps a b -> Cps a c
. Cps a ~> b
g = (a ~> b) -> Cps (C a) (C b)
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps (a ~> b
f (a ~> b) -> (a ~> a) -> 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
. a ~> a
a ~> b
g)

instance (CategoryOf k) => CategoryOf (CPS (r :: k)) where
  type (~>) = Cps
  type Ob a = WrappedOb C a

instance (Monoidal k) => MonoidalProfunctor (Cps :: CAT (CPS (r :: k))) where
  one :: Cps Unit Unit
one = (Unit ~> Unit) -> Cps (C Unit) (C Unit)
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps Unit ~> Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one
  Cps a ~> b
f ** :: forall (x1 :: CPS r) (x2 :: CPS r) (y1 :: CPS r) (y2 :: CPS r).
Cps x1 x2 -> Cps y1 y2 -> Cps (x1 ** y1) (x2 ** y2)
** Cps a ~> b
g = ((a ** a) ~> (b ** b)) -> Cps (C (a ** a)) (C (b ** b))
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps (a ~> b
f (a ~> b) -> (a ~> b) -> (a ** a) ~> (b ** 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)
** a ~> b
g)

instance (Monoidal k) => Monoidal (CPS (r :: k)) where
  type Unit = C Unit
  type a ** b = C (UN C a ** UN C b)
  withOb2 :: forall (a :: CPS r) (b :: CPS r) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @(C a) @(C b) Ob (a ** b) => r
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @b r
Ob (UN C a ** UN C b) => r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: CPS r). Ob a => (Unit ** a) ~> a
leftUnitor @(C a) = ((Unit ** UN C a) ~> UN C a)
-> Cps (C (Unit ** UN C a)) (C (UN C a))
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps (forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @k @a)
  leftUnitorInv :: forall (a :: CPS r). Ob a => a ~> (Unit ** a)
leftUnitorInv @(C a) = (UN C a ~> (Unit ** UN C a))
-> Cps (C (UN C a)) (C (Unit ** UN C a))
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps (forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @k @a)
  rightUnitor :: forall (a :: CPS r). Ob a => (a ** Unit) ~> a
rightUnitor @(C a) = ((UN C a ** Unit) ~> UN C a)
-> Cps (C (UN C a ** Unit)) (C (UN C a))
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps (forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor @k @a)
  rightUnitorInv :: forall (a :: CPS r). Ob a => a ~> (a ** Unit)
rightUnitorInv @(C a) = (UN C a ~> (UN C a ** Unit))
-> Cps (C (UN C a)) (C (UN C a ** Unit))
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps (forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv @k @a)
  associator :: forall (a :: CPS r) (b :: CPS r) (c :: CPS r).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(C a) @(C b) @(C c) = (((UN C a ** UN C b) ** UN C c) ~> (UN C a ** (UN C b ** UN C c)))
-> Cps
     (C ((UN C a ** UN C b) ** UN C c))
     (C (UN C a ** (UN C b ** UN C c)))
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @a @b @c)
  associatorInv :: forall (a :: CPS r) (b :: CPS r) (c :: CPS r).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(C a) @(C b) @(C c) = ((UN C a ** (UN C b ** UN C c)) ~> ((UN C a ** UN C b) ** UN C c))
-> Cps
     (C (UN C a ** (UN C b ** UN C c)))
     (C ((UN C a ** UN C b) ** UN C c))
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @a @b @c)

instance (SymMonoidal k) => SymMonoidal (CPS (r :: k)) where
  swap :: forall (a :: CPS r) (b :: CPS r).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @(C a) @(C b) = ((UN C a ** UN C b) ~> (UN C b ** UN C a))
-> Cps (C (UN C a ** UN C b)) (C (UN C b ** UN C a))
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @a @b)

instance (Closed k) => Closed (CPS (r :: k)) where
  type a ~~> b = C (UN C a ~~> UN C b)
  withObExp :: forall (a :: CPS r) (b :: CPS r) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @(C a) @(C b) Ob (a ~~> b) => r
r = forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @a @b r
Ob (UN C a ~~> UN C b) => r
Ob (a ~~> b) => r
r
  curry :: forall (a :: CPS r) (b :: CPS r) (c :: CPS r).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @(C a) @(C b) (Cps a ~> b
f) = (UN C a ~> (UN C b ~~> b)) -> Cps (C (UN C a)) (C (UN C b ~~> b))
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps (forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @a @b a ~> b
(UN C a ** UN C b) ~> b
f)
  apply :: forall (a :: CPS r) (b :: CPS r).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @(C a) @(C b) = (((UN C a ~~> UN C b) ** UN C a) ~> UN C b)
-> Cps (C ((UN C a ~~> UN C b) ** UN C a)) (C (UN C b))
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps (forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @a @b)
  Cps a ~> b
f ^^^ :: forall (a :: CPS r) (b :: CPS r) (x :: CPS r) (y :: CPS r).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ Cps a ~> b
g = ((b ~~> a) ~> (a ~~> b)) -> Cps (C (b ~~> a)) (C (a ~~> b))
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps (a ~> b
f (a ~> b) -> (a ~> b) -> (b ~~> a) ~> (a ~~> b)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ a ~> b
g)

-- | The dual of @a@ is @a '~~>' r@, the functor 'Proarrow.Category.Monoidal.Closed.Not' @r@ on
-- objects: linear distribution is uncurrying, reassociating and currying.
instance (Closed k, SymMonoidal k, Ob r) => Dialogue (CPS (r :: k)) where
  type Dual (a :: CPS r) = C (UN C a ~~> r)
  withObDual :: forall (a :: CPS r) r. Ob a => (Ob (Dual a) => r) -> r
withObDual @(C a) Ob (Dual a) => r
r' = forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @a @r r
Ob (UN C a ~~> r) => r
Ob (Dual a) => r
r'
  dual :: forall (a :: CPS r) (b :: CPS r). (a ~> b) -> Dual b ~> Dual a
dual (Cps a ~> b
f) = ((b ~~> r) ~> (a ~~> r)) -> Cps (C (b ~~> r)) (C (a ~~> r))
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @r Obj r -> (a ~> b) -> (b ~~> r) ~> (a ~~> r)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ a ~> b
f)
  linDist :: forall (a :: CPS r) (b :: CPS r) (c :: CPS r).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist @(C a) @(C b) @(C c) (Cps a ~> b
f) =
    forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @b @c ((UN C a ~> ((UN C b ** UN C c) ~~> r))
-> Cps (C (UN C a)) (C ((UN C b ** UN C c) ~~> r))
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps (forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @a @(b ** c) (forall (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
forall {k} (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry @c @r a ~> b
a ~> (UN C c ~~> r)
f ((a ** UN C c) ~> r)
-> ((UN C a ** (UN C b ** UN C c)) ~> (a ** UN C c))
-> (UN C a ** (UN C b ** UN C c)) ~> r
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)
associatorInv @k @a @b @c)))
  linDistInv :: forall (a :: CPS r) (b :: CPS r) (c :: CPS r).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv @(C a) @(C b) @(C c) (Cps a ~> b
f) =
    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) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @b @c (((UN C a ** UN C b) ~> (UN C c ~~> r))
-> Cps (C (UN C a ** UN C b)) (C (UN C c ~~> r))
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps (forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @(a ** b) @c (forall (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
forall {k} (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry @(b ** c) @r a ~> b
UN C a ~> ((UN C b ** UN C c) ~~> r)
f ((UN C a ** (UN C b ** UN C c)) ~> r)
-> (((UN C a ** UN C b) ** UN C c)
    ~> (UN C a ** (UN C b ** UN C c)))
-> ((UN C a ** UN C b) ** UN C c) ~> r
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 @a @b @c))))
  doubleNegInv :: forall (a :: CPS r). Ob a => a ~> Dual (Dual a)
doubleNegInv @(C a) = forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @a @r ((UN C a ~> ((UN C a ~~> r) ~~> r))
-> Cps (C (UN C a)) (C ((UN C a ~~> r) ~~> r))
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps (forall (c :: k) (a :: k) (b :: k).
(Closed k, SymMonoidal k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> b ~> (a ~~> c)
forall {k} (c :: k) (a :: k) (b :: k).
(Closed k, SymMonoidal k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> b ~> (a ~~> c)
swapClosed @r (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(a ~~> r))))

-- | With the unit as the answer object, @'Dual' 'Unit' = Unit ~~> Unit ≅ Unit@, and a consumer meets
-- its value in 'apply'. With any other answer object the units differ, so this is the only isomix
-- instance; the constraint on @r@ says so, since 'Unit' is a type family and cannot head an
-- instance.
instance (Closed k, SymMonoidal k, r ~ Unit) => IsoMix (CPS (r :: k)) where
  dualUnit :: Dual Unit ~> Unit
dualUnit = forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @Unit @Unit (((r ~~> r) ~> r) -> Cps (C (r ~~> r)) (C r)
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps (forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @Unit @Unit (((r ~~> r) ** r) ~> r)
-> ((r ~~> r) ~> ((r ~~> r) ** r)) -> (r ~~> r) ~> r
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 ~> (a ** Unit)
rightUnitorInv @k @(Unit ~~> Unit)))
  dualUnitInv :: Unit ~> Dual Unit
dualUnitInv = (r ~> (r ~~> r)) -> Cps (C r) (C (r ~~> r))
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps (forall (a :: k). (Closed k, Ob a) => a ~> (Unit ~~> a)
forall {k} (a :: k). (Closed k, Ob a) => a ~> (Unit ~~> a)
toEl @Unit)
  dualityCounit :: forall (a :: CPS r). Ob a => (Dual a ** a) ~> Unit
dualityCounit @(C a) = (((UN C a ~~> r) ** UN C a) ~> r)
-> Cps (C ((UN C a ~~> r) ** UN C a)) (C r)
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps (forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @a @Unit)

-- | The converse: an isomix structure on @CPS r@ makes @r@ the unit, through @Unit ~~> r ≅ r@.
answerUnit :: forall {k} (r :: k). (Closed k, Ob r, IsoMix (CPS r)) => PIso' r Unit
answerUnit :: forall {k} (r :: k).
(Closed k, Ob r, IsoMix (CPS r)) =>
PIso' r Unit
answerUnit =
  forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k @Unit @r
    ( (r ~> Unit) -> (Unit ~> r) -> PIso' r Unit
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
        (Cps (C (Unit ~~> r)) (C Unit) -> (Unit ~~> r) ~> Unit
forall {k} (a :: k) (b :: k) (r :: k). Cps (C a) (C b) -> a ~> b
unCps (forall k. IsoMix k => Dual Unit ~> Unit
dualUnit @(CPS r)) ((Unit ~~> r) ~> Unit) -> (r ~> (Unit ~~> r)) -> r ~> Unit
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). (Closed k, Ob a) => a ~> (Unit ~~> a)
forall {k} (a :: k). (Closed k, Ob a) => a ~> (Unit ~~> a)
toEl @r)
        (forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @Unit @r (((Unit ~~> r) ** Unit) ~> r)
-> (Unit ~> ((Unit ~~> r) ** Unit)) -> Unit ~> r
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 ~> (a ** Unit)
rightUnitorInv @k @(Unit ~~> r) ((Unit ~~> r) ~> ((Unit ~~> r) ** Unit))
-> (Unit ~> (Unit ~~> r)) -> Unit ~> ((Unit ~~> r) ** Unit)
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
. Cps (C Unit) (C (Unit ~~> r)) -> Unit ~> (Unit ~~> r)
forall {k} (a :: k) (b :: k) (r :: k). Cps (C a) (C b) -> a ~> b
unCps (forall k. IsoMix k => Unit ~> Dual Unit
dualUnitInv @(CPS r)))
    )

instance (Comonoid a) => Comonoid (C a :: CPS r) where
  counit :: C a ~> Unit
counit = (a ~> Unit) -> Cps (C a) (C Unit)
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps a ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit
  comult :: C a ~> (C a ** C a)
comult = (a ~> (a ** a)) -> Cps (C a) (C (a ** a))
forall {k} (a :: k) (b :: k) (r :: k). (a ~> b) -> Cps (C a) (C b)
Cps a ~> (a ** a)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult

instance (CocommutativeComonoid a) => CocommutativeComonoid (C a :: CPS r)