{-# OPTIONS_GHC -Wno-orphans #-} module Proarrow.Profunctor.Day where import Proarrow.Core (PRO, Profunctor(..), CategoryOf(..), Promonad(..), lmap, rmap, (//)) import Proarrow.Category.Instance.Prof (Prof(..)) import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..), swap) import Proarrow.Object (src, tgt) import Proarrow.Monoid (Monoid (..)) import Proarrow.Object.Exponential (Closed(..)) data DayUnit a b where DayUnit :: a ~> Unit -> Unit ~> b -> DayUnit a b instance (CategoryOf j, CategoryOf k) => Profunctor (DayUnit :: PRO j k) where dimap :: forall (c :: j) (a :: j) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> DayUnit a b -> DayUnit c d dimap c ~> a l b ~> d r (DayUnit a ~> Unit f Unit ~> b g) = (c ~> Unit) -> (Unit ~> d) -> DayUnit c d forall {k} {k} (a :: k) (b :: k). (a ~> Unit) -> (Unit ~> b) -> DayUnit a b DayUnit (a ~> Unit f (a ~> Unit) -> (c ~> a) -> c ~> Unit forall (b :: j) (c :: j) (a :: j). (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) (b ~> d r (b ~> d) -> (Unit ~> b) -> Unit ~> 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 . Unit ~> b g) (Ob a, Ob b) => r r \\ :: forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> DayUnit a b -> r \\ DayUnit a ~> Unit f Unit ~> b g = r (Ob a, Ob Unit) => r (Ob a, Ob b) => r r ((Ob a, Ob Unit) => r) -> (a ~> Unit) -> r forall (a :: j) (b :: j) 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 ~> Unit f ((Ob Unit, Ob b) => r) -> (Unit ~> 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 \\ Unit ~> b g data Day p q a b where Day :: forall p q a b c d e f. a ~> c ** e -> p c d -> q e f -> d ** f ~> b -> Day p q a b instance (Profunctor p, Profunctor q) => Profunctor (Day p q) where dimap :: forall (c :: j) (a :: j) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> Day p q a b -> Day p q c d dimap c ~> a l b ~> d r (Day a ~> (c ** e) f p c d p q e f q (d ** f) ~> b g) = (c ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> d) -> Day p q c d forall {k} {k} (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). (a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b Day ((c ~> a) -> (a ~> (c ** e)) -> c ~> (c ** e) forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k). Profunctor p => (c ~> a) -> p a b -> p c b lmap c ~> a l a ~> (c ** e) f) p c d p q e f q ((b ~> d) -> ((d ** f) ~> b) -> (d ** f) ~> d forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j). Profunctor p => (b ~> d) -> p a b -> p a d rmap b ~> d r (d ** f) ~> b g) (Ob a, Ob b) => r r \\ :: forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> Day p q a b -> r \\ Day a ~> (c ** e) f p c d _ q e f _ (d ** f) ~> b g = r (Ob a, Ob (c ** e)) => r (Ob a, Ob b) => r r ((Ob a, Ob (c ** e)) => r) -> (a ~> (c ** e)) -> r forall (a :: j) (b :: j) 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 ~> (c ** e) f ((Ob (d ** f), Ob b) => r) -> ((d ** f) ~> 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 \\ (d ** f) ~> b g instance (Monoidal j, Monoidal k) => Monoidal (PRO j k) where type Unit = DayUnit type p ** q = Day p q Prof a :~> b m par :: forall (a :: PRO j k) (b :: PRO j k) (c :: PRO j k) (d :: PRO j k). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` Prof c :~> d n = (Day a c :~> Day b d) -> Prof (Day a c) (Day b d) forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \(Day a ~> (c ** e) f a c d p c e f q (d ** f) ~> b g) -> (a ~> (c ** e)) -> b c d -> d e f -> ((d ** f) ~> b) -> Day b d a b forall {k} {k} (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). (a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b Day a ~> (c ** e) f (a c d -> b c d a :~> b m a c d p) (c e f -> d e f c :~> d n c e f q) (d ** f) ~> b g leftUnitor :: forall (a :: PRO j k). Obj a -> (Unit ** a) ~> a leftUnitor Prof{} = (Day DayUnit a :~> a) -> Prof (Day DayUnit a) a forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \(Day a ~> (c ** e) f (DayUnit c ~> Unit h Unit ~> d i) a e f q (d ** f) ~> b g) -> (a ~> e) -> (f ~> b) -> a e f -> a a b forall (c :: j) (a :: j) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> a a b -> a c d forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k). Profunctor p => (c ~> a) -> (b ~> d) -> p a b -> p c d dimap (Obj e -> (Unit ** e) ~> e forall (a :: j). Obj a -> (Unit ** a) ~> a forall k (a :: k). Monoidal k => Obj a -> (Unit ** a) ~> a leftUnitor (a e f -> Obj e forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src a e f q) ((Unit ** e) ~> e) -> (a ~> (Unit ** e)) -> a ~> e forall (b :: j) (c :: j) (a :: j). (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 ~> Unit h (c ~> Unit) -> Obj e -> (c ** e) ~> (Unit ** e) forall (a :: j) (b :: j) (c :: j) (d :: j). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) forall k (a :: k) (b :: k) (c :: k) (d :: k). Monoidal k => (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` a e f -> Obj e forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src a e f q) ((c ** e) ~> (Unit ** e)) -> (a ~> (c ** e)) -> a ~> (Unit ** e) forall (b :: j) (c :: j) (a :: j). (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 ~> (c ** e) f) ((d ** f) ~> b g ((d ** f) ~> b) -> (f ~> (d ** f)) -> f ~> 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 . (Unit ~> d i (Unit ~> d) -> (f ~> f) -> (Unit ** f) ~> (d ** f) forall (a :: k) (b :: k) (c :: k) (d :: k). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) forall k (a :: k) (b :: k) (c :: k) (d :: k). Monoidal k => (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` a e f -> f ~> f forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt a e f q) ((Unit ** f) ~> (d ** f)) -> (f ~> (Unit ** f)) -> f ~> (d ** f) 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 . (f ~> f) -> f ~> (Unit ** f) forall (a :: k). Obj a -> a ~> (Unit ** a) forall k (a :: k). Monoidal k => Obj a -> a ~> (Unit ** a) leftUnitorInv (a e f -> f ~> f forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt a e f q)) a e f q leftUnitorInv :: forall (a :: PRO j k). Obj a -> a ~> (Unit ** a) leftUnitorInv Prof{} = (a :~> Day DayUnit a) -> Prof a (Day DayUnit a) forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \a a b q -> (a ~> (Unit ** a)) -> DayUnit Unit Unit -> a a b -> ((Unit ** b) ~> b) -> Day DayUnit a a b forall {k} {k} (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). (a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b Day (Obj a -> a ~> (Unit ** a) forall (a :: j). Obj a -> a ~> (Unit ** a) forall k (a :: k). Monoidal k => Obj a -> a ~> (Unit ** a) leftUnitorInv (a a b -> Obj a forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src a a b q)) ((Unit ~> Unit) -> (Unit ~> Unit) -> DayUnit Unit Unit forall {k} {k} (a :: k) (b :: k). (a ~> Unit) -> (Unit ~> b) -> DayUnit a b DayUnit Unit ~> Unit forall (a :: j). Ob a => a ~> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id Unit ~> Unit forall (a :: k). Ob a => a ~> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id) a a b q (Obj b -> (Unit ** b) ~> b forall (a :: k). Obj a -> (Unit ** a) ~> a forall k (a :: k). Monoidal k => Obj a -> (Unit ** a) ~> a leftUnitor (a a b -> Obj b forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt a a b q)) rightUnitor :: forall (a :: PRO j k). Obj a -> (a ** Unit) ~> a rightUnitor Prof{} = (Day a DayUnit :~> a) -> Prof (Day a DayUnit) a forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \(Day a ~> (c ** e) f a c d p (DayUnit e ~> Unit h Unit ~> f i) (d ** f) ~> b g) -> (a ~> c) -> (d ~> b) -> a c d -> a a b forall (c :: j) (a :: j) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> a a b -> a c d forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k). Profunctor p => (c ~> a) -> (b ~> d) -> p a b -> p c d dimap (Obj c -> (c ** Unit) ~> c forall (a :: j). Obj a -> (a ** Unit) ~> a forall k (a :: k). Monoidal k => Obj a -> (a ** Unit) ~> a rightUnitor (a c d -> Obj c forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src a c d p) ((c ** Unit) ~> c) -> (a ~> (c ** Unit)) -> a ~> c forall (b :: j) (c :: j) (a :: j). (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 c d -> Obj c forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src a c d p Obj c -> (e ~> Unit) -> (c ** e) ~> (c ** Unit) forall (a :: j) (b :: j) (c :: j) (d :: j). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) forall k (a :: k) (b :: k) (c :: k) (d :: k). Monoidal k => (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` e ~> Unit h) ((c ** e) ~> (c ** Unit)) -> (a ~> (c ** e)) -> a ~> (c ** Unit) forall (b :: j) (c :: j) (a :: j). (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 ~> (c ** e) f) ((d ** f) ~> b g ((d ** f) ~> b) -> (d ~> (d ** f)) -> d ~> 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 c d -> d ~> d forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt a c d p (d ~> d) -> (Unit ~> f) -> (d ** Unit) ~> (d ** f) forall (a :: k) (b :: k) (c :: k) (d :: k). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) forall k (a :: k) (b :: k) (c :: k) (d :: k). Monoidal k => (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` Unit ~> f i) ((d ** Unit) ~> (d ** f)) -> (d ~> (d ** Unit)) -> d ~> (d ** f) 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 . (d ~> d) -> d ~> (d ** Unit) forall (a :: k). Obj a -> a ~> (a ** Unit) forall k (a :: k). Monoidal k => Obj a -> a ~> (a ** Unit) rightUnitorInv (a c d -> d ~> d forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt a c d p)) a c d p rightUnitorInv :: forall (a :: PRO j k). Obj a -> a ~> (a ** Unit) rightUnitorInv Prof{} = (a :~> Day a DayUnit) -> Prof a (Day a DayUnit) forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \a a b p -> (a ~> (a ** Unit)) -> a a b -> DayUnit Unit Unit -> ((b ** Unit) ~> b) -> Day a DayUnit a b forall {k} {k} (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). (a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b Day (Obj a -> a ~> (a ** Unit) forall (a :: j). Obj a -> a ~> (a ** Unit) forall k (a :: k). Monoidal k => Obj a -> a ~> (a ** Unit) rightUnitorInv (a a b -> Obj a forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src a a b p)) a a b p ((Unit ~> Unit) -> (Unit ~> Unit) -> DayUnit Unit Unit forall {k} {k} (a :: k) (b :: k). (a ~> Unit) -> (Unit ~> b) -> DayUnit a b DayUnit Unit ~> Unit forall (a :: j). Ob a => a ~> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id Unit ~> Unit forall (a :: k). Ob a => a ~> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id) (Obj b -> (b ** Unit) ~> b forall (a :: k). Obj a -> (a ** Unit) ~> a forall k (a :: k). Monoidal k => Obj a -> (a ** Unit) ~> a rightUnitor (a a b -> Obj b forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt a a b p)) associator :: forall (a :: PRO j k) (b :: PRO j k) (c :: PRO j k). Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c)) associator Prof{} Prof{} Prof{} = (Day (Day a b) c :~> Day a (Day b c)) -> Prof (Day (Day a b) c) (Day a (Day b c)) forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \(Day a ~> (c ** e) f1 (Day c ~> (c ** e) f2 a c d p2 b e f q2 (d ** f) ~> d g2) c e f q1 (d ** f) ~> b g1) -> let f :: a ~> (c ** (e ** e)) f = Obj c -> Obj e -> Obj e -> ((c ** e) ** e) ~> (c ** (e ** e)) forall (a :: j) (b :: j) (c :: j). Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c)) forall k (a :: k) (b :: k) (c :: k). Monoidal k => Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c)) associator (a c d -> Obj c forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src a c d p2) (b e f -> Obj e forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src b e f q2) (c e f -> Obj e forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src c e f q1) (((c ** e) ** e) ~> (c ** (e ** e))) -> (a ~> ((c ** e) ** e)) -> a ~> (c ** (e ** e)) forall (b :: j) (c :: j) (a :: j). (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 ~> (c ** e) f2 (c ~> (c ** e)) -> Obj e -> (c ** e) ~> ((c ** e) ** e) forall (a :: j) (b :: j) (c :: j) (d :: j). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) forall k (a :: k) (b :: k) (c :: k) (d :: k). Monoidal k => (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` c e f -> Obj e forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src c e f q1) ((c ** e) ~> ((c ** e) ** e)) -> (a ~> (c ** e)) -> a ~> ((c ** e) ** e) forall (b :: j) (c :: j) (a :: j). (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 ~> (c ** e) f1 g :: (d ** (f ** f)) ~> b g = (d ** f) ~> b g1 ((d ** f) ~> b) -> ((d ** (f ** f)) ~> (d ** f)) -> (d ** (f ** f)) ~> 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 . ((d ** f) ~> d g2 ((d ** f) ~> d) -> (f ~> f) -> ((d ** f) ** f) ~> (d ** f) forall (a :: k) (b :: k) (c :: k) (d :: k). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) forall k (a :: k) (b :: k) (c :: k) (d :: k). Monoidal k => (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` c e f -> f ~> f forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt c e f q1) (((d ** f) ** f) ~> (d ** f)) -> ((d ** (f ** f)) ~> ((d ** f) ** f)) -> (d ** (f ** f)) ~> (d ** f) 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 . Obj d -> Obj f -> (f ~> f) -> (d ** (f ** f)) ~> ((d ** f) ** f) forall (a :: k) (b :: k) (c :: k). Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c) forall k (a :: k) (b :: k) (c :: k). Monoidal k => Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c) associatorInv (a c d -> Obj d forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt a c d p2) (b e f -> Obj f forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt b e f q2) (c e f -> f ~> f forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt c e f q1) in (a ~> (c ** (e ** e))) -> a c d -> Day b c (e ** e) (f ** f) -> ((d ** (f ** f)) ~> b) -> Day a (Day b c) a b forall {k} {k} (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). (a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b Day a ~> (c ** (e ** e)) f a c d p2 (((e ** e) ~> (e ** e)) -> b e f -> c e f -> ((f ** f) ~> (f ** f)) -> Day b c (e ** e) (f ** f) forall {k} {k} (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). (a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b Day (b e f -> Obj e forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src b e f q2 Obj e -> Obj e -> (e ** e) ~> (e ** e) forall (a :: j) (b :: j) (c :: j) (d :: j). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) forall k (a :: k) (b :: k) (c :: k) (d :: k). Monoidal k => (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` c e f -> Obj e forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src c e f q1) b e f q2 c e f q1 (b e f -> Obj f forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt b e f q2 Obj f -> (f ~> f) -> (f ** f) ~> (f ** f) forall (a :: k) (b :: k) (c :: k) (d :: k). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) forall k (a :: k) (b :: k) (c :: k) (d :: k). Monoidal k => (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` c e f -> f ~> f forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt c e f q1)) (d ** (f ** f)) ~> b g associatorInv :: forall (a :: PRO j k) (b :: PRO j k) (c :: PRO j k). Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c) associatorInv Prof{} Prof{} Prof{} = (Day a (Day b c) :~> Day (Day a b) c) -> Prof (Day a (Day b c)) (Day (Day a b) c) forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \(Day a ~> (c ** e) f1 a c d p1 (Day e ~> (c ** e) f2 b c d p2 c e f q2 (d ** f) ~> f g2) (d ** f) ~> b g1) -> let f :: a ~> ((c ** c) ** e) f = Obj c -> Obj c -> Obj e -> (c ** (c ** e)) ~> ((c ** c) ** e) forall (a :: j) (b :: j) (c :: j). Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c) forall k (a :: k) (b :: k) (c :: k). Monoidal k => Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c) associatorInv (a c d -> Obj c forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src a c d p1) (b c d -> Obj c forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src b c d p2) (c e f -> Obj e forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src c e f q2) ((c ** (c ** e)) ~> ((c ** c) ** e)) -> (a ~> (c ** (c ** e))) -> a ~> ((c ** c) ** e) forall (b :: j) (c :: j) (a :: j). (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 c d -> Obj c forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src a c d p1 Obj c -> (e ~> (c ** e)) -> (c ** e) ~> (c ** (c ** e)) forall (a :: j) (b :: j) (c :: j) (d :: j). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) forall k (a :: k) (b :: k) (c :: k) (d :: k). Monoidal k => (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` e ~> (c ** e) f2) ((c ** e) ~> (c ** (c ** e))) -> (a ~> (c ** e)) -> a ~> (c ** (c ** e)) forall (b :: j) (c :: j) (a :: j). (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 ~> (c ** e) f1 g :: ((d ** d) ** f) ~> b g = (d ** f) ~> b g1 ((d ** f) ~> b) -> (((d ** d) ** f) ~> (d ** f)) -> ((d ** d) ** f) ~> 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 c d -> d ~> d forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt a c d p1 (d ~> d) -> ((d ** f) ~> f) -> (d ** (d ** f)) ~> (d ** f) forall (a :: k) (b :: k) (c :: k) (d :: k). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) forall k (a :: k) (b :: k) (c :: k) (d :: k). Monoidal k => (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` (d ** f) ~> f g2) ((d ** (d ** f)) ~> (d ** f)) -> (((d ** d) ** f) ~> (d ** (d ** f))) -> ((d ** d) ** f) ~> (d ** f) 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 . (d ~> d) -> Obj d -> Obj f -> ((d ** d) ** f) ~> (d ** (d ** f)) forall (a :: k) (b :: k) (c :: k). Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c)) forall k (a :: k) (b :: k) (c :: k). Monoidal k => Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c)) associator (a c d -> d ~> d forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt a c d p1) (b c d -> Obj d forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt b c d p2) (c e f -> Obj f forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt c e f q2) in (a ~> ((c ** c) ** e)) -> Day a b (c ** c) (d ** d) -> c e f -> (((d ** d) ** f) ~> b) -> Day (Day a b) c a b forall {k} {k} (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). (a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b Day a ~> ((c ** c) ** e) f (((c ** c) ~> (c ** c)) -> a c d -> b c d -> ((d ** d) ~> (d ** d)) -> Day a b (c ** c) (d ** d) forall {k} {k} (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). (a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b Day (a c d -> Obj c forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src a c d p1 Obj c -> Obj c -> (c ** c) ~> (c ** c) forall (a :: j) (b :: j) (c :: j) (d :: j). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) forall k (a :: k) (b :: k) (c :: k) (d :: k). Monoidal k => (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` b c d -> Obj c forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src b c d p2) a c d p1 b c d p2 (a c d -> d ~> d forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt a c d p1 (d ~> d) -> Obj d -> (d ** d) ~> (d ** d) forall (a :: k) (b :: k) (c :: k) (d :: k). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) forall k (a :: k) (b :: k) (c :: k) (d :: k). Monoidal k => (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` b c d -> Obj d forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt b c d p2)) c e f q2 ((d ** d) ** f) ~> b g instance (SymMonoidal j, SymMonoidal k) => SymMonoidal (PRO j k) where swap' :: forall (a :: PRO j k) (b :: PRO j k). Obj a -> Obj b -> (a ** b) ~> (b ** a) swap' Prof{} Prof{} = (Day a b :~> Day b a) -> Prof (Day a b) (Day b a) forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \(Day @p @q @a @b @c @d @e @f a ~> (c ** e) f a c d p b e f q (d ** f) ~> b g) -> (a ~> (e ** c)) -> b e f -> a c d -> ((f ** d) ~> b) -> Day b a a b forall {k} {k} (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). (a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b Day (forall (a :: j) (b :: j). (SymMonoidal j, Ob a, Ob b) => (a ** b) ~> (b ** a) forall {k} (a :: k) (b :: k). (SymMonoidal k, Ob a, Ob b) => (a ** b) ~> (b ** a) swap @c @e ((c ** e) ~> (e ** c)) -> (a ~> (c ** e)) -> a ~> (e ** c) forall (b :: j) (c :: j) (a :: j). (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 ~> (c ** e) f) b e f q a c d p ((d ** f) ~> b g ((d ** f) ~> b) -> ((f ** d) ~> (d ** f)) -> (f ** d) ~> 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 :: k) (b :: k). (SymMonoidal k, Ob a, Ob b) => (a ** b) ~> (b ** a) forall {k} (a :: k) (b :: k). (SymMonoidal k, Ob a, Ob b) => (a ** b) ~> (b ** a) swap @f @d) ((Ob c, Ob d) => Day b a a b) -> a c d -> Day b a a b forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> a 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 c d p ((Ob e, Ob f) => Day b a a b) -> b e f -> Day b a a b forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> b 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 e f q data DayExp p q a b where DayExp :: forall p q a b. (Ob a, Ob b) => (forall c d e f. e ~> a ** c -> b ** d ~> f -> p c d -> q e f) -> DayExp p q a b instance (Monoidal j, Monoidal k, Profunctor p, Profunctor q) => Profunctor (DayExp (p :: PRO j k) q) where dimap :: forall (c :: j) (a :: j) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> DayExp p q a b -> DayExp p q c d dimap c ~> a l b ~> d r (DayExp forall (c :: j) (d :: k) (e :: j) (f :: k). (e ~> (a ** c)) -> ((b ** d) ~> f) -> p c d -> q e f n) = c ~> a l (c ~> a) -> ((Ob c, Ob a) => DayExp p q c d) -> DayExp p q c d forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r. Profunctor p => p a b -> ((Ob a, Ob b) => r) -> r // b ~> d r (b ~> d) -> ((Ob b, Ob d) => DayExp p q c d) -> DayExp p q c d forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r. Profunctor p => p a b -> ((Ob a, Ob b) => r) -> r // (forall (c :: j) (d :: k) (e :: j) (f :: k). (e ~> (c ** c)) -> ((d ** d) ~> f) -> p c d -> q e f) -> DayExp p q c d forall {k} {k} (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k). (Ob a, Ob b) => (forall (c :: k) (d :: k) (e :: k) (f :: k). (e ~> (a ** c)) -> ((b ** d) ~> f) -> p c d -> q e f) -> DayExp p q a b DayExp \e ~> (c ** c) f (d ** d) ~> f g p c d p -> (e ~> (a ** c)) -> ((b ** d) ~> f) -> p c d -> q e f forall (c :: j) (d :: k) (e :: j) (f :: k). (e ~> (a ** c)) -> ((b ** d) ~> f) -> p c d -> q e f n ((c ~> a l (c ~> a) -> (c ~> c) -> (c ** c) ~> (a ** c) forall (a :: j) (b :: j) (c :: j) (d :: j). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) forall k (a :: k) (b :: k) (c :: k) (d :: k). Monoidal k => (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` p c d -> c ~> c forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj a src p c d p) ((c ** c) ~> (a ** c)) -> (e ~> (c ** c)) -> e ~> (a ** c) forall (b :: j) (c :: j) (a :: j). (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 . e ~> (c ** c) f) ((d ** d) ~> f g ((d ** d) ~> f) -> ((b ** d) ~> (d ** d)) -> (b ** d) ~> f 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 ~> d r (b ~> d) -> (d ~> d) -> (b ** d) ~> (d ** d) forall (a :: k) (b :: k) (c :: k) (d :: k). (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) forall k (a :: k) (b :: k) (c :: k) (d :: k). Monoidal k => (a ~> b) -> (c ~> d) -> (a ** c) ~> (b ** d) `par` p c d -> d ~> d forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1). Profunctor p => p a b -> Obj b tgt p c d p)) p c d p (Ob a, Ob b) => r r \\ :: forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> DayExp p q a b -> r \\ DayExp forall (c :: j) (d :: k) (e :: j) (f :: k). (e ~> (a ** c)) -> ((b ** d) ~> f) -> p c d -> q e f n = r (Ob a, Ob b) => r (Ob (Any ~> (a ** Any)), Ob (((b ** Any) ~> Any) -> p Any Any -> q Any Any)) => r r ((Ob (Any ~> (a ** Any)), Ob (((b ** Any) ~> Any) -> p Any Any -> q Any Any)) => r) -> ((Any ~> (a ** Any)) -> ((b ** Any) ~> Any) -> p Any Any -> q Any Any) -> r forall a b 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 \\ (Any ~> (a ** Any)) -> ((b ** Any) ~> Any) -> p Any Any -> q Any Any forall (c :: j) (d :: k) (e :: j) (f :: k). (e ~> (a ** c)) -> ((b ** d) ~> f) -> p c d -> q e f n instance (Monoidal j, Monoidal k) => Closed (PRO j k) where type p ~~> q = DayExp p q curry' :: forall (a :: PRO j k) (b :: PRO j k) (c :: PRO j k). Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c) curry' Prof{} Prof{} (Prof Day a b :~> c n) = (a :~> DayExp b c) -> Prof a (DayExp b c) forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \a a b p -> a a b p a a b -> ((Ob a, Ob b) => DayExp b c a b) -> DayExp b c a b forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r. Profunctor p => p a b -> ((Ob a, Ob b) => r) -> r // (forall (c :: j) (d :: k) (e :: j) (f :: k). (e ~> (a ** c)) -> ((b ** d) ~> f) -> b c d -> c e f) -> DayExp b c a b forall {k} {k} (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k). (Ob a, Ob b) => (forall (c :: k) (d :: k) (e :: k) (f :: k). (e ~> (a ** c)) -> ((b ** d) ~> f) -> p c d -> q e f) -> DayExp p q a b DayExp \e ~> (a ** c) f (b ** d) ~> f g b c d q -> Day a b e f -> c e f Day a b :~> c n ((e ~> (a ** c)) -> a a b -> b c d -> ((b ** d) ~> f) -> Day a b e f forall {k} {k} (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k). (a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b Day e ~> (a ** c) f a a b p b c d q (b ** d) ~> f g) uncurry' :: forall (b :: PRO j k) (c :: PRO j k) (a :: PRO j k). Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c uncurry' Prof{} Prof{} (Prof a :~> DayExp b c n) = (Day a b :~> c) -> Prof (Day a b) c forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \(Day a ~> (c ** e) f a c d p b e f q (d ** f) ~> b g) -> case a c d -> DayExp b c c d a :~> DayExp b c n a c d p of DayExp forall (c :: j) (d :: k) (e :: j) (f :: k). (e ~> (c ** c)) -> ((d ** d) ~> f) -> b c d -> c e f h -> (a ~> (c ** e)) -> ((d ** f) ~> b) -> b e f -> c a b forall (c :: j) (d :: k) (e :: j) (f :: k). (e ~> (c ** c)) -> ((d ** d) ~> f) -> b c d -> c e f h a ~> (c ** e) f (d ** f) ~> b g b e f q ^^^ :: forall (b :: PRO j k) (y :: PRO j k) (x :: PRO j k) (a :: PRO j k). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) (^^^) (Prof b :~> y n) (Prof x :~> a m) = (DayExp a b :~> DayExp x y) -> Prof (DayExp a b) (DayExp x y) forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \(DayExp forall (c :: j) (d :: k) (e :: j) (f :: k). (e ~> (a ** c)) -> ((b ** d) ~> f) -> a c d -> b e f k) -> (forall (c :: j) (d :: k) (e :: j) (f :: k). (e ~> (a ** c)) -> ((b ** d) ~> f) -> x c d -> y e f) -> DayExp x y a b forall {k} {k} (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k). (Ob a, Ob b) => (forall (c :: k) (d :: k) (e :: k) (f :: k). (e ~> (a ** c)) -> ((b ** d) ~> f) -> p c d -> q e f) -> DayExp p q a b DayExp \e ~> (a ** c) f (b ** d) ~> f g x c d p -> b e f -> y e f b :~> y n ((e ~> (a ** c)) -> ((b ** d) ~> f) -> a c d -> b e f forall (c :: j) (d :: k) (e :: j) (f :: k). (e ~> (a ** c)) -> ((b ** d) ~> f) -> a c d -> b e f k e ~> (a ** c) f (b ** d) ~> f g (x c d -> a c d x :~> a m x c d p)) instance (Profunctor p, MonoidalProfunctor p) => Monoid p where mempty :: Unit ~> p mempty = (DayUnit :~> p) -> Prof DayUnit p forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \(DayUnit a ~> Unit f Unit ~> b g) -> (a ~> Unit) -> (Unit ~> b) -> p Unit Unit -> p a b forall (c :: j) (a :: j) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> p a b -> p c d forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k). Profunctor p => (c ~> a) -> (b ~> d) -> p a b -> p c d dimap a ~> Unit f Unit ~> b g p Unit Unit forall j k (p :: PRO j k). MonoidalProfunctor p => p Unit Unit lift0 mappend :: (p ** p) ~> p mappend = (Day p p :~> p) -> Prof (Day p p) p forall {j} {k} (p :: PRO j k) (q :: PRO j k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \(Day a ~> (c ** e) f p c d p p e f q (d ** f) ~> b g) -> (a ~> (c ** e)) -> ((d ** f) ~> b) -> p (c ** e) (d ** f) -> p a b forall (c :: j) (a :: j) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> p a b -> p c d forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k). Profunctor p => (c ~> a) -> (b ~> d) -> p a b -> p c d dimap a ~> (c ** e) f (d ** f) ~> b g (p c d -> p e f -> p (c ** e) (d ** f) forall (x1 :: j) (x2 :: k) (y1 :: j) (y2 :: k). p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2) forall j k (p :: PRO j k) (x1 :: j) (x2 :: k) (y1 :: j) (y2 :: k). MonoidalProfunctor p => p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2) lift2 p c d p p e f q)