{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ImpredicativeTypes #-}

module Proarrow.Category.Equipment.Stateful where

import Prelude (($))

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 (MonoidalProfunctor, par)
import Proarrow.Category.Monoidal qualified as M
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), SelfAction, Strong (..), toSelfAct)
import Proarrow.Category.Monoidal.Distributive (Distributive (..))
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.Object (pattern Obj, type Obj)
import Proarrow.Object.BinaryCoproduct (Coprod, HasBinaryCoproducts (..), HasCoproducts, codiag, copar)
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Coproduct (coproduct, (:+:) (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Product ((:*:) (..))
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) -> (a ~> b) -> c ~> d
(c ~> a) -> (b ~> d) -> StT a b -> StT c d
forall {k} (p :: 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 (ZonkAny 0) (ZonkAny 1)), Ob (q (ZonkAny 0) (ZonkAny 1))) =>
r
(Ob a, Ob b) => r
r ((Ob (p (ZonkAny 0) (ZonkAny 1)),
  Ob (q (ZonkAny 0) (ZonkAny 1))) =>
 r)
-> (p (ZonkAny 0) (ZonkAny 1) -> q (ZonkAny 0) (ZonkAny 1)) -> r
forall a b 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
\\ p (ZonkAny 0) (ZonkAny 1) -> q (ZonkAny 0) (ZonkAny 1)
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 :: 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 :: 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
  withOb0s :: forall {j :: ()} {k :: ()} (a :: STT m k j k) r.
Ob a =>
((Ob0 (STT m k) j, Ob0 (STT m k) k) => r) -> r
withOb0s (Ob0 (STT m k) j, Ob0 (STT m k) k) => r
r = r
(Ob0 (STT m k) j, Ob0 (STT m k) k) => 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 :: j +-> k) (c :: k) (a :: k) (b :: j).
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 {j} {k} (a :: k) (b :: j) (p :: j +-> k).
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 :: j +-> k) (b :: j) (d :: j) (a :: k).
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 :: k1 +-> k2).
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) => 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 {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
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) => Companion (STT m k) f ~> Companion (STT m k) g)
-> (a1 ~> b1) -> Companion (STT m k) f ~> Companion (STT m k) g
forall (a :: m) (b :: m) 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
\\ 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 :: 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} (b :: k) (a :: k) (w :: m).
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 :: 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 :: j +-> k) (a :: k) (b :: j) 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
m1 (a1 ~> b1)
-> ((Ob a1, Ob b1) =>
    Companion (STT m k) (O f g)
    ~> O (Companion (STT m k) f) (Companion (STT m k) g))
-> Companion (STT m k) (O f g)
   ~> O (Companion (STT m k) f) (Companion (STT m k) g)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// a1 ~> b1
m2 (a1 ~> b1)
-> ((Ob a1, Ob b1) =>
    Companion (STT m k) (O f g)
    ~> O (Companion (STT m k) f) (Companion (STT m k) g))
-> Companion (STT m k) (O f g)
   ~> O (Companion (STT m k) f) (Companion (STT m k) g)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// a1 ~> b1
m1 (a1 ~> b1) -> (a1 ~> b1) -> (a1 ** a1) ~> (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
m2 ((a1 ** a1) ~> (b1 ** b1))
-> ((Ob (a1 ** a1), Ob (b1 ** b1)) =>
    Companion (STT m k) (O f g)
    ~> O (Companion (STT m k) f) (Companion (STT m k) g))
-> Companion (STT m k) (O f g)
   ~> O (Companion (STT m k) f) (Companion (STT m k) g)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) 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} (b :: k) (a :: k) (w :: m).
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 (a1 ** a1) b ~> Act a1 (Act a1 b))
-> (a ~> Act (a1 ** a1) b) -> a ~> Act a1 (Act a1 b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> Act (a1 ** a1) b
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} (b :: k) (a :: k) (w :: m).
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 :: j +-> k) (a :: k) (b :: j) 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
m1 (a1 ~> b1)
-> ((Ob a1, Ob b1) =>
    O (Companion (STT m k) f) (Companion (STT m k) g)
    ~> Companion (STT m k) (O f g))
-> O (Companion (STT m k) f) (Companion (STT m k) g)
   ~> Companion (STT m k) (O f g)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// a1 ~> b1
m2 (a1 ~> b1)
-> ((Ob a1, Ob b1) =>
    O (Companion (STT m k) f) (Companion (STT m k) g)
    ~> Companion (STT m k) (O f g))
