module Proarrow.Category.Equipment.Stateful where

import Proarrow.Category.Bicategory (Adjunction (..), Bicategory (..))
import Proarrow.Category.Bicategory.MonoidalAsBi (Mon2 (..), MonK (..))
import Proarrow.Category.Bicategory.Prof (PROFK (..), Prof (..))
import Proarrow.Category.Equipment (Equipment (..), HasCompanions (..), Sq (..))
import Proarrow.Category.Instance.Prof (unProf)
import Proarrow.Category.Monoidal (par)
import Proarrow.Category.Monoidal qualified as M
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), Strong (..))
import Proarrow.Category.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Is
  , Kind
  , Profunctor (..)
  , Promonad (..)
  , UN
  , dimapDefault
  , lmap
  , obj
  , rmap
  , src
  , tgt
  , (//)
  , (:~>)
  , type (+->)
  )
import Proarrow.Functor (map)
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Promonad.Reader (Reader)
import Proarrow.Promonad.Writer (Writer (..))

type STT :: Kind -> Kind -> CAT ()
newtype STT m k i j = ST (k +-> k)
type instance UN ST (ST p) = p

type StT :: CAT (STT m k i j)
data StT a b where
  StT :: (Strong m p, Strong m q) => p :~> q -> StT (ST p :: STT m k i j) (ST q)
instance (MonoidalAction m k) => Profunctor (StT :: CAT (STT m k i j)) where
  dimap :: forall (c :: STT m k i j) (a :: STT m k i j) (b :: STT m k i j)
       (d :: STT m k i j).
(c ~> a) -> (b ~> d) -> StT a b -> StT c d
dimap = (c ~> a) -> (b ~> d) -> StT a b -> StT c d
StT c a -> StT b d -> StT a b -> StT c d
forall {k} (p :: PRO k 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 :: STT m k i j) (b :: STT m k i j) r.
((Ob a, Ob b) => r) -> StT a b -> r
\\ StT p :~> q
p = r
(Ob (p Any Any), Ob (q Any Any)) => r
(Ob a, Ob b) => r
r ((Ob (p Any Any), Ob (q Any Any)) => r)
-> (p Any Any -> q Any Any) -> r
forall a b r. ((Ob a, Ob b) => r) -> (a -> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p Any Any -> q Any Any
p :~> q
p
instance (MonoidalAction m k) => Promonad (StT :: CAT (STT m k i j)) where
  id :: forall (a :: STT m k i j). Ob a => StT a a
id = (UN 'ST a :~> UN 'ST a) -> StT ('ST (UN 'ST a)) ('ST (UN 'ST a))
forall m k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong m p, Strong m q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT UN 'ST a a b -> UN 'ST a a b
UN 'ST a :~> UN 'ST a
forall a. Ob a => a -> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
  StT p :~> q
f . :: forall (b :: STT m k i j) (c :: STT m k i j) (a :: STT m k i j).
StT b c -> StT a b -> StT a c
. StT p :~> q
g = (p :~> q) -> StT ('ST p) ('ST q)
forall m k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong m p, Strong m q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT (p a b -> q a b
p :~> q
f (p a b -> q a b) -> (p a b -> p a b) -> p a b -> q a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a b -> p a b
p a b -> q a b
p :~> q
g)
instance (MonoidalAction m k) => CategoryOf (STT m k i j) where
  type (~>) = StT
  type Ob (a :: STT m k i j) = (Is ST a, Strong m (UN ST a))

instance (MonoidalAction m k) => Bicategory (STT m k) where
  type I = ST Id
  type ST a `O` ST b = ST (a :.: b)
  withOb2 :: forall {i :: ()} {j :: ()} {k :: ()} (a :: STT m k j k)
       (b :: STT m k i j) r.
(Ob a, Ob b, Ob0 (STT m k) i, Ob0 (STT m k) j, Ob0 (STT m k) k) =>
(Ob (O a b) => r) -> r
withOb2 Ob (O a b) => r
r = r
Ob (O a b) => r
r
  StT p :~> q
m o :: forall {i :: ()} (j :: ()) (k :: ()) (a :: STT m k j k)
       (b :: STT m k j k) (c :: STT m k i j) (d :: STT m k i j).
