module Proarrow.Promonad.Reader where

import Prelude (($))

import Proarrow.Adjunction (Adjunction (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , SymMonoidal (..)
  , first
  , second
  , swap'
  , unitObj
  )
import Proarrow.Category.Monoidal.Action (MonoidalAction (..), SelfAction, Strong (..), strongPar0)
import Proarrow.Category.Monoidal.Distributive (Cotraversable (..))
import Proarrow.Category.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj, rmap, src, (//), type (+->))
import Proarrow.Functor (Functor (..))
import Proarrow.Monoid (Comonoid (..), Monoid (..), comultAct, counitAct, mappendAct, memptyAct)
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Promonad (Procomonad (..))
import Proarrow.Promonad.Writer (Writer (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))

data Reader r a b where
  Reader :: forall a b r. (Ob a) => Act r a ~> b -> Reader (OP r) a b

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

instance (Ob (r :: m), MonoidalAction m k) => Corepresentable (Reader (OP r) :: k +-> k) where
  type Reader (OP r) %% a = Act r a
  coindex :: forall (a :: k) (b :: k).
Reader ('OP r) a b -> (Reader ('OP r) %% a) ~> b
coindex (Reader Act r a ~> b
f) = Act r a ~> b
(Reader ('OP r) %% a) ~> b
f
  cotabulate :: forall (a :: k) (b :: k).
Ob a =>
((Reader ('OP r) %% a) ~> b) -> Reader ('OP r) a b
cotabulate (Reader ('OP r) %% a) ~> b
f = (Act r a ~> b) -> Reader ('OP r) a b
forall {k} {m} (a :: k) (b :: k) (r :: m).
Ob a =>
(Act r a ~> b) -> Reader ('OP r) a b
Reader Act r a ~> b
(Reader ('OP r) %% a) ~> b
f
  corepMap :: forall (a :: k) (b :: k).
(a ~> b) -> (Reader ('OP r) %% a) ~> (Reader ('OP r) %% b)
corepMap a ~> b
f = (r ~> r) -> (a ~> b) -> Act r a ~> Act r 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 :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @r) a ~> b
f

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

instance (Comonoid (r :: m), MonoidalAction m k) => Promonad (Reader (OP r) :: k +-> k) where
  id :: forall (a :: k). Ob a => Reader ('OP r) a a
id = (Act r a ~> a) -> Reader ('OP r) a a
forall {k} {m} (a :: k) (b :: k) (r :: m).
Ob a =>
(Act r a ~> b) -> Reader ('OP r) a b
Reader (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 @r)
  Reader Act r b ~> c
g . :: forall (b :: k) (c :: k) (a :: k).
Reader ('OP r) b c -> Reader ('OP r) a b -> Reader ('OP r) a c
. Reader @a Act r a ~> b
f = (Act r a ~> c) -> Reader ('OP r) a c
forall {k} {m} (a :: k) (b :: k) (r :: m).
Ob a =>
(Act r a ~> b) -> Reader ('OP r) a b
Reader (Act r b ~> c
Act r b ~> c
g (Act r b ~> c) -> (Act r a ~> Act r b) -> Act r a ~> 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
. (r ~> r) -> (Act r a ~> b) -> Act r (Act r a) ~> Act r 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 :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @r) Act r a ~> b
Act r a ~> b
f (Act r (Act r a) ~> Act r b)
-> (Act r a ~> Act r (Act r a)) -> Act r a ~> Act r 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
. 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 @r @a)

instance (Monoid (r :: m), MonoidalAction m k) => Procomonad (Reader (OP r) :: k +-> k) where
  extract :: Reader ('OP r) :~> (~>)
extract (Reader Act r a ~> b
f) = Act r a ~> b
Act r a ~> b
f (Act r a ~> b) -> (a ~> Act r a) -> 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
. 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 @r
  duplicate :: Reader ('OP r) :~> (Reader ('OP r) :.: Reader ('OP r))
duplicate (Reader @a Act r a ~> b
f) = (Act r a ~> Act r a) -> Reader ('OP r) a (Act r a)
forall {k} {m} (a :: k) (b :: k) (r :: m).
Ob a =>
(Act r a ~> b) -> Reader ('OP r) a b
Reader Act r a ~> Act r a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id Reader ('OP r) a (Act r a)
-> Reader ('OP r) (Act r a) b
-> (:.:) (Reader ('OP r)) (Reader ('OP r)) 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 r (Act r a) ~> b) -> Reader ('OP r) (Act r a) b
forall {k} {m} (a :: k) (b :: k) (r :: m).
Ob a =>
(Act r a ~> b) -> Reader ('OP r) a b
Reader (Act r a ~> b
Act r a ~> b
f (Act r a ~> b)
-> (Act r (Act r a) ~> Act r a) -> Act r (Act r 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
. 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 @r @a) ((Ob (Act r a), Ob b) =>
 (:.:) (Reader ('OP r)) (Reader ('OP r)) a b)
-> (Act r a ~> b) -> (:.:) (Reader ('OP r)) (Reader ('OP r)) a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ Act r a ~> b
Act r a ~> b
f

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

-- | Note: This is only premonoidal, not monoidal, unless the comonoid is cocommutative.
instance (Comonoid (r :: k), SelfAction k, SymMonoidal k) => MonoidalProfunctor (Reader (OP r) :: k +-> k) where
  par0 :: Reader ('OP r) Unit Unit
par0 = Reader ('OP r) Unit Unit
(Ob Unit, Ob Unit) => Reader ('OP r) Unit Unit
forall (a :: k). Ob a => Reader ('OP r) a a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id ((Ob Unit, Ob Unit) => Reader ('OP r) Unit Unit)
-> (Unit ~> Unit) -> Reader ('OP r) 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
  Reader @x1 @x2 Act r x1 ~> x2
f par :: forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
Reader ('OP r) x1 x2
-> Reader ('OP r) y1 y2 -> Reader ('OP r) (x1 ** y1) (x2 ** y2)
`par` Reader @y1 @y2 Act r y1 ~> y2
g =
    Act r x1 ~> x2
Act r x1 ~> x2
f (Act r x1 ~> x2)
-> ((Ob (Act r x1), Ob x2) => Reader ('OP r) (x1 ** y1) (x2 ** y2))
-> Reader ('OP r) (x1 ** y1) (x2 ** y2)
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
      Act r y1 ~> y2
Act r y1 ~> y2
g (Act r y1 ~> y2)
-> ((Ob (Act r y1), Ob y2) => Reader ('OP r) (x1 ** y1) (x2 ** y2))
-> Reader ('OP r) (x1 ** y1) (x2 ** y2)
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
        forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @x1 @y1 ((Ob (x1 ** y1) => Reader ('OP r) (x1 ** y1) (x2 ** y2))
 -> Reader ('OP r) (x1 ** y1) (x2 ** y2))
-> (Ob (x1 ** y1) => Reader ('OP r) (x1 ** y1) (x2 ** y2))
-> Reader ('OP r) (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$
          forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @x2 @y2 ((Ob (x2 ** y2) => Reader ('OP r) (x1 ** y1) (x2 ** y2))
 -> Reader ('OP r) (x1 ** y1) (x2 ** y2))
-> (Ob (x2 ** y2) => Reader ('OP r) (x1 ** y1) (x2 ** y2))
-> Reader ('OP r) (x1 ** y1) (x2 ** y2)
forall a b. (a -> b) -> a -> b
$
            (Act r (x1 ** y1) ~> (x2 ** y2))
-> Reader ('OP r) (x1 ** y1) (x2 ** y2)
forall {k} {m} (a :: k) (b :: k) (r :: m).
Ob a =>
(Act r a ~> b) -> Reader ('OP r) a b
Reader
              ( 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 @x2 Act r y1 ~> y2
Act r y1 ~> y2
g
                  ((x2 ** Act r y1) ~> (x2 ** y2))
-> (Act r (x1 ** y1) ~> (x2 ** Act r y1))
-> Act r (x1 ** y1) ~> (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))
associator @k @x2 @r @y1
                  (((x2 ** r) ** y1) ~> (x2 ** Act r y1))
-> (Act r (x1 ** y1) ~> ((x2 ** r) ** y1))
-> Act r (x1 ** y1) ~> (x2 ** Act r y1)
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
. (((r ~> r) -> (Act r x1 ~> x2) -> (r ** Act r x1) ~> (x2 ** r)
forall {k} (a :: k) (a' :: k) (b :: k) (b' :: k).
SymMonoidal k =>
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @r) Act r x1 ~> x2
Act r x1 ~> x2
f ((r ** Act r x1) ~> (x2 ** r))
-> ((r ** x1) ~> (r ** Act r x1)) -> (r ** x1) ~> (x2 ** r)
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))
associator @k @r @r @x1 (((r ** r) ** x1) ~> (r ** Act r x1))
-> ((r ** x1) ~> ((r ** r) ** x1)) -> (r ** x1) ~> (r ** Act r x1)
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 @x1 (forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @r)) ((r ** x1) ~> (x2 ** r))
-> (y1 ~> y1) -> ((r ** x1) ** y1) ~> ((x2 ** r) ** y1)
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 @y1)
                  (((r ** x1) ** y1) ~> ((x2 ** r) ** y1))
-> (Act r (x1 ** y1) ~> ((r ** x1) ** y1))
-> Act r (x1 ** y1) ~> ((x2 ** r) ** y1)
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 @r @x1 @y1
              )

instance (Comonoid (r :: k), SelfAction k) => Cotraversable (Reader (OP r) :: k +-> k) where
  cotraverse :: forall (p :: k +-> k).
(DistributiveProfunctor p, Strong k p, SelfAction k) =>
(p :.: Reader ('OP r)) :~> (Reader ('OP r) :.: p)
cotraverse (p a b
p :.: Reader Act r b ~> b
f) = let rp :: p (Act r a) (Act r b)
rp = forall (a :: k).
(SelfAction k, Strong k (~>), MonoidalProfunctor (~>), Ob a) =>
a ~> a
forall {k} {p :: CAT k} (a :: k).
(SelfAction k, Strong k p, MonoidalProfunctor p, Ob a) =>
p a a
strongPar0 @r (r ~> r) -> p a b -> p (Act r a) (Act r 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` p a b
p in (Act r a ~> Act r a) -> Reader ('OP r) a (Act r a)
forall {k} {m} (a :: k) (b :: k) (r :: m).
Ob a =>
(Act r a ~> b) -> Reader ('OP r) a b
Reader (p (Act r a) (Act r b) -> Act r a ~> Act r a
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src p (Act r a) (Act r b)
rp) Reader ('OP r) a (Act r a)
-> p (Act r a) b -> (:.:) (Reader ('OP r)) p 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 r b ~> b) -> p (Act r a) (Act r b) -> p (Act r a) b
forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap Act r b ~> b
Act r b ~> b
f p (Act r a) (Act r b)
rp ((Ob (Act r a), Ob (Act r b)) => (:.:) (Reader ('OP r)) p a b)
-> p (Act r a) (Act r b) -> (:.:) (Reader ('OP r)) p a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p (Act r a) (Act r b)
rp ((Ob a, Ob b) => (:.:) (Reader ('OP r)) p a b)
-> p a b -> (:.:) (Reader ('OP r)) p a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

instance (Ob (r :: m), MonoidalAction m k) => Adjunction (Writer r :: k +-> k) (Reader (OP r)) where
  unit :: forall (a :: k). Ob a => (:.:) (Reader ('OP r)) (Writer r) a a
unit @a = (Act r a ~> Act r a) -> Reader ('OP r) a (Act r a)
forall {k} {m} (a :: k) (b :: k) (r :: m).
Ob a =>
(Act r a ~> b) -> Reader ('OP r) a b
Reader Act r a ~> Act r a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id Reader ('OP r) a (Act r a)
-> Writer r (Act r a) a -> (:.:) (Reader ('OP r)) (Writer r) a a
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 r a ~> Act r a) -> Writer r (Act r a) a
forall {k} {m} (b :: k) (a :: k) (w :: m).
Ob b =>
(a ~> Act w b) -> Writer w a b
Writer Act r a ~> Act r a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id ((Ob (Act r a), Ob (Act r a)) =>
 (:.:) (Reader ('OP r)) (Writer r) a a)
-> (Act r a ~> Act r a) -> (:.:) (Reader ('OP r)) (Writer r) a a
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
\\ (r ~> r) -> (a ~> a) -> Act r a ~> Act r a
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 @r) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a)
  counit :: (Writer r :.: Reader ('OP r)) :~> (~>)
counit (Writer a ~> Act r b
f :.: Reader Act r b ~> b
g) = Act r b ~> b
Act r b ~> b
g (Act r b ~> b) -> (a ~> Act r 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 r b
f