{-# LANGUAGE TupleSections #-}

module Proarrow.Promonad.Writer where

import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , SymMonoidal (..)
  , first
  , obj2
  , second
  , swap'
  , unitObj
  )
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), SelfAction, Strong (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj, (//), type (+->))
import Proarrow.Functor (Functor (..))
import Proarrow.Monoid (Comonoid, Monoid (..), comultAct, counitAct, mappendAct, memptyAct)
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Promonad (Procomonad (..))

data Writer w a b where
  Writer :: (Ob a, Ob b) => a ~> Act w b -> Writer w a b

instance (Ob (w :: m), MonoidalAction m k) => Profunctor (Writer w :: k +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> Writer w a b -> Writer w c d
dimap c ~> a
l b ~> d
r (Writer a ~> Act w b
f) = (c ~> Act w d) -> Writer w c d
forall {k} {m} (a :: k) (b :: k) (w :: m).
(Ob a, Ob b) =>
(a ~> Act w b) -> Writer w a b
Writer ((w ~> w) -> (b ~> d) -> Act w b ~> Act w d
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 :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @w) b ~> d
r (Act w b ~> Act w d) -> (c ~> Act w b) -> c ~> Act w d
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 w b
f (a ~> Act w b) -> (c ~> a) -> c ~> Act w 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
. c ~> a
l) ((Ob b, Ob d) => Writer w c d) -> (b ~> d) -> Writer w c d
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
\\ b ~> d
r ((Ob c, Ob a) => Writer w c d) -> (c ~> a) -> Writer w c d
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
\\ c ~> a
l
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: k) r.
((Ob a, Ob b) => r) -> Writer w a b -> r
\\ Writer a ~> Act w b
f = r
(Ob a, Ob b) => r
(Ob a, Ob (Act w b)) => r
r ((Ob a, Ob (Act w b)) => r) -> (a ~> Act w b) -> r
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 w b
f

instance (MonoidalAction m k) => Functor (Writer :: m -> k +-> k) where
  map :: forall (a :: m) (b :: m). (a ~> b) -> Writer a ~> Writer b
map a ~> b
f = a ~> b
f (a ~> b)
-> ((Ob a, Ob b) => Prof (Writer a) (Writer b))
-> Prof (Writer a) (Writer b)
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (Writer a :~> Writer b) -> Prof (Writer a) (Writer b)
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Writer @_ @b a ~> Act a b
g) -> (a ~> Act b b) -> Writer b a b
forall {k} {m} (a :: k) (b :: k) (w :: m).
(Ob a, Ob b) =>
(a ~> Act w b) -> Writer w a b
Writer ((a ~> b) -> (b ~> b) -> Act a 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 a ~> b
f (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b) (Act a b ~> Act b b) -> (a ~> Act a b) -> a ~> Act b 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 a b
g)

instance (Monoid (w :: m), MonoidalAction m k) => Promonad (Writer w :: k +-> k) where
  id :: forall (a :: k). Ob a => Writer w a a
id = (a ~> Act w a) -> Writer w a a
forall {k} {m} (a :: k) (b :: k) (w :: m).
(Ob a, Ob b) =>
(a ~> Act w b) -> Writer w a b
Writer (forall (a :: m) (n :: k).
(MonoidalAction m k, Monoid a, Ob n) =>
n ~> Act a n
forall {m} {c} (a :: m) (n :: c).
(MonoidalAction m c, Monoid a, Ob n) =>
n ~> Act a n
memptyAct @w)
  Writer @_ @c b ~> Act w c
