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

module Proarrow.Category.Equipment.Stateful where

import Prelude (type (~))

import Proarrow.Adjunction (Proadjunction)
import Proarrow.Category.Bicategory (Adj (..), Adjunction (..), Adjunction_ (..), Bicategory (..))
import Proarrow.Category.Bicategory.Prof (PROFK (..), Prof (..))
import Proarrow.Category.Equipment (Cotight, CotightAdjoint, Equipment (..), IsOb, Tight, TightAdjoint, WithObO2 (..))
import Proarrow.Category.Monoidal.Action (SelfAction, Strong (..))
import Proarrow.Category.Opposite (OPPOSITE (..))
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Is
  , Kind
  , Profunctor (..)
  , Promonad (..)
  , UN
  , dimapDefault
  , lmap
  , obj
  , rmap
  , src
  , tgt
  , (:~>)
  , type (+->)
  )
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Coproduct ((:+:) (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Product ((:*:) (..))
import Proarrow.Promonad.Reader (Reader (..))
import Proarrow.Promonad.Writer (Writer (..))

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

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

instance (SelfAction k) => Bicategory (STT' k) where
  type I = ST Id
  type a `O` b = ST (UN ST a :.: UN ST b)
  withOb2 :: forall {i :: ()} {j :: ()} {k :: ()} (a :: STT' k j k)
       (b :: STT' k i j) r.
(Ob a, Ob b, Ob0 (STT' k) i, Ob0 (STT' k) j, Ob0 (STT' 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' k j k) r.
Ob a =>
((Ob0 (STT' k) j, Ob0 (STT' k) k) => r) -> r
withOb0s (Ob0 (STT' k) j, Ob0 (STT' k) k) => r
r = r
(Ob0 (STT' k) j, Ob0 (STT' k) k) => r
r
  StT p :~> q
m o :: forall {i :: ()} (j :: ()) (k :: ()) (a :: STT' k j k)
       (b :: STT' k j k) (c :: STT' k i j) (d :: STT' 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 k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong k p, Strong k 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' k) i, Ob0 (STT' k) j, Ob ps, Ob qs) => r
r \\\ :: forall (i :: ()) (j :: ()) (ps :: STT' k i j) (qs :: STT' k i j) r.
((Ob0 (STT' k) i, Ob0 (STT' k) j, Ob ps, Ob qs) => r)
-> (ps ~> qs) -> r
\\\ StT{} = r
(Ob0 (STT' k) i, Ob0 (STT' k) j, Ob ps, Ob qs) => r
r
  leftUnitor :: forall {i :: ()} {j :: ()} (a :: STT' k i j).
(Ob0 (STT' k) i, Ob0 (STT' 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 k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong k p, Strong k 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' k i j).
(Ob0 (STT' k) i, Ob0 (STT' 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 k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong k p, Strong k 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' k i j).
(Ob0 (STT' k) i, Ob0 (STT' 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 k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong k p, Strong k 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' k i j).
(Ob0 (STT' k) i, Ob0 (STT' 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 k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong k p, Strong k 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' k j k)
       (b :: STT' k i j) (c :: STT' k h i).
(Ob0 (STT' k) h, Ob0 (STT' k) i, Ob0 (STT' k) j, Ob0 (STT' 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 k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong k p, Strong k 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' k j k)
       (b :: STT' k i j) (c :: STT' k h i).
(Ob0 (STT' k) h, Ob0 (STT' k) i, Ob0 (STT' k) j, Ob0 (STT' 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 k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong k p, Strong k 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

instance
  (SelfAction k, Adjunction (PK l) (PK r), Ob l, Ob r, Strong k r, Strong k l)
  => Adjunction_ (ST l :: STT' k i j) (ST r)
  where
  adj :: Adj ('ST l) ('ST r)
adj =
    Adj
      { adjUnit :: I ~> O ('ST r) ('ST l)
adjUnit = (Id :~> (r :.: l)) -> StT ('ST Id) ('ST (r :.: l))
forall k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong k p, Strong k 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)
      , adjCounit :: O ('ST l) ('ST r) ~> I
adjCounit = ((l :.: r) :~> Id) -> StT ('ST (l :.: r)) ('ST Id)
forall k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong k p, Strong k 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)
      }

class
  ( IsReader (WithReader p)
  , Strong k (WithReader p)
  , Proadjunction p (WithReader p)
  , WithWriter (WithReader p) ~ p
  ) =>
  IsWriter (p :: k +-> k)
  where
  type WithReader p :: k +-> k
instance (SelfAction k) => IsWriter (Id :: k +-> k) where type WithReader Id = Id
instance (SelfAction k, Ob (a :: k)) => IsWriter (Writer a :: k +-> k) where
  type WithReader (Writer a) = Reader (OP a)
instance (IsWriter p, IsWriter q) => IsWriter (p :.: q) where
  type WithReader (p :.: q) = WithReader q :.: WithReader p

class
  ( IsWriter (WithWriter p)
  , Strong k (WithWriter p)
  , Proadjunction (WithWriter p) p
  , WithReader (WithWriter p) ~ p
  ) =>
  IsReader (p :: k +-> k)
  where
  type WithWriter p :: k +-> k
instance (SelfAction k) => IsReader (Id :: k +-> k) where type WithWriter Id = Id
instance (SelfAction k, Ob (a :: k)) => IsReader (Reader (OP a) :: k +-> k) where
  type WithWriter (Reader (OP a)) = Writer a
instance (IsReader p, IsReader q) => IsReader (p :.: q) where
  type WithWriter (p :.: q) = WithWriter q :.: WithWriter p

type instance IsOb Tight (p :: STT' k i j) = IsWriter (UN ST p)
type instance IsOb Cotight (p :: STT' k i j) = (IsReader (UN ST p))
type instance CotightAdjoint (p :: STT' k i j) = ST (WithReader (UN ST p))
type instance TightAdjoint (p :: STT' k i j) = ST (WithWriter (UN ST p))
instance (SelfAction k) => WithObO2 Tight (STT' k) where withObO2 :: forall {i :: ()} {j :: ()} {k :: ()} (a :: STT' k j k)
       (b :: STT' k i j) r.
(Ob a, Ob b, IsOb Tight a, IsOb Tight b) =>
((IsOb Tight (O a b), Ob (O a b)) => r) -> r
withObO2 (IsOb Tight (O a b), Ob (O a b)) => r
r = r
(IsOb Tight (O a b), Ob (O a b)) => r
r
instance (SelfAction k) => WithObO2 Cotight (STT' k) where withObO2 :: forall {i :: ()} {j :: ()} {k :: ()} (a :: STT' k j k)
       (b :: STT' k i j) r.
(Ob a, Ob b, IsOb Cotight a, IsOb Cotight b) =>
((IsOb Cotight (O a b), Ob (O a b)) => r) -> r
withObO2 (IsOb Cotight (O a b), Ob (O a b)) => r
r = r
(IsOb Cotight (O a b), Ob (O a b)) => r
r

-- | Stateful transformers.
-- https://arxiv.org/pdf/2305.16899 definition 6
-- Generalized to any symmetric monoidal action.
instance (SelfAction k) => Equipment (STT' k) where
  withTightAdjoint :: forall {j :: ()} {k1 :: ()} (f :: STT' k j k1) r.
IsCotight f =>
((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r)
-> r
withTightAdjoint (Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r
r = r
(Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r
r
  withCotightAdjoint :: forall {j :: ()} {k1 :: ()} (f :: STT' k j k1) r.
IsTight f =>
((Adjunction_ f (CotightAdjoint f),
  IsCotight (CotightAdjoint f)) =>
 r)
-> r
withCotightAdjoint (Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) =>
r
r = r
(Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) =>
r
r

type STSq (p :: k +-> k) (q :: k +-> k) (a :: k) (b :: k) =
  ST (Writer a) `O` (ST p :: STT k) ~> (ST q :: STT k) `O` ST (Writer a)

crossing
  :: forall {k} (p :: k +-> k) (a :: k)
   . (Strong k p, Ob a, SelfAction k) => STSq p p a a
crossing :: forall {k} (p :: k +-> k) (a :: k).
(Strong k p, Ob a, SelfAction k) =>
STSq p p a a
crossing = ((Writer a :.: p) :~> (p :.: Writer a))
-> StT ('ST (Writer a :.: p)) ('ST (p :.: Writer a))
forall k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong k p, Strong k q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT \(Writer a ~> (a ** b)
g :.: p b b
p) -> (a ~> Act a b) -> p (Act a b) (Act a b) -> p a (Act 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 ~> (a ** b)
a ~> Act a b
g ((a ~> a) -> p b b -> p (Act a b) (Act a b)
forall (a :: k) (b :: k) (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 :: k). (CategoryOf k, 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 ~> (a ** b)) -> Writer a (Act a b) b
forall {k} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a (a ~> a) -> (b ~> b) -> Act a b ~> Act a b
forall (a :: k) (b :: k) (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) => (:.:) 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 :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p b b
p

pi0
  :: forall {k} (p :: STT k) (q :: STT k). (Ob p, Ob q, SelfAction k) => ST (UN ST p :*: UN ST q) ~> p
pi0 :: forall {k} (p :: STT k) (q :: STT k).
(Ob p, Ob q, SelfAction k) =>
'ST (UN 'ST p :*: UN 'ST q) ~> p
pi0 = ((UN 'ST p :*: UN 'ST q) :~> UN 'ST p)
-> StT ('ST (UN 'ST p :*: UN 'ST q)) ('ST (UN 'ST p))
forall k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong k p, Strong k q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT \(UN 'ST p a b
p :*: UN 'ST q a b
_) -> UN 'ST p a b
p

pi1
  :: forall {k} (p :: STT k) (q :: STT k). (Ob p, Ob q, SelfAction k) => ST (UN ST p :*: UN ST q) ~> q
pi1 :: forall {k} (p :: STT k) (q :: STT k).
(Ob p, Ob q, SelfAction k) =>
'ST (UN 'ST p :*: UN 'ST q) ~> q
pi1 = ((UN 'ST p :*: UN 'ST q) :~> UN 'ST q)
-> StT ('ST (UN 'ST p :*: UN 'ST q)) ('ST (UN 'ST q))
forall k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong k p, Strong k q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT \(UN 'ST p a b
_ :*: UN 'ST q a b
q) -> UN 'ST q a b
q

mult
  :: forall {k} (p :: STT k) q r (a :: k) b
   . (Ob p, Ob q, Ob r, SelfAction k, Ob a, Ob b)
  => p ~> q -> p ~> r -> p ~> ST (UN ST q :*: UN ST r)
StT p :~> q
n mult :: forall {k} {k} (p :: STT k) (q :: STT k) (r :: STT k) (a :: k)
       (b :: k).
(Ob p, Ob q, Ob r, SelfAction k, Ob a, Ob b) =>
(p ~> q) -> (p ~> r) -> p ~> 'ST (UN 'ST q :*: UN 'ST r)
`mult` StT p :~> q
m = (p :~> (UN 'ST q :*: UN 'ST r))
-> StT ('ST p) ('ST (UN 'ST q :*: UN 'ST r))
forall k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong k p, Strong k q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT \p a b
p -> p a b -> q a b
p :~> q
n p a b
p q a b -> q a b -> (:*:) q q a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> q a b -> (:*:) p q a b
:*: p a b -> q a b
p :~> q
m p a b
p a b
p

ip0
  :: forall {k} (p :: STT k) q. (Ob p, Ob q, SelfAction k) => p ~> ST (UN ST p :+: UN ST q)
ip0 :: forall {i :: ()} {j :: ()} {k} (p :: STT k) (q :: STT' k i j).
(Ob p, Ob q, SelfAction k) =>
p ~> 'ST (UN 'ST p :+: UN 'ST q)
ip0 = (UN 'ST p :~> (UN 'ST p :+: UN 'ST q))
-> StT ('ST (UN 'ST p)) ('ST (UN 'ST p :+: UN 'ST q))
forall k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong k p, Strong k q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT \UN 'ST p a b
p -> UN 'ST p a b -> (:+:) (UN 'ST p) (UN 'ST q) a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> (:+:) p q a b
InjL UN 'ST p a b
p

ip1
  :: forall {k} (p :: STT k) q. (Ob p, Ob q, SelfAction k) => q ~> ST (UN ST p :+: UN ST q)
ip1 :: forall {i :: ()} {j :: ()} {k} (p :: STT k) (q :: STT' k i j).
(Ob p, Ob q, SelfAction k) =>
q ~> 'ST (UN 'ST p :+: UN 'ST q)
ip1 = (UN 'ST q :~> (UN 'ST p :+: UN 'ST q))
-> StT ('ST (UN 'ST q)) ('ST (UN 'ST p :+: UN 'ST q))
forall k (p :: k +-> k) (q :: k +-> k) (i :: ()) (j :: ()).
(Strong k p, Strong k q) =>
(p :~> q) -> StT ('ST p) ('ST q)
StT \UN 'ST q a b
p -> UN 'ST q a b -> (:+:) (UN 'ST p) (UN 'ST q) a b
forall {j} {k} (q :: j +-> k) (a :: k) (b :: j) (p :: j +-> k).
q a b -> (:+:) p q a b
InjR UN 'ST q a b
p

-- plus
--   :: forall {k} (p :: k +-> k) q r (a :: k) b
--    . (Strong k p, Strong k q, Strong k 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 n `plus` STSq m = STSq (coproduct n m)

-- sigma0
--   :: forall {k} (a :: k) b
--    . (Ob a, Ob b, M.SymMonoidal m, SelfAction k, HasCoproducts m) => STSq (Id :: k +-> k) Id a (a || b)
-- sigma0 = withObCoprod @m @a @b $ STSq \(Id f) -> Id (act (lft @m @a @b) f)

-- sigma1
--   :: forall {k} (a :: k) b
--    . (Ob a, Ob b, M.SymMonoidal m, SelfAction k, HasCoproducts m) => STSq (Id :: k +-> k) Id b (a || b)
-- sigma1 = withObCoprod @m @a @b $ STSq \(Id f) -> Id (act (rgt @m @a @b) 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 n `copair` STSq m =
--   withObCoprod @k @a @b $
--     STSq
--       ( \(p :: p x y) ->
--           dimap ((toSelfAct @a @x +++ toSelfAct @b @x) . distR @k @a @b @x) (withObAct @k @k @c @y codiag) ((n p `copar` m p))
--             \\ p
--       )