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

module Proarrow.Category.Equipment.Stateful where

import Data.Kind (Type)
import Prelude (type (~))

import Proarrow.Adjunction (Proadjunction)
import Proarrow.Category.Bicategory (Adjunction (..), Bicategory (..), Adjunction_ (..), Adj (..))
import Proarrow.Category.Bicategory.Prof (PROFK (..), Prof (..))
import Proarrow.Category.Equipment (Cotight, CotightAdjoint, Equipment (..), IsOb, Tight, TightAdjoint, WithObO2 (..))
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), Strong (..), SymMonoidalAction)
import Proarrow.Category.Opposite (OPPOSITE (..))
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Is
  , Kind
  , Profunctor (..)
  , Promonad (..)
  , UN
  , dimapDefault
  , lmap
  , rmap
  , src
  , tgt
  , (:~>)
  , type (+->)
  )
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 m k = STT' m k '() '()

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, m ~ Type) => Bicategory (STT' m k) where
  type I = ST Id
  type a `O` b = ST (UN ST a :.: UN ST 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

instance
  (MonoidalAction m k, Adjunction (PK l) (PK r), Ob l, Ob r, Strong m r, Strong m l, m ~ Type)
  => Adjunction_ (ST l :: STT' m 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 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)
      , adjCounit :: O ('ST l) ('ST r) ~> I
adjCounit = ((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)
      }

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

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

type instance IsOb Tight (p :: STT' m k i j) = IsWriter m (UN ST p)
type instance IsOb Cotight (p :: STT' m k i j) = (IsReader m (UN ST p))
type instance CotightAdjoint (p :: STT' m k i j) = ST (WithReader m (UN ST p))
type instance TightAdjoint (p :: STT' m k i j) = ST (WithWriter m (UN ST p))
instance (MonoidalAction m k, m ~ Type) => WithObO2 Tight (STT' m k) where withObO2 :: forall {i :: ()} {j :: ()} {k :: ()} (a :: STT' m k j k)
       (b :: STT' m 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 (MonoidalAction m k, m ~ Type) => WithObO2 Cotight (STT' m k) where withObO2 :: forall {i :: ()} {j :: ()} {k :: ()} (a :: STT' m k j k)
       (b :: STT' m 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 (SymMonoidalAction m k, m ~ Type) => Equipment (STT' m k) where
  withTightAdjoint :: forall {j :: ()} {k1 :: ()} (f :: STT' m 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' m 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 :: m) (b :: m) = ST (Writer a) `O` (ST p :: STT m k) ~> (ST q :: STT m k) `O` ST (Writer a)

-- crossing
--   :: forall {k} {m} (p :: k +-> k) (a :: m)
--    . (Strong m p, Ob a, SymMonoidalAction m k) => STSq p p a a
-- crossing = StT \(Writer g :.: p) -> lmap g (act (obj @a) p) :.: Writer (obj @a `act` tgt p) \\ p

-- pi0
--   :: forall {m} {k} (p :: STT m k) (q :: STT m k). (Ob p, Ob q, SymMonoidalAction m k) => ST (UN ST p :*: UN ST q) ~> p
-- pi0 = StT \(p :*: _) -> p

-- pi1
--   :: forall {m} {k} (p :: STT m k) (q :: STT m k). (Ob p, Ob q, SymMonoidalAction m k) => ST (UN ST p :*: UN ST q) ~> q
-- pi1 = StT \(_ :*: q) -> 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 n `mult` STSq m = STSq (\p -> n p :*: m 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 = STSq \p -> act (obj @(M.Unit :: m)) (InjL 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 = STSq \p -> act (obj @(M.Unit :: m)) (InjR 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 n `plus` STSq m = STSq (coproduct n 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 = withObCoprod @m @a @b $ STSq \(Id f) -> Id (act (lft @m @a @b) 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 = 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
--       )