-> O (Companion (STT m k) f) (Companion (STT m k) g)
   ~> Companion (STT m k) (O f g)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// a1 ~> b1
m1 (a1 ~> b1) -> (a1 ~> b1) -> (a1 ** a1) ~> (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
m2 ((a1 ** a1) ~> (b1 ** b1))
-> ((Ob (a1 ** a1), Ob (b1 ** b1)) =>
    O (Companion (STT m k) f) (Companion (STT m k) g)
    ~> Companion (STT m k) (O f g))
-> O (Companion (STT m k) f) (Companion (STT m k) g)
   ~> Companion (STT m k) (O f g)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) 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} (b :: k) (a :: k) (w :: m).
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 :: 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 :: 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) => 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 {k1} {k} (p :: k1 +-> k) (q :: k1 +-> k).
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) => Conjoint (STT m k) g ~> Conjoint (STT m k) f)
-> (a1 ~> b1) -> Conjoint (STT m k) g ~> Conjoint (STT m k) f
forall (a :: m) (b :: m) 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
\\ 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 '() '())

unSTSq
  :: forall {m} {k} p q (a :: m) b
   . (M.SymMonoidal m)
  => STSq p q a b
  -> (forall x y. p x y -> q (Act a x) (Act b y), Obj a, Obj b, Obj (ST p :: STT m k '() '()), Obj (ST q :: STT m k '() '()))
unSTSq :: forall {m} {k} (p :: k +-> k) (q :: k +-> k) (a :: m) (b :: m).
SymMonoidal m =>
STSq p q a b
-> (forall (x :: k) (y :: k). p x y -> q (Act a x) (Act b y),
    Obj a, Obj b, Obj ('ST p), Obj ('ST q))
unSTSq (Sq (StT p :~> q
f)) = (\p x y
p -> p x y
p p x y
-> ((Ob x, Ob y) => q (Act a x) (Act b y)) -> q (Act a x) (Act b y)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// case p (Act a x) y -> q (Act a x) y
p :~> q
f ((Act a x ~> Act a x) -> Writer a (Act a x) x
forall {k} {m} (b :: k) (a :: k) (w :: m).
Ob b =>
(a ~> Act w b) -> Writer w a b
Writer (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a Obj a -> (x ~> x) -> Act a x ~> Act a x
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 x y -> x ~> x
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src p x y
p) Writer a (Act a x) x -> p x y -> (:.:) (Writer a) p (Act a x) y
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 x y
p) of q (Act a x) b
q :.: Writer b ~> Act b y
g -> (b ~> Act b y) -> q (Act a x) b -> q (Act a x) (Act b y)
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> Act b y
g q (Act a x) b
q, Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
Obj, Obj b
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
Obj, Obj ('ST p)
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
Obj, Obj ('ST q)
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
Obj)

pattern STSq
  :: forall {m} {k} (p :: k +-> k) q (a :: m) b
   . (M.SymMonoidal m, MonoidalAction m k)
  => (Strong m p, Strong m q, Ob a, Ob b)
  => (forall x y. p x y -> q (Act a x) (Act b y)) -> STSq p q a b
pattern $bSTSq :: forall {m} {k} (p :: k +-> k) (q :: k +-> k) (a :: m) (b :: m).
(SymMonoidal m, MonoidalAction m k, Strong m p, Strong m q, Ob a,
 Ob b) =>
(forall (x :: k) (y :: k). p x y -> q (Act a x) (Act b y))
-> STSq p q a b
$mSTSq :: forall {r} {m} {k} {p :: k +-> k} {q :: k +-> k} {a :: m} {b :: m}.
(SymMonoidal m, MonoidalAction m k) =>
STSq p q a b
-> ((Strong m p, Strong m q, Ob a, Ob b) =>
    (forall (x :: k) (y :: k). p x y -> q (Act a x) (Act b y)) -> r)
-> ((# #) -> r)
-> r
STSq f <- (unSTSq -> (f, Obj, Obj, Obj, Obj))
  where
    STSq forall (x :: k) (y :: k). p x y -> q (Act a x) (Act b y)
f = (O (Companion (STT m k) ('MK a)) ('ST p)
 ~> O ('ST q) (Companion (STT m k) ('MK b)))
-> Sq '( 'ST p, 'MK a) '( 'ST q, 'MK b)
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) :~> (q :.: Writer b))
-> StT ('ST (Writer a :.: p)) ('ST (q :.: Writer b))
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 a b
g :.: p b b
p) -> (a ~> Act a b) -> q (Act a b) (Act b b) -> q a (Act b b)
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> Act a b
g (p b b -> q (Act a b) (Act b b)
forall (x :: k) (y :: k). p x y -> q (Act a x) (Act b y)
f p b b
p) q a (Act b b) -> Writer b (Act b b) b -> (:.:) q (Writer 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
:.: (Act b b ~> Act b b) -> Writer b (Act b b) b
forall {k} {m} (b :: k) (a :: k) (w :: m).
Ob b =>
(a ~> Act w b) -> Writer w a b
Writer (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b Obj b -> (b ~> b) -> Act b b ~> Act b 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 :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt p b b
p) ((Ob b, Ob b) => (:.:) q (Writer b) a b)
-> p b b -> (:.:) q (Writer b) a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p b b
p))