g . :: forall (b :: k) (c :: k) (a :: k).
Writer w b c -> Writer w a b -> Writer w a c
. Writer a ~> Act w b
f = (a ~> Act w c) -> Writer w a c
forall {k} {m} (a :: k) (b :: k) (w :: m).
(Ob a, Ob b) =>
(a ~> Act w b) -> Writer w a b
Writer (forall (a :: m) (n :: k).
(MonoidalAction m k, Monoid a, Ob n) =>
Act a (Act a n) ~> Act a n
forall {m} {c} (a :: m) (n :: c).
(MonoidalAction m c, Monoid a, Ob n) =>
Act a (Act a n) ~> Act a n
mappendAct @w @c (Act w (Act w c) ~> Act w c)
-> (a ~> Act w (Act w c)) -> a ~> Act w c
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
. (w ~> w) -> (b ~> Act w c) -> Act w b ~> Act w (Act w c)
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 :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @w) b ~> Act w c
g (Act w b ~> Act w (Act w c))
-> (a ~> Act w b) -> a ~> Act w (Act w c)
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 w b
f)

instance (Comonoid (w :: m), MonoidalAction m k) => Procomonad (Writer w :: k +-> k) where
  extract :: Writer w :~> (~>)
extract (Writer a ~> Act w b
f) = forall (a :: m) (n :: k).
(MonoidalAction m k, Comonoid a, Ob n) =>
Act a n ~> n
forall {m} {c} (a :: m) (n :: c).
(MonoidalAction m c, Comonoid a, Ob n) =>
Act a n ~> n
counitAct @w (Act w b ~> b) -> (a ~> Act w 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 w b
f
  duplicate :: Writer w :~> (Writer w :.: Writer w)
duplicate (Writer @_ @b a ~> Act w b
f) = (a ~> Act w (Act w b)) -> Writer w a (Act w b)
forall {k} {m} (a :: k) (b :: k) (w :: m).
(Ob a, Ob b) =>
(a ~> Act w b) -> Writer w a b
Writer (forall (a :: m) (n :: k).
(MonoidalAction m k, Comonoid a, Ob n) =>
Act a n ~> Act a (Act a n)
forall {m} {c} (a :: m) (n :: c).
(MonoidalAction m c, Comonoid a, Ob n) =>
Act a n ~> Act a (Act a n)
comultAct @w @b (Act w b ~> Act w (Act w b))
-> (a ~> Act w b) -> a ~> Act w (Act w 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 w b
f) Writer w a (Act w b)
-> Writer w (Act w b) b -> (:.:) (Writer w) (Writer w) 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 w b ~> Act w b) -> Writer w (Act w 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 w b ~> Act w 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 w b)) => (:.:) (Writer w) (Writer w) a b)
-> (a ~> Act w b) -> (:.:) (Writer w) (Writer w) 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 w b
f

instance (Ob (w :: m), MonoidalAction m k, SymMonoidal m) => Strong m (Writer w :: k +-> k) where
  act :: forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> Writer w x y -> Writer w (Act a x) (Act b y)
act @a @b @x @y a ~> b
f (Writer x ~> Act w y
g) =
    (Act a x ~> Act w (Act b y)) -> Writer w (Act a x) (Act b y)
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 @w @b @y (Act (w ** b) y ~> Act w (Act b y))
-> (Act a x ~> Act (w ** b) y) -> Act a x ~> Act w (Act b y)
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
. ((b ** w) ~> (w ** b))
-> (y ~> y) -> Act (b ** w) y ~> Act (w ** 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).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @b @w) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @y) (Act (b ** w) y ~> Act (w ** b) y)
-> (Act a x ~> Act (b ** w) y) -> Act a x ~> Act (w ** b) y
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
. 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 @b @w @y (Act b (Act w y) ~> Act (b ** w) y)
-> (Act a x ~> Act b (Act w y)) -> Act a x ~> Act (b ** w) y
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) -> (x ~> Act w y) -> Act a x ~> Act b (Act w 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 a ~> b
f x ~> Act w y
g)
      ((Ob (Act a x), Ob (Act a x)) => Writer w (Act a x) (Act b y))
-> (Act a x ~> Act a x) -> Writer w (Act a x) (Act b y)
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 ~> 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 (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x)
      ((Ob (Act b y), Ob (Act b y)) => Writer w (Act a x) (Act b y))
-> (Act b y ~> Act b y) -> Writer w (Act a x) (Act b y)
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
\\ (b ~> b) -> (y ~> y) -> Act b y ~> Act 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 (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @y)
      ((Ob a, Ob b) => Writer w (Act a x) (Act b y))
