{-# 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)