{-# COMPLETE STSq #-}

crossing
  :: forall {k} {m} p a. (Strong m (p :: k +-> k), Ob (a :: m), M.SymMonoidal m) => STSq p p a a
crossing :: forall {k} {m} (p :: k +-> k) (a :: m).
(Strong m p, Ob a, SymMonoidal m) =>
STSq p p a a
crossing = (forall (x :: k) (y :: k). p x y -> p (Act a x) (Act a y))
-> STSq p p a a
forall {m} {k} (p :: k +-> k) (q :: k +-> k) (a :: m) (b :: m).
(SymMonoidal m, MonoidalAction m k, Strong m p, Strong m q, Ob a,
 Ob b) =>
(forall (x :: k) (y :: k). p x y -> q (Act a x) (Act b y))
-> STSq p q a b
STSq ((a ~> a) -> p x y -> p (Act a x) (Act a y)
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))

pi0
  :: forall {m} {k} p q. (Strong m (p :: k +-> k), Strong m q, M.SymMonoidal m) => STSq (p :*: q) p (M.Unit :: m) M.Unit
pi0 :: forall {m} {k} (p :: k +-> k) (q :: k +-> k).
(Strong m p, Strong m q, SymMonoidal m) =>
STSq (p :*: q) p Unit Unit
pi0 = (forall (x :: k) (y :: k).
 (:*:) p q x y -> p (Act Unit x) (Act Unit y))
-> STSq (p :*: q) p Unit Unit
forall {m} {k} (p :: k +-> k) (q :: k +-> k) (a :: m) (b :: m).
(SymMonoidal m, MonoidalAction m k, Strong m p, Strong m q, Ob a,
 Ob b) =>
(forall (x :: k) (y :: k). p x y -> q (Act a x) (Act b y))
-> STSq p q a b
STSq \(p x y
p :*: q x y
_) -> (Unit ~> Unit) -> p x y -> p (Act Unit x) (Act Unit y)
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 @(M.Unit :: m)) p x y
p

pi1
  :: forall {m} {k} p q. (Strong m (p :: k +-> k), Strong m q, M.SymMonoidal m) => STSq (p :*: q) q (M.Unit :: m) M.Unit
pi1 :: forall {m} {k} (p :: k +-> k) (q :: k +-> k).
(Strong m p, Strong m q, SymMonoidal m) =>
STSq (p :*: q) q Unit Unit
pi1 = (forall (x :: k) (y :: k).
 (:*:) p q x y -> q (Act Unit x) (Act Unit y))
-> STSq (p :*: q) q Unit Unit
forall {m} {k} (p :: k +-> k) (q :: k +-> k) (a :: m) (b :: m).
(SymMonoidal m, MonoidalAction m k, Strong m p, Strong m q, Ob a,
 Ob b) =>
(forall (x :: k) (y :: k). p x y -> q (Act a x) (Act b y))
-> STSq p q a b
STSq \(p x y
_ :*: q x y
q) -> (Unit ~> Unit) -> q x y -> q (Act Unit x) (Act Unit y)
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> q x y -> q (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 @(M.Unit :: m)) q x y
q

mult
  :: forall {m} {k} (p :: k +-> k) q r (a :: m) b
   . (Strong m p, Strong m q, Strong m r, M.SymMonoidal m, Ob a, Ob b)
  => STSq p q a b -> STSq p r a b -> STSq p (q :*: r) a b