-> (a ~> b) -> Writer w (Act a x) (Act b y)
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
\\ a ~> b
f

instance (Monoid (w :: k), SelfAction k, SymMonoidal k) => MonoidalProfunctor (Writer w :: k +-> k) where
  par0 :: Writer w Unit Unit
par0 = Writer w Unit Unit
(Ob Unit, Ob Unit) => Writer w Unit Unit
forall (a :: k). Ob a => Writer w a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id ((Ob Unit, Ob Unit) => Writer w Unit Unit)
-> (Unit ~> Unit) -> Writer w Unit Unit
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 k. Monoidal k => Obj Unit
unitObj @k
  Writer @x1 @x2 x1 ~> Act w x2
f par :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
Writer w x1 x2 -> Writer w y1 y2 -> Writer w (x1 ** y1) (x2 ** y2)
`par` Writer @y1 @y2 y1 ~> Act w y2
g =
    ((x1 ** y1) ~> Act w (x2 ** y2)) -> Writer w (x1 ** y1) (x2 ** y2)
forall {k} {m} (a :: k) (b :: k) (w :: m).
(Ob a, Ob b) =>
(a ~> Act w b) -> Writer w a b
Writer
      ( forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @w @x2 @y2
          (((w ** x2) ** y2) ~> Act w (x2 ** y2))
-> ((x1 ** y1) ~> ((w ** x2) ** y2))
-> (x1 ** y1) ~> Act w (x2 ** y2)
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
. ((forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (a ** c) ~> (b ** c)
first @x2 (forall (m :: k). Monoid m => (m ** m) ~> m
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend @w) (((w ** w) ** x2) ~> (w ** x2))
-> ((x1 ** w) ~> ((w ** w) ** x2)) -> (x1 ** w) ~> (w ** x2)
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
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @w @w @x2 ((w ** (w ** x2)) ~> ((w ** w) ** x2))
-> ((x1 ** w) ~> (w ** (w ** x2))) -> (x1 ** w) ~> ((w ** w) ** x2)
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
. (x1 ~> Act w x2) -> (w ~> w) -> (x1 ** w) ~> (w ** Act w x2)
forall {k} (a :: k) (a' :: k) (b :: k) (b' :: k).
SymMonoidal k =>
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' x1 ~> Act w x2
f (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @w)) ((x1 ** w) ~> (w ** x2))
-> (y2 ~> y2) -> ((x1 ** w) ** y2) ~> ((w ** x2) ** y2)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
`par` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @y2)
          (((x1 ** w) ** y2) ~> ((w ** x2) ** y2))
-> ((x1 ** y1) ~> ((x1 ** w) ** y2))
-> (x1 ** y1) ~> ((w ** x2) ** y2)
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
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @x1 @w @y2
          ((x1 ** (w ** y2)) ~> ((x1 ** w) ** y2))
-> ((x1 ** y1) ~> (x1 ** (w ** y2)))
-> (x1 ** y1) ~> ((x1 ** w) ** y2)
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
. forall (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
forall {k} (c :: k) (a :: k) (b :: k).
(Monoidal k, Ob c) =>
(a ~> b) -> (c ** a) ~> (c ** b)
second @x1 y1 ~> Act w y2
g
      )
      ((Ob (x1 ** y1), Ob (x1 ** y1)) => Writer w (x1 ** y1) (x2 ** y2))
-> ((x1 ** y1) ~> (x1 ** y1)) -> Writer w (x1 ** y1) (x2 ** y2)
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 :: k) (b :: k). (Monoidal k, Ob a, Ob b) => Obj (a ** b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
obj2 @x1 @y1
      ((Ob (x2 ** y2), Ob (x2 ** y2)) => Writer w (x1 ** y1) (x2 ** y2))
-> ((x2 ** y2) ~> (x2 ** y2)) -> Writer w (x1 ** y1) (x2 ** y2)
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 :: k) (b :: k). (Monoidal k, Ob a, Ob b) => Obj (a ** b)
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a, Ob b) =>
Obj (a ** b)
obj2 @x2 @y2