module Proarrow.Promonad.Reader where

import Prelude (($))

import Proarrow.Adjunction qualified as Adj
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , MonoidalProfunctor (..)
  , SymMonoidal (..)
  , first
  , leftUnitorInvWith
  , leftUnitorWith
  , second
  , swap'
  , swapInner
  , 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 (..))
import Proarrow.Object.BinaryProduct (Cartesian)
import Proarrow.Object.Exponential (Closed (..), uncurry)
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Profunctor.Day (Day (..))
import Proarrow.Profunctor.Identity (Id (..))
import Proarrow.Profunctor.Representable (Representable (..))
import Proarrow.Promonad (Procomonad (..))
import Proarrow.Promonad.Writer (Writer (..))

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

instance (Ob (r :: k), Monoidal 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 (r ** a) ~> b
f) = ((r ** c) ~> d) -> Reader ('OP r) c d
forall {k} (a :: k) (b :: k) (r :: k).
Ob a =>
((r ** a) ~> b) -> Reader ('OP r) a b
Reader (b ~> d
r (b ~> d) -> ((r ** c) ~> b) -> (r ** c) ~> d
forall (b :: k) (c :: k) (a :: k). (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
. (r ** a) ~> b
(r ** a) ~> b
f ((r ** a) ~> b) -> ((r ** c) ~> (r ** a)) -> (r ** c) ~> b
forall (b :: k) (c :: k) (a :: k). (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
. 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 @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 :: j +-> k) (a :: k) (b :: j) 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 :: j +-> k) (a :: k) (b :: j) 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 (r ** a) ~> b
f = r
(Ob a, Ob b) => r
(Ob (r ** a), Ob b) => r
r ((Ob (r ** a), Ob b) => r) -> ((r ** a) ~> b) -> r
forall (a :: k) (b :: k) 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
\\ (r ** a) ~> b
(r ** a) ~> b
f

-- | The coreader comonad given the Promonad instance.
-- Together with the 'Representable' instance this gives the curry/uncurry adjunction.
instance (Ob (r :: k), Monoidal k) => Corepresentable (Reader (OP r) :: k +-> k) where
  type Reader (OP r) %% a = r ** a
  coindex :: forall (a :: k) (b :: k).
Reader ('OP r) a b -> (Reader ('OP r) %% a) ~> b
coindex (Reader (r ** a) ~> b
f) = (Reader ('OP r) %% a) ~> b
(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 = ((r ** a) ~> b) -> Reader ('OP r) a b
forall {k} (a :: k) (b :: k) (r :: k).
Ob a =>
((r ** a) ~> b) -> Reader ('OP r) a b
Reader (Reader ('OP r) %% a) ~> b
(r ** a) ~> b
f
  corepMap :: forall (a :: k) (b :: k).
(a ~> b) -> (Reader ('OP r) %% a) ~> (Reader ('OP r) %% b)
corepMap a ~> b
f = 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 @r a ~> b
f

-- | The reader monad given the Promonad instance.
instance (Ob (r :: k), SymMonoidal k, Closed k) => Representable (Reader (OP r) :: k +-> k) where
  type Reader (OP r) % a = r ~~> a
  index :: forall (a :: k) (b :: k).
Reader ('OP r) a b -> a ~> (Reader ('OP r) % b)
index (Reader @a @b (r ** a) ~> b
f) = forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @_ @a @r @b ((r ** a) ~> b
(r ** a) ~> b
f ((r ** a) ~> b) -> ((a ** r) ~> (r ** a)) -> (a ** r) ~> b
forall (b :: k) (c :: k) (a :: k). (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
. forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @a @r)
  tabulate :: forall (b :: k) (a :: k).
Ob b =>
(a ~> (Reader ('OP r) % b)) -> Reader ('OP r) a b
tabulate @b @a a ~> (Reader ('OP r) % b)
f = ((r ** a) ~> b) -> Reader ('OP r) a b
forall {k} (a :: k) (b :: k) (r :: k).
Ob a =>
((r ** a) ~> b) -> Reader ('OP r) a b
Reader (forall (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
forall {k} (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry @r @b a ~> (Reader ('OP r) % b)
a ~> (r ~~> b)
f ((a ** r) ~> b) -> ((r ** a) ~> (a ** r)) -> (r ** a) ~> b
forall (b :: k) (c :: k) (a :: k). (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
. forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @r @a) ((Ob a, Ob (r ~~> b)) => Reader ('OP r) a b)
-> (a ~> (r ~~> b)) -> Reader ('OP r) a b
forall (a :: k) (b :: k) 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
\\ a ~> (Reader ('OP r) % b)
a ~> (r ~~> b)
f
  repMap :: forall (a :: k) (b :: k).
(a ~> b) -> (Reader ('OP r) % a) ~> (Reader ('OP r) % b)
repMap a ~> b
f = a ~> b
f (a ~> b) -> (r ~> r) -> (r ~~> a) ~> (r ~~> b)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @r

instance (Monoidal k) => Functor (Reader :: OPPOSITE k -> k +-> k) where
  map :: forall (a :: OPPOSITE k) (b :: OPPOSITE k).
(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 :: k1 +-> k2) (a :: k2) (b :: k1) 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 {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Reader @a (r ** a) ~> b
g) -> ((b1 ** a) ~> b) -> Reader ('OP b1) a b
forall {k} (a :: k) (b :: k) (r :: k).
Ob a =>
((r ** a) ~> b) -> Reader ('OP r) a b
Reader ((a1 ** a) ~> b
(r ** a) ~> b
g ((a1 ** a) ~> b) -> ((b1 ** a) ~> (a1 ** a)) -> (b1 ** a) ~> b
forall (b :: k) (c :: k) (a :: k). (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
. 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 @a b1 ~> a1
f)

instance (Comonoid (r :: k), Monoidal k) => Promonad (Reader (OP r) :: k +-> k) where
  id :: forall (a :: k). Ob a => Reader ('OP r) a a
id = ((r ** a) ~> a) -> Reader ('OP r) a a
forall {k} (a :: k) (b :: k) (r :: k).
Ob a =>
((r ** a) ~> b) -> Reader ('OP r) a b
Reader ((r ~> Unit) -> (r ** a) ~> a
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (b ** a) ~> a
leftUnitorWith (forall (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit @r))
  Reader (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 (r ** a) ~> b
f = ((r ** a) ~> c) -> Reader ('OP r) a c
forall {k} (a :: k) (b :: k) (r :: k).
Ob a =>
((r ** a) ~> b) -> Reader ('OP r) a b
Reader ((r ** b) ~> c
(r ** b) ~> c
g ((r ** b) ~> c) -> ((r ** a) ~> (r ** b)) -> (r ** a) ~> c
forall (b :: k) (c :: k) (a :: k). (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
. 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 @r (r ** a) ~> b
(r ** a) ~> b
f ((r ** (r ** a)) ~> (r ** b))
-> ((r ** a) ~> (r ** (r ** a))) -> (r ** a) ~> (r ** b)
forall (b :: k) (c :: k) (a :: k). (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
. 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 @a (((r ** r) ** a) ~> (r ** (r ** a)))
-> ((r ** a) ~> ((r ** r) ** a)) -> (r ** a) ~> (r ** (r ** a))
forall (b :: k) (c :: k) (a :: k). (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
. 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 @a (forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @r))

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

instance (Ob (r :: k), SelfAction k) => Strong k (Reader (OP r) :: k +-> k) where
  act :: forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> b)
-> Reader ('OP r) x y -> Reader ('OP r) (Act a x) (Act b y)
act @a @_ @x @_ a ~> b
f (Reader (r ** x) ~> y
g) =
    a ~> b
f (a ~> b)
-> ((Ob a, Ob b) => Reader ('OP r) (Act a x) (Act b y))
-> Reader ('OP r) (Act a x) (Act b y)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
      forall m k (a :: m) (x :: k) r.
(MonoidalAction m k, Ob a, Ob x) =>
(Ob (Act a x) => r) -> r
withObAct @k @k @a @x ((Ob (Act a x) => Reader ('OP r) (Act a x) (Act b y))
 -> Reader ('OP r) (Act a x) (Act b y))
-> (Ob (Act a x) => Reader ('OP r) (Act a x) (Act b y))
-> Reader ('OP r) (Act a x) (Act b y)
forall a b. (a -> b) -> a -> b
$
        ((r ** Act a x) ~> Act b y) -> Reader ('OP r) (Act a x) (Act b y)
forall {k} (a :: k) (b :: k) (r :: k).
Ob a =>
((r ** a) ~> b) -> Reader ('OP r) a b
Reader ((a ~> b
f (a ~> b) -> ((r ** x) ~> y) -> (a ** (r ** x)) ~> (b ** y)
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` (r ** x) ~> y
(r ** x) ~> y
g) ((a ** (r ** x)) ~> Act b y)
-> ((r ** Act a x) ~> (a ** (r ** x))) -> (r ** Act a x) ~> Act b y
forall (b :: k) (c :: k) (a :: k). (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
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @a @r @x (((a ** r) ** x) ~> (a ** (r ** x)))
-> ((r ** Act a x) ~> ((a ** r) ** x))
-> (r ** Act a x) ~> (a ** (r ** x))
forall (b :: k) (c :: k) (a :: k). (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
. 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 @x (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @_ @r @a) (((r ** a) ** x) ~> ((a ** r) ** x))
-> ((r ** Act a x) ~> ((r ** a) ** x))
-> (r ** Act a x) ~> ((a ** r) ** x)
forall (b :: k) (c :: k) (a :: k). (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
. 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 @a @x)

-- | 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 :: 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 :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall k. Monoidal k => Obj Unit
unitObj @k
  Reader @x1 @x2 (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 (r ** y1) ~> y2
g =
    (r ** x1) ~> x2
(r ** x1) ~> x2
f ((r ** x1) ~> x2)
-> ((Ob (r ** x1), Ob x2) => Reader ('OP r) (x1 ** y1) (x2 ** y2))
-> Reader ('OP r) (x1 ** y1) (x2 ** y2)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
//
      (r ** y1) ~> y2
(r ** y1) ~> y2
g ((r ** y1) ~> y2)
-> ((Ob (r ** y1), Ob y2) => Reader ('OP r) (x1 ** y1) (x2 ** y2))
-> Reader ('OP r) (x1 ** y1) (x2 ** y2)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) 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
$
            ((r ** (x1 ** y1)) ~> (x2 ** y2))
-> Reader ('OP r) (x1 ** y1) (x2 ** y2)
forall {k} (a :: k) (b :: k) (r :: k).
Ob a =>
((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 (r ** y1) ~> y2
(r ** y1) ~> y2
g
                  ((x2 ** (r ** y1)) ~> (x2 ** y2))
-> ((r ** (x1 ** y1)) ~> (x2 ** (r ** y1)))
-> (r ** (x1 ** y1)) ~> (x2 ** y2)
forall (b :: k) (c :: k) (a :: k). (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
. 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 ** (r ** y1)))
-> ((r ** (x1 ** y1)) ~> ((x2 ** r) ** y1))
-> (r ** (x1 ** y1)) ~> (x2 ** (r ** y1))
forall (b :: k) (c :: k) (a :: k). (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
. (((r ~> r) -> ((r ** x1) ~> x2) -> (r ** (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) (r ** x1) ~> x2
(r ** x1) ~> x2
f ((r ** (r ** x1)) ~> (x2 ** r))
-> ((r ** x1) ~> (r ** (r ** x1))) -> (r ** x1) ~> (x2 ** r)
forall (b :: k) (c :: k) (a :: k). (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
. 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 ** (r ** x1)))
-> ((r ** x1) ~> ((r ** r) ** x1)) -> (r ** x1) ~> (r ** (r ** x1))
forall (b :: k) (c :: k) (a :: k). (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
. 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))
-> ((r ** (x1 ** y1)) ~> ((r ** x1) ** y1))
-> (r ** (x1 ** y1)) ~> ((x2 ** r) ** y1)
forall (b :: k) (c :: k) (a :: k). (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
. 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 (r ** b) ~> b
f) = let rp :: p (Act r a) (Act r b)
rp = Id r r -> r ~> r
forall k (a :: k) (b :: k). Id a b -> a ~> b
unId (forall (a :: k).
(SelfAction k, Strong k Id, MonoidalProfunctor Id, Ob a) =>
Id 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 ((r ** a) ~> (r ** a)) -> Reader ('OP r) a (r ** a)
forall {k} (a :: k) (b :: k) (r :: k).
Ob a =>
((r ** a) ~> b) -> Reader ('OP r) a b
Reader (p (r ** a) (Act r b) -> (r ** a) ~> (r ** a)
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
Profunctor p =>
p a b -> Obj a
src p (r ** a) (Act r b)
p (Act r a) (Act r b)
rp) Reader ('OP r) a (r ** a)
-> p (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
:.: ((r ** b) ~> b) -> p (r ** a) (r ** b) -> p (r ** 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 (r ** b) ~> b
(r ** b) ~> b
f p (r ** a) (r ** b)
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 :: j +-> k) (a :: k) (b :: j) 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 :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

instance (Ob (r :: k), Monoidal k) => Adj.Proadjunction (Writer r :: k +-> k) (Reader (OP r)) where
  unit :: forall (a :: k). Ob a => (:.:) (Reader ('OP r)) (Writer r) a a
unit @a = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @r @a ((Ob (r ** a) => (:.:) (Reader ('OP r)) (Writer r) a a)
 -> (:.:) (Reader ('OP r)) (Writer r) a a)
-> (Ob (r ** a) => (:.:) (Reader ('OP r)) (Writer r) a a)
-> (:.:) (Reader ('OP r)) (Writer r) a a
forall a b. (a -> b) -> a -> b
$ ((r ** a) ~> (r ** a)) -> Reader ('OP r) a (r ** a)
forall {k} (a :: k) (b :: k) (r :: k).
Ob a =>
((r ** a) ~> b) -> Reader ('OP r) a b
Reader (r ** a) ~> (r ** a)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id Reader ('OP r) a (r ** a)
-> Writer r (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
:.: ((r ** a) ~> (r ** a)) -> Writer r (r ** a) a
forall {k} (b :: k) (a :: k) (w :: k).
Ob b =>
(a ~> (w ** b)) -> Writer w a b
Writer (r ** a) ~> (r ** a)
forall (a :: k). Ob a => a ~> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  counit :: (Writer r :.: Reader ('OP r)) :~> (~>)
counit (Writer a ~> (r ** b)
f :.: Reader (r ** b) ~> b
g) = (r ** b) ~> b
(r ** b) ~> b
g ((r ** b) ~> b) -> (a ~> (r ** b)) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (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
. a ~> (r ** b)
f

dayCounit :: forall {k} (r :: k). (Ob r, Cartesian k) => Writer r `Day` Reader (OP r) ~> (~>)
dayCounit :: forall {k} (r :: k).
(Ob r, Cartesian k) =>
Day (Writer r) (Reader ('OP r)) ~> (~>)
dayCounit = (Day (Writer r) (Reader ('OP r)) :~> (~>))
-> Prof (Day (Writer r) (Reader ('OP r))) (~>)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Day @_ @d @e a ~> (c ** e)
f (Writer c ~> (r ** d)
p) (Reader (r ** e) ~> f
q) (d ** f) ~> b
g) -> (d ** f) ~> b
g ((d ** f) ~> b) -> (a ~> (d ** f)) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (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
. 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 @d (r ** e) ~> f
(r ** e) ~> f
q ((d ** (r ** e)) ~> (d ** f))
-> (a ~> (d ** (r ** e))) -> a ~> (d ** f)
forall (b :: k) (c :: k) (a :: k). (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
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @d @r @e (((d ** r) ** e) ~> (d ** (r ** e)))
-> (a ~> ((d ** r) ** e)) -> a ~> (d ** (r ** e))
forall (b :: k) (c :: k) (a :: k). (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
. 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 @e (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @r @d ((r ** d) ~> (d ** r)) -> (c ~> (r ** d)) -> c ~> (d ** r)
forall (b :: k) (c :: k) (a :: k). (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
. c ~> (r ** d)
p) ((c ** e) ~> ((d ** r) ** e))
-> (a ~> (c ** e)) -> a ~> ((d ** r) ** e)
forall (b :: k) (c :: k) (a :: k). (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
. a ~> (c ** e)
f

readerComp
  :: forall {k} (r :: k) (s :: k). (SymMonoidal k, Ob r, Ob s) => Reader (OP r) :.: Reader (OP s) ~> Reader (OP (r ** s))
readerComp :: forall {k} (r :: k) (s :: k).
(SymMonoidal k, Ob r, Ob s) =>
(Reader ('OP r) :.: Reader ('OP s)) ~> Reader ('OP (r ** s))
readerComp = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @r @s ((Ob (r ** s) =>
  (Reader ('OP r) :.: Reader ('OP s)) ~> Reader ('OP (r ** s)))
 -> (Reader ('OP r) :.: Reader ('OP s)) ~> Reader ('OP (r ** s)))
-> (Ob (r ** s) =>
    (Reader ('OP r) :.: Reader ('OP s)) ~> Reader ('OP (r ** s)))
-> (Reader ('OP r) :.: Reader ('OP s)) ~> Reader ('OP (r ** s))
forall a b. (a -> b) -> a -> b
$
  ((Reader ('OP r) :.: Reader ('OP s)) :~> Reader ('OP (r ** s)))
-> Prof (Reader ('OP r) :.: Reader ('OP s)) (Reader ('OP (r ** s)))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Reader @a (r ** a) ~> b
f :.: Reader (r ** b) ~> b
g) -> (((r ** s) ** a) ~> b) -> Reader ('OP (r ** s)) a b
forall {k} (a :: k) (b :: k) (r :: k).
Ob a =>
((r ** a) ~> b) -> Reader ('OP r) a b
Reader ((s ** b) ~> b
(r ** b) ~> b
g ((s ** b) ~> b)
-> (((r ** s) ** a) ~> (s ** b)) -> ((r ** s) ** a) ~> b
forall (b :: k) (c :: k) (a :: k). (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
. 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 @s (r ** a) ~> b
(r ** a) ~> b
f ((s ** (r ** a)) ~> (s ** b))
-> (((r ** s) ** a) ~> (s ** (r ** a)))
-> ((r ** s) ** a) ~> (s ** b)
forall (b :: k) (c :: k) (a :: k). (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
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @s @r @a (((s ** r) ** a) ~> (s ** (r ** a)))
-> (((r ** s) ** a) ~> ((s ** r) ** a))
-> ((r ** s) ** a) ~> (s ** (r ** a))
forall (b :: k) (c :: k) (a :: k). (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
. 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 @a (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @r @s))

readerDay
  :: forall {k} (r :: k) (s :: k). (SymMonoidal k, Ob r, Ob s) => Reader (OP r) `Day` Reader (OP s) ~> Reader (OP (r ** s))
readerDay :: forall {k} (r :: k) (s :: k).
(SymMonoidal k, Ob r, Ob s) =>
Day (Reader ('OP r)) (Reader ('OP s)) ~> Reader ('OP (r ** s))
readerDay = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @r @s ((Ob (r ** s) =>
  Day (Reader ('OP r)) (Reader ('OP s)) ~> Reader ('OP (r ** s)))
 -> Day (Reader ('OP r)) (Reader ('OP s)) ~> Reader ('OP (r ** s)))
-> (Ob (r ** s) =>
    Day (Reader ('OP r)) (Reader ('OP s)) ~> Reader ('OP (r ** s)))
-> Day (Reader ('OP r)) (Reader ('OP s)) ~> Reader ('OP (r ** s))
forall a b. (a -> b) -> a -> b
$
  (Day (Reader ('OP r)) (Reader ('OP s)) :~> Reader ('OP (r ** s)))
-> Prof
     (Day (Reader ('OP r)) (Reader ('OP s))) (Reader ('OP (r ** s)))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Day @c @_ @e @_ a ~> (c ** e)
f (Reader (r ** c) ~> d
p) (Reader (r ** e) ~> f
q) (d ** f) ~> b
g) -> (((r ** s) ** a) ~> b) -> Reader ('OP (r ** s)) a b
forall {k} (a :: k) (b :: k) (r :: k).
Ob a =>
((r ** a) ~> b) -> Reader ('OP r) a b
Reader ((d ** f) ~> b
g ((d ** f) ~> b)
-> (((r ** s) ** a) ~> (d ** f)) -> ((r ** s) ** a) ~> b
forall (b :: k) (c :: k) (a :: k). (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
. ((r ** c) ~> d
(r ** c) ~> d
p ((r ** c) ~> d)
-> ((s ** e) ~> f) -> ((r ** c) ** (s ** e)) ~> (d ** f)
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` (s ** e) ~> f
(r ** e) ~> f
q) (((r ** c) ** (s ** e)) ~> (d ** f))
-> (((r ** s) ** a) ~> ((r ** c) ** (s ** e)))
-> ((r ** s) ** a) ~> (d ** f)
forall (b :: k) (c :: k) (a :: k). (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
. forall (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
swapInner @r @s @c @e (((r ** s) ** (c ** e)) ~> ((r ** c) ** (s ** e)))
-> (((r ** s) ** a) ~> ((r ** s) ** (c ** e)))
-> ((r ** s) ** a) ~> ((r ** c) ** (s ** e))
forall (b :: k) (c :: k) (a :: k). (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
. 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 @(r ** s) a ~> (c ** e)
f) ((Ob a, Ob (c ** e)) => Reader ('OP (r ** s)) a b)
-> (a ~> (c ** e)) -> Reader ('OP (r ** s)) a b
forall (a :: k) (b :: k) 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
\\ a ~> (c ** e)
f