STSq forall (x :: k) (y :: k). p x y -> q (Act a x) (Act b y)
n mult :: forall {m} {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k)
       (a :: m) (b :: m).
(Strong m p, Strong m q, Strong m r, SymMonoidal m, Ob a, Ob b) =>
STSq p q a b -> STSq p r a b -> STSq p (q :*: r) a b
`mult` STSq forall (x :: k) (y :: k). p x y -> r (Act a x) (Act b y)
m = (forall (x :: k) (y :: k). p x y -> (:*:) q r (Act a x) (Act b y))
-> STSq p (q :*: r) a b
forall {m} {k} (p :: k +-> k) (q :: k +-> k) (a :: m) (b :: m).
(SymMonoidal m, MonoidalAction m k, Strong m p, Strong m q, Ob a,
 Ob b) =>
(forall (x :: k) (y :: k). p x y -> q (Act a x) (Act b y))
-> STSq p q a b
STSq (\p x y
p -> p x y -> q (Act a x) (Act b y)
forall (x :: k) (y :: k). p x y -> q (Act a x) (Act b y)
n p x y
p q (Act a x) (Act b y)
-> r (Act a x) (Act b y) -> (:*:) q r (Act a x) (Act b y)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> q a b -> (:*:) p q a b
:*: p x y -> r (Act a x) (Act b y)
forall (x :: k) (y :: k). p x y -> r (Act a x) (Act b y)
m p x y
p)

ip0
  :: forall {m} {k} p q. (Strong m (p :: k +-> k), Strong m q, M.SymMonoidal m) => STSq p (p :+: q) (M.Unit :: m) M.Unit
ip0 :: forall {m} {k} (p :: k +-> k) (q :: k +-> k).
(Strong m p, Strong m q, SymMonoidal m) =>
STSq p (p :+: q) Unit Unit
ip0 = (forall (x :: k) (y :: k).
 p x y -> (:+:) p q (Act Unit x) (Act Unit y))
-> STSq p (p :+: q) Unit Unit
forall {m} {k} (p :: k +-> k) (q :: k +-> k) (a :: m) (b :: m).
(SymMonoidal m, MonoidalAction m k, Strong m p, Strong m q, Ob a,
 Ob b) =>
(forall (x :: k) (y :: k). p x y -> q (Act a x) (Act b y))
-> STSq p q a b
STSq \p x y
p -> (Unit ~> Unit)
-> (:+:) p q x y -> (:+:) p q (Act Unit x) (Act Unit y)
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> (:+:) p q x y -> (:+:) p q (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 @(M.Unit :: m)) (p x y -> (:+:) p q x y
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> (:+:) p q a b
InjL p x y
p)

ip1
  :: forall {m} {k} p q. (Strong m (p :: k +-> k), Strong m q, M.SymMonoidal m) => STSq q (p :+: q) (M.Unit :: m) M.Unit
ip1 :: forall {m} {k} (p :: k +-> k) (q :: k +-> k).
(Strong m p, Strong m q, SymMonoidal m) =>
STSq q (p :+: q) Unit Unit
ip1 = (forall (x :: k) (y :: k).
 q x y -> (:+:) p q (Act Unit x) (Act Unit y))
-> STSq q (p :+: q) Unit Unit
forall {m} {k} (p :: k +-> k) (q :: k +-> k) (a :: m) (b :: m).
(SymMonoidal m, MonoidalAction m k, Strong m p, Strong m q, Ob a,
 Ob b) =>
(forall (x :: k) (y :: k). p x y -> q (Act a x) (Act b y))
-> STSq p q a b
STSq \q x y
p -> (Unit ~> Unit)
-> (:+:) p q x y -> (:+:) p q (Act Unit x) (Act Unit y)
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> (:+:) p q x y -> (:+:) p q (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 @(M.Unit :: m)) (q x y -> (:+:) p q x y
forall {j} {k} (q :: j +-> k) (a :: k) (b :: j) (p :: j +-> k).
q a b -> (:+:) p q a b
InjR q x y
p)

plus
  :: forall {m} {k} (p :: k +-> k) q r (a :: m) b
   . (Strong m p, Strong m q, Strong m r, M.SymMonoidal m, Ob a, Ob b)
  => STSq p r a b -> STSq q r a b -> STSq (p :+: q) r a b