(a ~> b) -> (c ~> d) -> O a c ~> O b d
`o` StT p :~> q
n = ((p :.: p) :~> (q :.: q)) -> StT ('ST (p :.: p)) ('ST (q :.: q))
forall m k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong m p, Strong m q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT \(p a b
p :.: p b b
q) -> p a b -> q a b
p :~> q
m p a b
p q a b -> q b b -> (:.:) q q a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: p b b -> q b b
p :~> q
n p b b
q
  (Ob0 (STT m k) i, Ob0 (STT m k) j, Ob ps, Ob qs) => r
r \\\ :: forall (i :: ()) (j :: ()) (ps :: STT m k i j) (qs :: STT m k i j)
       r.
((Ob0 (STT m k) i, Ob0 (STT m k) j, Ob ps, Ob qs) => r)
-> (ps ~> qs) -> r
\\\ StT{} = r
(Ob0 (STT m k) i, Ob0 (STT m k) j, Ob ps, Ob qs) => r
r
  leftUnitor :: forall {i :: ()} {j :: ()} (a :: STT m k i j).
(Ob0 (STT m k) i, Ob0 (STT m k) j, Ob a) =>
O I a ~> a
leftUnitor = ((Id :.: UN 'ST a) :~> UN 'ST a)
-> StT ('ST (Id :.: UN 'ST a)) ('ST (UN 'ST a))
forall m k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong m p, Strong m q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT \(Id a ~> b
h :.: UN 'ST a b b
q) -> (a ~> b) -> UN 'ST a b b -> UN 'ST a a b
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> b
h UN 'ST a b b
q
  leftUnitorInv :: forall {i :: ()} {j :: ()} (a :: STT m k i j).
(Ob0 (STT m k) i, Ob0 (STT m k) j, Ob a) =>
a ~> O I a
leftUnitorInv = (UN 'ST a :~> (Id :.: UN 'ST a))
-> StT ('ST (UN 'ST a)) ('ST (Id :.: UN 'ST a))
forall m k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong m p, Strong m q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT \UN 'ST a a b
p -> (a ~> a) -> Id a a
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (UN 'ST a a b -> a ~> a
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src UN 'ST a a b
p) Id a a -> UN 'ST a a b -> (:.:) Id (UN 'ST a) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: UN 'ST a a b
p
  rightUnitor :: forall {i :: ()} {j :: ()} (a :: STT m k i j).
(Ob0 (STT m k) i, Ob0 (STT m k) j, Ob a) =>
O a I ~> a
rightUnitor = ((UN 'ST a :.: Id) :~> UN 'ST a)
-> StT ('ST (UN 'ST a :.: Id)) ('ST (UN 'ST a))
forall m k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong m p, Strong m q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT \(UN 'ST a a b
p :.: Id b ~> b
h) -> (b ~> b) -> UN 'ST a a b -> UN 'ST a a b
forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> b
h UN 'ST a a b
p
  rightUnitorInv :: forall {i :: ()} {j :: ()} (a :: STT m k i j).
(Ob0 (STT m k) i, Ob0 (STT m k) j, Ob a) =>
a ~> O a I
rightUnitorInv = (UN 'ST a :~> (UN 'ST a :.: Id))
-> StT ('ST (UN 'ST a)) ('ST (UN 'ST a :.: Id))
forall m k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong m p, Strong m q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT \UN 'ST a a b
p -> UN 'ST a a b
p UN 'ST a a b -> Id b b -> (:.:) (UN 'ST a) Id a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (b ~> b) -> Id b b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (UN 'ST a a b -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt UN 'ST a a b
p)
  associator :: forall {h :: ()} {i :: ()} {j :: ()} {k :: ()} (a :: STT m k j k)
       (b :: STT m k i j) (c :: STT m k h i).
(Ob0 (STT m k) h, Ob0 (STT m k) i, Ob0 (STT m k) j,
 Ob0 (STT m k) k, Ob a, Ob b, Ob c) =>
