module Proarrow.Promonad.Reader where import Proarrow.Adjunction (Adjunction (..)) 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.Category.Opposite (OPPOSITE (..), Op (..)) 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 (..)) import Proarrow.Promonad.Writer (Writer (..)) data Reader r a b where Reader :: (Ob a, Ob b) => 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, Ob b) => (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 (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, Ob b) => (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, Ob b) => (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, Ob b) => (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, Ob b) => (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, Ob b) => (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, Ob b) => (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 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 ** y1) ~> (x2 ** y2)) -> Reader ('OP r) (x1 ** y1) (x2 ** y2) forall {k} {m} (a :: k) (b :: k) (r :: m). (Ob a, Ob b) => (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 ) ((Ob (x1 ** y1), Ob (x1 ** y1)) => Reader ('OP r) (x1 ** y1) (x2 ** y2)) -> ((x1 ** y1) ~> (x1 ** y1)) -> Reader ('OP r) (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)) => Reader ('OP r) (x1 ** y1) (x2 ** y2)) -> ((x2 ** y2) ~> (x2 ** y2)) -> Reader ('OP r) (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 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, Ob b) => (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} (a :: k) (b :: k) (w :: m). (Ob a, 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