STSq forall (x :: k) (y :: k). p x y -> r (Act a x) (Act b y)
n plus :: forall {m} {k} (p :: k +-> k) (q :: k +-> k) (r :: k +-> k)
       (a :: m) (b :: m).
(Strong m p, Strong m q, Strong m r, SymMonoidal m, Ob a, Ob b) =>
STSq p r a b -> STSq q r a b -> STSq (p :+: q) r a b
`plus` STSq forall (x :: k) (y :: k). q x y -> r (Act a x) (Act b y)
m = (forall (x :: k) (y :: k). (:+:) p q x y -> r (Act a x) (Act b y))
-> STSq (p :+: q) r a b
forall {m} {k} (p :: k +-> k) (q :: k +-> k) (a :: m) (b :: m).
(SymMonoidal m, MonoidalAction m k, Strong m p, Strong m q, Ob a,
 Ob b) =>
(forall (x :: k) (y :: k). p x y -> q (Act a x) (Act b y))
-> STSq p q a b
STSq ((p x y -> r (Act a x) (Act b y))
-> (q x y -> r (Act a x) (Act b y))
-> (:+:) p q x y
-> r (Act a x) (Act b y)
forall {k} {j} (p :: k -> j -> Type) (x :: k) (y :: j) r
       (q :: k -> j -> Type).
(p x y -> r) -> (q x y -> r) -> (:+:) p q x y -> r
coproduct p x y -> r (Act a x) (Act b y)
forall (x :: k) (y :: k). p x y -> r (Act a x) (Act b y)
n q x y -> r (Act a x) (Act b y)
forall (x :: k) (y :: k). q x y -> r (Act a x) (Act b y)
m)

sigma0
  :: forall {m} {k} (a :: m) b
   . (Ob a, Ob b, M.SymMonoidal m, MonoidalAction m k, HasCoproducts m) => STSq (Id :: k +-> k) Id a (a || b)
sigma0 :: forall {m} {k} (a :: m) (b :: m).
(Ob a, Ob b, SymMonoidal m, MonoidalAction m k, HasCoproducts m) =>
STSq Id Id a (a || b)
sigma0 = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @m @a @b ((Ob (a || b) => STSq Id Id a (a || b)) -> STSq Id Id a (a || b))
-> (Ob (a || b) => STSq Id Id a (a || b)) -> STSq Id Id a (a || b)
forall a b. (a -> b) -> a -> b
$ (forall (x :: k) (y :: k). Id x y -> Id (Act a x) (Act (a || b) y))
-> STSq Id Id a (a || b)
forall {m} {k} (p :: k +-> k) (q :: k +-> k) (a :: m) (b :: m).
(SymMonoidal m, MonoidalAction m k, Strong m p, Strong m q, Ob a,
 Ob b) =>
(forall (x :: k) (y :: k). p x y -> q (Act a x) (Act b y))
-> STSq p q a b
STSq \(Id x ~> y
f) -> (Act a x ~> Act (a || b) y) -> Id (Act a x) (Act (a || b) y)
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id ((a ~> (a || b)) -> (x ~> y) -> Act a x ~> Act (a || b) y
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 k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @m @a @b) x ~> y
f)

sigma1
  :: forall {m} {k} (a :: m) b
   . (Ob a, Ob b, M.SymMonoidal m, MonoidalAction m k, HasCoproducts m) => STSq (Id :: k +-> k) Id b (a || b)
sigma1 :: forall {m} {k} (a :: m) (b :: m).
(Ob a, Ob b, SymMonoidal m, MonoidalAction m k, HasCoproducts m) =>
STSq Id Id b (a || b)
sigma1 = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @m @a @b ((Ob (a || b) => STSq Id Id b (a || b)) -> STSq Id Id b (a || b))
-> (Ob (a || b) => STSq Id Id b (a || b)) -> STSq Id Id b (a || b)
forall a b. (a -> b) -> a -> b
$ (forall (x :: k) (y :: k). Id x y -> Id (Act b x) (Act (a || b) y))
-> STSq Id Id b (a || b)
forall {m} {k} (p :: k +-> k) (q :: k +-> k) (a :: m) (b :: m).
(SymMonoidal m, MonoidalAction m k, Strong m p, Strong m q, Ob a,
 Ob b) =>