O (O a b) c ~> O a (O b c)
associator = (((UN 'ST a :.: UN 'ST b) :.: UN 'ST c)
 :~> (UN 'ST a :.: (UN 'ST b :.: UN 'ST c)))
-> StT
     ('ST ((UN 'ST a :.: UN 'ST b) :.: UN 'ST c))
     ('ST (UN 'ST a :.: (UN 'ST b :.: UN 'ST c)))
forall m k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong m p, Strong m q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT \((UN 'ST a a b
p :.: UN 'ST b b b
q) :.: UN 'ST c b b
r) -> UN 'ST a a b
p UN 'ST a a b
-> (:.:) (UN 'ST b) (UN 'ST c) b b
-> (:.:) (UN 'ST a) (UN 'ST b :.: UN 'ST c) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (UN 'ST b b b
q UN 'ST b b b -> UN 'ST c b b -> (:.:) (UN 'ST b) (UN 'ST c) b b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: UN 'ST c b b
r)
  associatorInv :: forall {h :: ()} {i :: ()} {j :: ()} {k :: ()} (a :: STT m k j k)
       (b :: STT m k i j) (c :: STT m k h i).
(Ob0 (STT m k) h, Ob0 (STT m k) i, Ob0 (STT m k) j,
 Ob0 (STT m k) k, Ob a, Ob b, Ob c) =>
O a (O b c) ~> O (O a b) c
associatorInv = ((UN 'ST a :.: (UN 'ST b :.: UN 'ST c))
 :~> ((UN 'ST a :.: UN 'ST b) :.: UN 'ST c))
-> StT
     ('ST (UN 'ST a :.: (UN 'ST b :.: UN 'ST c)))
     ('ST ((UN 'ST a :.: UN 'ST b) :.: UN 'ST c))
forall m k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong m p, Strong m q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT \(UN 'ST a a b
p :.: (UN 'ST b b b
q :.: UN 'ST c b b
r)) -> (UN 'ST a a b
p UN 'ST a a b -> UN 'ST b b b -> (:.:) (UN 'ST a) (UN 'ST b) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: UN 'ST b b b
q) (:.:) (UN 'ST a) (UN 'ST b) a b
-> UN 'ST c b b -> (:.:) (UN 'ST a :.: UN 'ST b) (UN 'ST c) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: UN 'ST c b b
r

-- | Stateful transformers.
-- https://arxiv.org/pdf/2305.16899 definition 6
-- Generalized to any monoidal action.
instance (MonoidalAction m k, M.SymMonoidal m, Ob (M.Unit @m)) => HasCompanions (STT m k) (MonK m) where
  type Companion (STT m k) (MK a) = ST (Writer a)
  mapCompanion :: forall {j :: ()} {k :: ()} (f :: MonK m j k) (g :: MonK m j k).
(f ~> g) -> Companion (STT m k) f ~> Companion (STT m k) g
mapCompanion (Mon2 a1 ~> b1
f) = (Writer a1 :~> Writer b1)
-> StT ('ST (Writer a1)) ('ST (Writer b1))
forall m k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong m p, Strong m q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT (Prof (Writer a1) (Writer b1) -> Writer a1 :~> Writer b1
forall {k} {k1} (p :: PRO k k1) (q :: PRO k k1).
Prof p q -> p :~> q
unProf ((a1 ~> b1) -> Writer a1 ~> Writer b1
forall (a :: m) (b :: m). (a ~> b) -> Writer a ~> Writer b
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
map a1 ~> b1
f)) ((Ob a1, Ob b1) => StT ('ST (Writer a1)) ('ST (Writer b1)))
-> (a1 ~> b1) -> StT ('ST (Writer a1)) ('ST (Writer b1))
forall (a :: m) (b :: m) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a1 ~> b1
f
  withObCompanion :: forall {j :: ()} {k :: ()} (f :: MonK m j k) r.
Ob f =>
(Ob (Companion (STT m k) f) => r) -> r
withObCompanion Ob (Companion (STT m k) f) => r
r = r
Ob (Companion (STT m k) f) => r
r
  compToId :: forall (k :: ()). Ob0 (MonK m) k => Companion (STT m k) I ~> I
compToId = (Writer Unit :~> Id) -> StT ('ST (Writer Unit)) ('ST Id)
forall m k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong m p, Strong m q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT \(Writer a ~> Act Unit b
f) -> (a ~> b) -> Id a b
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (forall m k (x :: k). (MonoidalAction m k, Ob x) => Act Unit x ~> x
unitor @m (Act Unit b ~> b) -> (a ~> Act Unit b) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> Act Unit b
f)
  compFromId :: forall (k :: ()). Ob0 (MonK m) k => I ~> Companion (STT m k) I
compFromId = (Id :~> Writer Unit) -> StT ('ST Id) ('ST (Writer Unit))
forall m k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong m p, Strong m q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT \(Id a ~> b
f) -> (a ~> Act Unit b) -> Writer Unit a b
forall {k} {m} (a :: k) (b :: k) (w :: m).
(Ob a, Ob b) =>
(a ~> Act w b) -> Writer w a b
Writer (forall m k (x :: k). (MonoidalAction m k, Ob x) => x ~> Act Unit x
unitorInv @m (b ~> Act Unit b) -> (a ~> b) -> a ~> Act Unit b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
f) ((Ob a, Ob b) => Writer Unit a b) -> (a ~> b) -> Writer Unit a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f
  compToCompose :: forall {i :: ()} {j :: ()} {k :: ()} (f :: MonK m j k)
       (g :: MonK m i j).
Obj f
-> Obj g
-> Companion (STT m k) (O f g)
   ~> O (Companion (STT m k) f) (Companion (STT m k) g)
compToCompose (Mon2 @m1 a1 ~> b1
m1) (Mon2 @m2 a1 ~> b1
m2) =
    a1 ~> b1
b1 ~> b1
m1 (b1 ~> b1)
-> ((Ob b1, Ob b1) =>
    StT ('ST (Writer (b1 ** b1))) ('ST (Writer b1 :.: Writer b1)))
-> StT ('ST (Writer (b1 ** b1))) ('ST (Writer b1 :.: Writer b1))
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// a1 ~> b1
b1 ~> b1
m2 (b1 ~> b1)
-> ((Ob b1, Ob b1) =>
    StT ('ST (Writer (b1 ** b1))) ('ST (Writer b1 :.: Writer b1)))
-> StT ('ST (Writer (b1 ** b1))) ('ST (Writer b1 :.: Writer b1))
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// a1 ~> b1
b1 ~> b1
m1 (b1 ~> b1) -> (b1 ~> b1) -> (b1 ** b1) ~> (b1 ** b1)
forall (x1 :: m) (x2 :: m) (y1 :: m) (y2 :: m).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` a1 ~> b1
b1 ~> b1
m2 ((b1 ** b1) ~> (b1 ** b1))
-> ((Ob (b1 ** b1), Ob (b1 ** b1)) =>
    StT ('ST (Writer (b1 ** b1))) ('ST (Writer b1 :.: Writer b1)))
-> StT ('ST (Writer (b1 ** b1))) ('ST (Writer b1 :.: Writer b1))
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (Writer (b1 ** b1) :~> (Writer b1 :.: Writer b1))
-> StT ('ST (Writer (b1 ** b1))) ('ST (Writer b1 :.: Writer b1))
forall m k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong m p, Strong m q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT \(Writer @_ @b a ~> Act (b1 ** b1) b
f) ->
      let m2b :: Act b1 b ~> Act b1 b
m2b = a1 ~> b1
b1 ~> b1
m2 (b1 ~> b1) -> (b ~> b) -> Act b1 b ~> Act b1 b
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
`act` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b in (a ~> Act b1 (Act b1 b)) -> Writer b1 a (Act b1 b)
forall {k} {m} (a :: k) (b :: k) (w :: m).
(Ob a, Ob b) =>
(a ~> Act w b) -> Writer w a b
Writer (forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv @m @k @m1 @m2 @b (Act (b1 ** b1) b ~> Act b1 (Act b1 b))
-> (a ~> Act (b1 ** b1) b) -> a ~> Act b1 (Act b1 b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> Act (b1 ** b1) b
f) Writer b1 a (Act b1 b)
-> Writer b1 (Act b1 b) b -> (:.:) (Writer b1) (Writer b1) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (Act b1 b ~> Act b1 b) -> Writer b1 (Act b1 b) b
forall {k} {m} (a :: k) (b :: k) (w :: m).
(Ob a, Ob b) =>
(a ~> Act w b) -> Writer w a b
Writer Act b1 b ~> Act b1 b
m2b ((Ob (Act b1 b), Ob (Act b1 b)) =>
 (:.:) (Writer b1) (Writer b1) a b)
-> (Act b1 b ~> Act b1 b) -> (:.:) (Writer b1) (Writer b1) a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Act b1 b ~> Act b1 b
m2b
  compFromCompose :: forall {j1 :: ()} {j2 :: ()} {k :: ()} (f :: MonK m j2 k)
       (g :: MonK m j1 j2).
Obj f
-> Obj g
-> O (Companion (STT m k) f) (Companion (STT m k) g)
   ~> Companion (STT m k) (O f g)
compFromCompose (Mon2 a1 ~> b1
m1) (Mon2 a1 ~> b1
m2) =
    a1 ~> b1
b1 ~> b1
m1 (b1 ~> b1)
-> ((Ob b1, Ob b1) =>
    StT ('ST (Writer b1 :.: Writer b1)) ('ST (Writer (b1 ** b1))))
-> StT ('ST (Writer b1 :.: Writer b1)) ('ST (Writer (b1 ** b1)))
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// a1 ~> b1
b1 ~> b1
m2 (b1 ~> b1)
-> ((Ob b1, Ob b1) =>
    StT ('ST (Writer b1 :.: Writer b1)) ('ST (Writer (b1 ** b1))))
-> StT ('ST (Writer b1 :.: Writer b1)) ('ST (Writer (b1 ** b1)))
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// a1 ~> b1
b1 ~> b1
m1 (b1 ~> b1) -> (b1 ~> b1) -> (b1 ** b1) ~> (b1 ** b1)
forall (x1 :: m) (x2 :: m) (y1 :: m) (y2 :: m).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` a1 ~> b1
b1 ~> b1
m2 ((b1 ** b1) ~> (b1 ** b1))
-> ((Ob (b1 ** b1), Ob (b1 ** b1)) =>
    StT ('ST (Writer b1 :.: Writer b1)) ('ST (Writer (b1 ** b1))))
-> StT ('ST (Writer b1 :.: Writer b1)) ('ST (Writer (b1 ** b1)))
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// ((Writer b1 :.: Writer b1) :~> Writer (b1 ** b1))
-> StT ('ST (Writer b1 :.: Writer b1)) ('ST (Writer (b1 ** b1)))
forall m k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong m p, Strong m q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT \(Writer @_ @_ @m1 a ~> Act b1 b
f :.: Writer @_ @c @m2 b ~> Act b1 b
g) ->
      (a ~> Act (b1 ** b1) b) -> Writer (b1 ** b1) a b
forall {k} {m} (a :: k) (b :: k) (w :: m).
(Ob a, Ob b) =>
(a ~> Act w b) -> Writer w a b
Writer (forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator @m @k @m1 @m2 @c (Act b1 (Act b1 b) ~> Act (b1 ** b1) b)
-> (a ~> Act b1 (Act b1 b)) -> a ~> Act (b1 ** b1) b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (b1 ~> b1) -> (b ~> Act b1 b) -> Act b1 b ~> Act b1 (Act b1 b)
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act a1 ~> b1
b1 ~> b1
m1 b ~> Act b1 b
g (Act b1 b ~> Act b1 (Act b1 b))
-> (a ~> Act b1 b) -> a ~> Act b1 (Act b1 b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> Act b1 b
f)

instance
  (MonoidalAction m k, M.SymMonoidal m, Adjunction (PK l) (PK r), Ob l, Ob r, Strong m r, Strong m l)
  => Adjunction (ST l :: STT m k i j) (ST r)
  where
  unit :: I ~> O ('ST r) ('ST l)
unit = (Id :~> (r :.: l)) -> StT ('ST Id) ('ST (r :.: l))
forall m k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong m p, Strong m q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT (case forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction l r =>
I ~> O r l
forall (l :: PROFK k k) (r :: PROFK k k).
Adjunction l r =>
I ~> O r l
unit @(PK l) @(PK r) of Prof p1 :~> q1
f -> p1 a b -> q1 a b
Id a b -> (:.:) r l a b
p1 :~> q1
f)
  counit :: O ('ST l) ('ST r) ~> I
counit = ((l :.: r) :~> Id) -> StT ('ST (l :.: r)) ('ST Id)
forall m k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong m p, Strong m q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT (case forall {k} {kk :: k -> k -> Type} {c :: k} {d :: k} (l :: kk c d)
       (r :: kk d c).
Adjunction l r =>
O l r ~> I
forall (l :: PROFK k k) (r :: PROFK k k).
Adjunction l r =>
O l r ~> I
counit @(PK l) @(PK r) of Prof p1 :~> q1
f -> p1 a b -> q1 a b
(:.:) l r a b -> Id a b
p1 :~> q1
f)

instance (MonoidalAction m k, M.SymMonoidal m, Ob (M.Unit @m)) => Equipment (STT m k) (MonK m) where
  type Conjoint (STT m k) (MK a) = ST (Reader (OP a))
  mapConjoint :: forall {j :: ()} {k :: ()} (f :: MonK m j k) (g :: MonK m j k).
(f ~> g) -> Conjoint (STT m k) g ~> Conjoint (STT m k) f
mapConjoint (Mon2 a1 ~> b1
f) = (Reader ('OP b1) :~> Reader ('OP a1))
-> StT ('ST (Reader ('OP b1))) ('ST (Reader ('OP a1)))
forall m k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong m p, Strong m q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT (Prof (Reader ('OP b1)) (Reader ('OP a1))
-> Reader ('OP b1) :~> Reader ('OP a1)
forall {k} {k1} (p :: PRO k k1) (q :: PRO k k1).
Prof p q -> p :~> q
unProf (('OP b1 ~> 'OP a1) -> Reader ('OP b1) ~> Reader ('OP a1)
forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (b :: k1).
Functor f =>
(a ~> b) -> f a ~> f b
forall (a :: OPPOSITE m) (b :: OPPOSITE m).
(a ~> b) -> Reader a ~> Reader b
map ((a1 ~> b1) -> Op (~>) ('OP b1) ('OP a1)
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p ('OP a1) ('OP b1)
Op a1 ~> b1
f))) ((Ob a1, Ob b1) =>
 StT ('ST (Reader ('OP b1))) ('ST (Reader ('OP a1))))
-> (a1 ~> b1)
-> StT ('ST (Reader ('OP b1))) ('ST (Reader ('OP a1)))
forall (a :: m) (b :: m) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a1 ~> b1
f
  withObConjoint :: forall {j :: ()} {k :: ()} (f :: MonK m j k) r.
Ob f =>
(Ob (Conjoint (STT m k) f) => r) -> r
withObConjoint Ob (Conjoint (STT m k) f) => r
r = r
Ob (Conjoint (STT m k) f) => r
r

type STSq (p :: k +-> k) (q :: k +-> k) (a :: m) (b :: m) =
  Sq '(ST p :: STT m k '() '(), MK a :: MonK m '() '()) '(ST q, MK b :: MonK m '() '())

crossing
  :: forall {k} {m} p a. (Strong m (p :: k +-> k), Ob (a :: m), MonoidalAction m k, M.SymMonoidal m) => STSq p p a a
crossing :: forall {k} {m} (p :: k +-> k) (a :: m).
(Strong m p, Ob a, MonoidalAction m k, SymMonoidal m) =>
STSq p p a a
crossing =
  (O (Companion (STT m k) ('MK a)) ('ST p)
 ~> O ('ST p) (Companion (STT m k) ('MK a)))
-> Sq '( 'ST p, 'MK a) '( 'ST p, 'MK a)
forall {c} {hk :: CAT c} {vk :: CAT c} {h :: c} {i :: c} {j :: c}
       {k :: c} (p :: hk j h) (q :: hk k i) (f :: vk h i) (g :: vk j k).