(forall (x :: k) (y :: k). p x y -> q (Act a x) (Act b y))
-> STSq p q a b
STSq \(Id x ~> y
f) -> (Act b x ~> Act (a || b) y) -> Id (Act b x) (Act (a || b) y)
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id ((b ~> (a || b)) -> (x ~> y) -> Act b x ~> Act (a || b) y
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 k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @m @a @b) x ~> y
f)

copair
  :: forall {k} (p :: k +-> k) q (a :: k) b c
   . (Strong k p, Strong k q, M.SymMonoidal k, Distributive k, SelfAction k, MonoidalProfunctor (Coprod q), Ob a, Ob b, Ob c)
  => STSq p q a c -> STSq p q b c -> STSq p q (a || b) c
STSq forall (x :: k) (y :: k). p x y -> q (Act a x) (Act c y)
n copair :: forall {k} (p :: k +-> k) (q :: k +-> k) (a :: k) (b :: k)
       (c :: k).
(Strong k p, Strong k q, SymMonoidal k, Distributive k,
 SelfAction k, MonoidalProfunctor (Coprod q), Ob a, Ob b, Ob c) =>
STSq p q a c -> STSq p q b c -> STSq p q (a || b) c
`copair` STSq forall (x :: k) (y :: k). p x y -> q (Act b x) (Act c y)
m =
  forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a @b ((Ob (a || b) => STSq p q (a || b) c) -> STSq p q (a || b) c)
-> (Ob (a || b) => STSq p q (a || b) c) -> STSq p q (a || b) c
forall a b. (a -> b) -> a -> b
$
    (forall (x :: k) (y :: k). p x y -> q (Act (a || b) x) (Act c y))
-> STSq p q (a || b) c
forall {m} {k} (p :: k +-> k) (q :: k +-> k) (a :: m) (b :: m).
(SymMonoidal m, MonoidalAction m k, Strong m p, Strong m q, Ob a,
 Ob b) =>
(forall (x :: k) (y :: k). p x y -> q (Act a x) (Act b y))
-> STSq p q a b
STSq
      ( \(p x y
p :: p x y) ->
          (Act (a || b) x ~> (Act a x || Act b x))
-> ((Act c y || Act c y) ~> Act c y)
-> q (Act a x || Act b x) (Act c y || Act c y)
-> q (Act (a || b) x) (Act c y)
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> q a b -> q c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap ((forall (a :: k) (b :: k).
(SelfAction k, Ob a, Ob b) =>
(a ** b) ~> Act a b
forall {k} (a :: k) (b :: k).
(SelfAction k, Ob a, Ob b) =>
(a ** b) ~> Act a b
toSelfAct @a @x ((a ** x) ~> Act a x)
-> ((b ** x) ~> Act b x)
-> ((a ** x) || (b ** x)) ~> (Act a x || Act b x)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryCoproducts k =>
(a ~> x) -> (b ~> y) -> (a || b) ~> (x || y)
+++ forall (a :: k) (b :: k).
(SelfAction k, Ob a, Ob b) =>
(a ** b) ~> Act a b
forall {k} (a :: k) (b :: k).
(SelfAction k, Ob a, Ob b) =>
(a ** b) ~> Act a b
toSelfAct @b @x) (((a ** x) || (b ** x)) ~> (Act a x || Act b x))
-> (((a || b) ** x) ~> ((a ** x) || (b ** x)))
-> ((a || b) ** x) ~> (Act a x || Act b x)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @k @a @b @x) (forall m k (a :: m) (x :: k) r.
(MonoidalAction m k, Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @k @k @c @y (Act c y || Act c y) ~> Act c y
Ob (Act c y) => (Act c y || Act c y) ~> Act c y
forall {k} (a :: k). (HasBinaryCoproducts k, Ob a) => (a || a) ~> a
codiag) ((p x y -> q (Act a x) (Act c y)
forall (x :: k) (y :: k). p x y -> q (Act a x) (Act c y)
n p x y
p q (Act a x) (Act c y)
-> q (Act b x) (Act c y)
-> q (Act a x || Act b x) (Act c y || Act c y)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) (c :: k2)
       (d :: k1).
MonoidalProfunctor (Coprod p) =>
p a b -> p c d -> p (a || c) (b || d)
`copar` p x y -> q (Act b x) (Act c y)
forall (x :: k) (y :: k). p x y -> q (Act b x) (Act c y)
m p x y
p))
            ((Ob x, Ob y) => q (Act (a || b) x) (Act c y))
-> p x y -> q (Act (a || b) x) (Act c y)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p x y
p
      )