(Ob0 vk h, Ob0 vk i, Ob0 vk j, Ob0 vk k, Ob p, Ob q, Ob f, Ob g) =>
(O (Companion hk f) p ~> O q (Companion hk g))
-> Sq '(p, f) '(q, g)
Sq
    ( ((Writer a :.: p) :~> (p :.: Writer a))
-> StT ('ST (Writer a :.: p)) ('ST (p :.: Writer a))
forall m k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong m p, Strong m q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT \(Writer @_ @_ @w a ~> Act a b
f :.: p b b
p) ->
        (a ~> Act a b) -> p (Act a b) (Act a b) -> p a (Act a b)
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> Act a b
f (((a ~> a) -> p b b -> p (Act a b) (Act a b)
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) p b b
p)) p a (Act a b) -> Writer a (Act a b) b -> (:.:) p (Writer a) a b
forall {j} {k} {i} (p :: j +-> k) (a :: k) (b :: j) (q :: i +-> j)
       (c :: i).
p a b -> q b c -> (:.:) p q a c
:.: (Act a b ~> Act a b) -> Writer a (Act a b) b
forall {k} {m} (a :: k) (b :: k) (w :: m).
(Ob a, Ob b) =>
(a ~> Act w b) -> Writer w a b
Writer Act a b ~> Act a b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id
          ((Ob a, Ob (Act a b)) => (:.:) p (Writer a) a b)
-> (a ~> Act a b) -> (:.:) p (Writer a) a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> Act a b
f
          ((Ob b, Ob b) => (:.:) p (Writer a) a b)
-> p b b -> (:.:) p (Writer a) a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p b b
p
          ((Ob (Act a b), Ob (Act a b)) => (:.:) p (Writer a) a b)
-> (Act a b ~> Act a b) -> (:.:) p (Writer a) a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @w (a ~> a) -> (b ~> b) -> Act a b ~> Act a b
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
`act` p b b -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt p b b
p
    )