{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Profunctor.Day where

import Proarrow.Category.Instance.Nat (Nat (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..), swap, swapInner', unitObj)
import Proarrow.Category.Monoidal.Distributive (Distributive (..))
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , PRO
  , Profunctor (..)
  , Promonad (..)
  , lmap
  , obj
  , rmap
  , src
  , tgt
  , (//)
  , type (+->)
  )
import Proarrow.Functor (Functor (..))
import Proarrow.Monoid (Monoid (..))
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Profunctor.Composition ((:.:) (..))
import Proarrow.Profunctor.Coproduct ((:+:) (..))

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 c d e f p q a b. 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} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: 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 (Profunctor p) => Functor (Day p) where
  map :: forall (a :: k -> k -> Type) (b :: k -> k -> Type).
(a ~> b) -> Day p a ~> Day p b
map (Prof a :~> b
n) = (Day p a :~> Day p b) -> Prof (Day p a) (Day p b)
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Day a ~> (c ** e)
f p c d
p a e f
q (d ** f) ~> b
g) -> (a ~> (c ** e)) -> p c d -> b e f -> ((d ** f) ~> b) -> Day p b a b
forall {k} {k} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k).
(a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b
Day a ~> (c ** e)
f p c d
p (a e f -> b e f
a :~> b
n a e f
q) (d ** f) ~> b
g

instance Functor Day where
  map :: forall (a :: k -> k -> Type) (b :: k -> k -> Type).
(a ~> b) -> Day a ~> Day b
map (Prof a :~> b
n) = (Day a .~> Day b) -> Nat (Day a) (Day b)
forall {j} {k} (f :: j -> k) (g :: j -> k).
(Functor f, Functor g) =>
(f .~> g) -> Nat f g
Nat ((Day a a :~> Day b a) -> Prof (Day a a) (Day b a)
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Day a ~> (c ** e)
f a c d
p a e f
q (d ** f) ~> b
g) -> (a ~> (c ** e)) -> b c d -> a e f -> ((d ** f) ~> b) -> Day b a a b
forall {k} {k} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: 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
n a c d
p) a e f
q (d ** f) ~> b
g)

instance (SymMonoidal j, SymMonoidal k, MonoidalProfunctor p, MonoidalProfunctor q) => MonoidalProfunctor (Day p q :: PRO j k) where
  par0 :: Day p q Unit Unit
par0 = (Unit ~> (Unit ** Unit))
-> p Unit Unit
-> q Unit Unit
-> ((Unit ** Unit) ~> Unit)
-> Day p q Unit Unit
forall {k} {k} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k).
(a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b
Day Unit ~> (Unit ** Unit)
forall (a :: j). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0 q Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0 (Unit ** Unit) ~> Unit
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor ((Ob Unit, Ob Unit) => Day p q Unit Unit)
-> (Unit ~> Unit) -> Day p q Unit Unit
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
\\ forall k. Monoidal k => Obj Unit
unitObj @j ((Ob Unit, Ob Unit) => Day p q Unit Unit)
-> (Unit ~> Unit) -> Day p q Unit Unit
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ forall k. Monoidal k => Obj Unit
unitObj @k
  Day x1 ~> (c ** e)
f1 p c d
p1 q e f
q1 (d ** f) ~> x2
g1 par :: forall (x1 :: j) (x2 :: k) (y1 :: j) (y2 :: k).
Day p q x1 x2 -> Day p q y1 y2 -> Day p q (x1 ** y1) (x2 ** y2)
`par` Day y1 ~> (c ** e)
f2 p c d
p2 q e f
q2 (d ** f) ~> y2
g2 =
    let f :: (x1 ** y1) ~> ((c ** c) ** (e ** e))
f = (c ~> c)
-> (e ~> e)
-> (c ~> c)
-> (e ~> e)
-> ((c ** e) ** (c ** e)) ~> ((c ** c) ** (e ** e))
forall k (a :: k) (a' :: k) (b :: k) (b' :: k) (c :: k) (c' :: k)
       (d :: k) (d' :: k).
SymMonoidal k =>
(a ~> a')
-> (b ~> b')
-> (c ~> c')
-> (d ~> d')
-> ((a ** b) ** (c ** d)) ~> ((a' ** c') ** (b' ** d'))
swapInner' (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
p1) (q e f -> e ~> e
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src q e f
q1) (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
p2) (q e f -> e ~> e
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src q e f
q2) (((c ** e) ** (c ** e)) ~> ((c ** c) ** (e ** e)))
-> ((x1 ** y1) ~> ((c ** e) ** (c ** e)))
-> (x1 ** y1) ~> ((c ** 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
. (x1 ~> (c ** e)
f1 (x1 ~> (c ** e))
-> (y1 ~> (c ** e)) -> (x1 ** y1) ~> ((c ** e) ** (c ** e))
forall (x1 :: j) (x2 :: j) (y1 :: j) (y2 :: j).
(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` y1 ~> (c ** e)
f2)
        g :: ((d ** d) ** (f ** f)) ~> (x2 ** y2)
g = ((d ** f) ~> x2
g1 ((d ** f) ~> x2)
-> ((d ** f) ~> y2) -> ((d ** f) ** (d ** f)) ~> (x2 ** y2)
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` (d ** f) ~> y2
g2) (((d ** f) ** (d ** f)) ~> (x2 ** y2))
-> (((d ** d) ** (f ** f)) ~> ((d ** f) ** (d ** f)))
-> ((d ** d) ** (f ** f)) ~> (x2 ** y2)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (d ~> d)
-> (d ~> d)
-> (f ~> f)
-> (f ~> f)
-> ((d ** d) ** (f ** f)) ~> ((d ** f) ** (d ** f))
forall k (a :: k) (a' :: k) (b :: k) (b' :: k) (c :: k) (c' :: k)
       (d :: k) (d' :: k).
SymMonoidal k =>
(a ~> a')
-> (b ~> b')
-> (c ~> c')
-> (d ~> d')
-> ((a ** b) ** (c ** d)) ~> ((a' ** c') ** (b' ** d'))
swapInner' (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
p1) (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
p2) (q e f -> f ~> f
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt q e f
q1) (q e f -> f ~> f
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt q e f
q2)
    in ((x1 ** y1) ~> ((c ** c) ** (e ** e)))
-> p (c ** c) (d ** d)
-> q (e ** e) (f ** f)
-> (((d ** d) ** (f ** f)) ~> (x2 ** y2))
-> Day p q (x1 ** y1) (x2 ** y2)
forall {k} {k} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k).
(a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b
Day (x1 ** y1) ~> ((c ** c) ** (e ** e))
f (p c d
p1 p c d -> p c d -> p (c ** c) (d ** d)
forall (x1 :: j) (x2 :: k) (y1 :: j) (y2 :: k).
p x1 x2 -> p y1 y2 -> p (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` p c d
p2) (q e f
q1 q e f -> q e f -> q (e ** e) (f ** f)
forall (x1 :: j) (x2 :: k) (y1 :: j) (y2 :: k).
q x1 x2 -> q y1 y2 -> q (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` q e f
q2) ((d ** d) ** (f ** f)) ~> (x2 ** y2)
g

instance (Monoidal j, Monoidal k) => MonoidalProfunctor (Prof :: CAT (j +-> k)) where
  par0 :: Prof Unit Unit
par0 = Prof Unit Unit
Prof DayUnit DayUnit
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: j +-> k). Ob a => Prof a a
id
  Prof x1 :~> x2
m par :: forall (x1 :: j +-> k) (x2 :: j +-> k) (y1 :: j +-> k)
       (y2 :: j +-> k).
Prof x1 x2 -> Prof y1 y2 -> Prof (x1 ** y1) (x2 ** y2)
`par` Prof y1 :~> y2
n = (Day x1 y1 :~> Day x2 y2) -> Prof (Day x1 y1) (Day x2 y2)
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Day a ~> (c ** e)
f x1 c d
p y1 e f
q (d ** f) ~> b
g) -> (a ~> (c ** e))
-> x2 c d -> y2 e f -> ((d ** f) ~> b) -> Day x2 y2 a b
forall {k} {k} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k).
(a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b
Day a ~> (c ** e)
f (x1 c d -> x2 c d
x1 :~> x2
m x1 c d
p) (y1 e f -> y2 e f
y1 :~> y2
n y1 e f
q) (d ** f) ~> b
g

instance (Monoidal j, Monoidal k) => Monoidal (PRO j k) where
  type Unit = DayUnit
  type p ** q = Day p q
  leftUnitor :: forall (a :: PRO j k). Ob a => (Unit ** a) ~> a
leftUnitor = (Day DayUnit a :~> a) -> Prof (Day DayUnit a) a
forall {k} {j} (p :: j +-> k) (q :: 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 ((Unit ** e) ~> e
forall (a :: j). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor ((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) -> (e ~> e) -> (c ** e) ~> (Unit ** e)
forall (x1 :: j) (x2 :: j) (y1 :: j) (y2 :: j).
(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` a e f -> e ~> 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 (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` 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 ~> (Unit ** f)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv) a e f
q ((Ob e, Ob f) => a a b) -> a e f -> 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 e f
q
  leftUnitorInv :: forall (a :: PRO j k). Ob a => a ~> (Unit ** a)
leftUnitorInv = (a :~> Day DayUnit a) -> Prof a (Day DayUnit a)
forall {k} {j} (p :: j +-> k) (q :: 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} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k).
(a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b
Day a ~> (Unit ** a)
forall (a :: j). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv ((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 {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0 Unit ~> Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0) a a b
q (Unit ** b) ~> b
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor ((Ob a, Ob b) => Day DayUnit a a b) -> a a b -> Day DayUnit 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 a b
q
  rightUnitor :: forall (a :: PRO j k). Ob a => (a ** Unit) ~> a
rightUnitor = (Day a DayUnit :~> a) -> Prof (Day a DayUnit) a
forall {k} {j} (p :: j +-> k) (q :: 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 ((c ** Unit) ~> c
forall (a :: j). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor ((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 -> c ~> 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 ~> c) -> (e ~> Unit) -> (c ** e) ~> (c ** Unit)
forall (x1 :: j) (x2 :: j) (y1 :: j) (y2 :: j).
(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` 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 (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` 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 ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv) a c d
p ((Ob c, Ob d) => a a b) -> a c d -> 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
  rightUnitorInv :: forall (a :: PRO j k). Ob a => a ~> (a ** Unit)
rightUnitorInv = (a :~> Day a DayUnit) -> Prof a (Day a DayUnit)
forall {k} {j} (p :: j +-> k) (q :: 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} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k).
(a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b
Day a ~> (a ** Unit)
forall (a :: j). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv 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 {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0 Unit ~> Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0) (b ** Unit) ~> b
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor ((Ob a, Ob b) => Day a DayUnit a b) -> a a b -> Day a DayUnit 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 a b
p
  associator :: forall (a :: PRO j k) (b :: PRO j k) (c :: PRO j k).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = (Day (Day a b) c :~> Day a (Day b c))
-> Prof (Day (Day a b) c) (Day a (Day b c))
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Day @_ @_ @e1 @f1 a ~> (c ** e)
f1 (Day @c2 @d2 @e2 @f2 c ~> (c ** e)
f2 a c d
p2 b e f
q2 (d ** f) ~> d
g2) c e f
q1 (d ** f) ~> b
g1) -> (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} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k).
(a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b
Day
    (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @c2 @e2 @e1 (((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)) -> (e ~> e) -> (c ** e) ~> ((c ** e) ** e)
forall (x1 :: j) (x2 :: j) (y1 :: j) (y2 :: j).
(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` c e f -> e ~> 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)
    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} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k).
(a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b
Day (b e f -> e ~> e
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src b e f
q2 (e ~> e) -> (e ~> e) -> (e ** e) ~> (e ** e)
forall (x1 :: j) (x2 :: j) (y1 :: j) (y2 :: j).
(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` c e f -> e ~> 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 -> f ~> f
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt b e f
q2 (f ~> f) -> (f ~> f) -> (f ** f) ~> (f ** 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` 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) ~> 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 (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` 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
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @_ @d2 @f2 @f1)
    ((Ob c, Ob d) => Day a (Day b c) a b)
-> a c d -> Day a (Day b c) 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
p2 ((Ob e, Ob f) => Day a (Day b c) a b)
-> b e f -> Day a (Day b c) 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
q2 ((Ob e, Ob f) => Day a (Day b c) a b)
-> c e f -> Day a (Day b c) a b
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> c a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ c e f
q1
  associatorInv :: forall (a :: PRO j k) (b :: PRO j k) (c :: PRO j k).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = (Day a (Day b c) :~> Day (Day a b) c)
-> Prof (Day a (Day b c)) (Day (Day a b) c)
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Day @c1 @d1 a ~> (c ** e)
f1 a c d
p1 (Day @c2 @d2 @e2 @f2 e ~> (c ** e)
f2 b c d
p2 c e f
q2 (d ** f) ~> f
g2) (d ** f) ~> b
g1) -> (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} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k).
(a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b
Day
    (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @_ @c1 @c2 @e2 ((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 -> c ~> c
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src a c d
p1 (c ~> c) -> (e ~> (c ** e)) -> (c ** e) ~> (c ** (c ** e))
forall (x1 :: j) (x2 :: j) (y1 :: j) (y2 :: j).
(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` 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)
    (((c ** c) ~> (c ** c))
-> a c d
-> b c d
-> ((d ** d) ~> (d ** d))
-> Day a b (c ** c) (d ** d)
forall {k} {k} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k).
(a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b
Day (a c d -> c ~> c
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src a c d
p1 (c ~> c) -> (c ~> c) -> (c ** c) ~> (c ** c)
forall (x1 :: j) (x2 :: j) (y1 :: j) (y2 :: j).
(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` b c d -> c ~> 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) -> (d ~> d) -> (d ** d) ~> (d ** d)
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` b c d -> d ~> 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 ** 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 (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` (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
. forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @_ @d1 @d2 @f2)
    ((Ob c, Ob d) => Day (Day a b) c a b)
-> a c d -> Day (Day a b) c 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
p1 ((Ob c, Ob d) => Day (Day a b) c a b)
-> b c d -> Day (Day a b) c 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 c d
p2 ((Ob e, Ob f) => Day (Day a b) c a b)
-> c e f -> Day (Day a b) c a b
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> c a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ c e f
q2

instance (SymMonoidal j, SymMonoidal k) => SymMonoidal (PRO j k) where
  swap' :: forall (a :: PRO j k) (a' :: PRO j k) (b :: PRO j k)
       (b' :: PRO j k).
(a ~> a') -> (b ~> b') -> (a ** b) ~> (b' ** a')
swap' (Prof a :~> a'
n) (Prof b :~> b'
m) = (Day a b :~> Day b' a') -> Prof (Day a b) (Day b' a')
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Day @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} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: 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 -> b' e f
b :~> b'
m b e f
q) (a c d -> a' c d
a :~> a'
n 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

instance (Monoidal j, Monoidal k) => Distributive (PRO j k) where
  distL :: forall (a :: PRO j k) (b :: PRO j k) (c :: PRO j k).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL = (Day a (b :+: c) :~> (Day a b :+: Day a c))
-> Prof (Day a (b :+: c)) (Day a b :+: Day a c)
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Day a ~> (c ** e)
l a c d
a (:+:) b c e f
bc (d ** f) ~> b
r) -> case (:+:) b c e f
bc of
    InjL b e f
b -> Day a b a b -> (:+:) (Day a b) (Day a c) a b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (q :: PRO j k).
p a b -> (:+:) p q a b
InjL ((a ~> (c ** e)) -> a c d -> b e f -> ((d ** f) ~> b) -> Day a b a b
forall {k} {k} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k).
(a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b
Day a ~> (c ** e)
l a c d
a b e f
b (d ** f) ~> b
r)
    InjR c e f
c -> Day a c a b -> (:+:) (Day a b) (Day a c) a b
forall {j} {k} (q :: PRO j k) (a :: j) (b :: k) (p :: PRO j k).
q a b -> (:+:) p q a b
InjR ((a ~> (c ** e)) -> a c d -> c e f -> ((d ** f) ~> b) -> Day a c a b
forall {k} {k} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k).
(a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b
Day a ~> (c ** e)
l a c d
a c e f
c (d ** f) ~> b
r)
  distR :: forall (a :: PRO j k) (b :: PRO j k) (c :: PRO j k).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR = (Day (a :+: b) c :~> (Day a c :+: Day b c))
-> Prof (Day (a :+: b) c) (Day a c :+: Day b c)
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Day a ~> (c ** e)
l (:+:) a b c d
ab c e f
c (d ** f) ~> b
r) -> case (:+:) a b c d
ab of
    InjL a c d
a -> Day a c a b -> (:+:) (Day a c) (Day b c) a b
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (q :: PRO j k).
p a b -> (:+:) p q a b
InjL ((a ~> (c ** e)) -> a c d -> c e f -> ((d ** f) ~> b) -> Day a c a b
forall {k} {k} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k).
(a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b
Day a ~> (c ** e)
l a c d
a c e f
c (d ** f) ~> b
r)
    InjR b c d
b -> Day b c a b -> (:+:) (Day a c) (Day b c) a b
forall {j} {k} (q :: PRO j k) (a :: j) (b :: k) (p :: PRO j k).
q a b -> (:+:) p q a b
InjR ((a ~> (c ** e)) -> b c d -> c e f -> ((d ** f) ~> b) -> Day b c a b
forall {k} {k} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k).
(a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b
Day a ~> (c ** e)
l b c d
b c e f
c (d ** f) ~> b
r)
  distL0 :: forall (a :: PRO j k).
Ob a =>
(a ** InitialObject) ~> InitialObject
distL0 = (Day a InitialProfunctor :~> InitialProfunctor)
-> Prof (Day a InitialProfunctor) InitialProfunctor
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \case {}
  distR0 :: forall (a :: PRO j k).
Ob a =>
(InitialObject ** a) ~> InitialObject
distR0 = (Day InitialProfunctor a :~> InitialProfunctor)
-> Prof (Day InitialProfunctor a) InitialProfunctor
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \case {}

duoidal
  :: (Monoidal k, Profunctor (p :: PRO i k), Profunctor p', Profunctor q, Profunctor q')
  => (p :.: p') `Day` (q :.: q') ~> (p `Day` q) :.: (p' `Day` q')
duoidal :: forall {i} k i (p :: PRO i k) (p' :: PRO k i) (q :: PRO i k)
       (q' :: PRO k i).
(Monoidal k, Profunctor p, Profunctor p', Profunctor q,
 Profunctor q') =>
Day (p :.: p') (q :.: q') ~> (Day p q :.: Day p' q')
duoidal = (Day (p :.: p') (q :.: q') :~> (Day p q :.: Day p' q'))
-> Prof (Day (p :.: p') (q :.: q')) (Day p q :.: Day p' q')
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Day a ~> (c ** e)
f (p c b
p :.: p' b d
p') (q e b
q :.: q' b f
q') (d ** f) ~> b
g) -> let b :: (b ** b) ~> (b ** b)
b = p c b -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt p c b
p (b ~> b) -> (b ~> b) -> (b ** b) ~> (b ** b)
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` q e b -> b ~> b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt q e b
q in (a ~> (c ** e))
-> p c b -> q e b -> ((b ** b) ~> (b ** b)) -> Day p q a (b ** b)
forall {k} {k} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k).
(a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b
Day a ~> (c ** e)
f p c b
p q e b
q (b ** b) ~> (b ** b)
b Day p q a (b ** b)
-> Day p' q' (b ** b) b -> (:.:) (Day p q) (Day p' q') 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
:.: ((b ** b) ~> (b ** b))
-> p' b d -> q' b f -> ((d ** f) ~> b) -> Day p' q' (b ** b) b
forall {k} {k} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k).
(a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b
Day (b ** b) ~> (b ** b)
b p' b d
p' q' b f
q' (d ** f) ~> b
g

instance (Profunctor p, MonoidalProfunctor p) => Monoid p where
  mempty :: Unit ~> p
mempty = (DayUnit :~> p) -> Prof DayUnit p
forall {k} {j} (p :: j +-> k) (q :: 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 :: k) (a :: k) (b :: j) (d :: j).
(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 :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0
  mappend :: (p ** p) ~> p
mappend = (Day p p :~> p) -> Prof (Day p p) p
forall {k} {j} (p :: j +-> k) (q :: 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 :: k) (a :: k) (b :: j) (d :: j).
(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 p c d -> p e f -> p (c ** e) (d ** f)
forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
p x1 x2 -> p y1 y2 -> p (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` p e f
q)

-- instance Monoidal k => Comonoid (E (PK (DayUnit :: PRO k k))) where
--   counit = Endo (Bi.Prof \(DayUnit f g) -> g . f)
--   comult = Endo (Bi.Prof \(DayUnit f g) -> DayUnit f id :.: DayUnit id g)

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 (x1 :: j) (x2 :: j) (y1 :: j) (y2 :: j).
(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` 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 (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` 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 {k} {j} (p :: j +-> k) (q :: 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} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: 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 {k} {j} (p :: j +-> k) (q :: 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 {k} {j} (p :: j +-> k) (q :: 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))

multDayExp
  :: (SymMonoidal j, SymMonoidal k, Profunctor (p :: PRO j k), Profunctor q, Profunctor p', Profunctor q')
  => (p ~~> q) `Day` (p' ~~> q') ~> (p `Day` p') ~~> (q `Day` q')
multDayExp :: forall j k (p :: PRO j k) (q :: PRO j k) (p' :: PRO j k)
       (q' :: PRO j k).
(SymMonoidal j, SymMonoidal k, Profunctor p, Profunctor q,
 Profunctor p', Profunctor q') =>
Day (p ~~> q) (p' ~~> q') ~> (Day p p' ~~> Day q q')
multDayExp = (Day (DayExp p q) (DayExp p' q') :~> DayExp (Day p p') (Day q q'))
-> Prof
     (Day (DayExp p q) (DayExp p' q')) (DayExp (Day p p') (Day q q'))
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Day @c @d @e @f a ~> (c ** e)
g (DayExp forall (c :: j) (d :: k) (e :: j) (f :: k).
(e ~> (c ** c)) -> ((d ** d) ~> f) -> p c d -> q e f
pq) (DayExp forall (c :: j) (d :: k) (e :: j) (f :: k).
(e ~> (e ** c)) -> ((f ** d) ~> f) -> p' c d -> q' e f
pq') (d ** f) ~> b
h) ->
  a ~> (c ** e)
g
    (a ~> (c ** e))
-> ((Ob a, Ob (c ** e)) => DayExp (Day p p') (Day q q') a b)
-> DayExp (Day p p') (Day q q') 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
// (d ** f) ~> b
h
    ((d ** f) ~> b)
-> ((Ob (d ** f), Ob b) => DayExp (Day p p') (Day q q') a b)
-> DayExp (Day p p') (Day q q') 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) -> Day p p' c d -> Day q q' e f)
-> DayExp (Day p p') (Day q q') 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)
l (b ** d) ~> f
r (Day c ~> (c ** e)
i p c d
p p' e f
p' (d ** f) ~> d
j) ->
          p c d
p
            p c d -> ((Ob c, Ob d) => Day q q' e f) -> Day q q' e f
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// p' e f
p'
            p' e f -> ((Ob e, Ob f) => Day q q' e f) -> Day q q' e f
forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// let c :: Obj c
c = forall (a :: j). (CategoryOf j, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c; d :: Obj d
d = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @d; e :: Obj e
e = forall (a :: j). (CategoryOf j, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @e; f :: Obj f
f = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @f; c' :: Obj c
c' = p c d -> Obj c
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src p c d
p; d' :: Obj d
d' = p c d -> Obj d
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt p c d
p; e' :: Obj e
e' = p' e f -> Obj e
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj a
src p' e f
p'; f' :: Obj f
f' = p' e f -> Obj f
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt p' e f
p'
               in (e ~> ((c ** c) ** (e ** e)))
-> q (c ** c) (d ** d)
-> q' (e ** e) (f ** f)
-> (((d ** d) ** (f ** f)) ~> f)
-> Day q q' e f
forall {k} {k} (c :: k) (d :: k) (e :: k) (f :: k)
       (p :: k -> k -> Type) (q :: k -> k -> Type) (a :: k) (b :: k).
(a ~> (c ** e)) -> p c d -> q e f -> ((d ** f) ~> b) -> Day p q a b
Day
                    (Obj c
-> Obj e
-> Obj c
-> Obj e
-> ((c ** e) ** (c ** e)) ~> ((c ** c) ** (e ** e))
forall k (a :: k) (a' :: k) (b :: k) (b' :: k) (c :: k) (c' :: k)
       (d :: k) (d' :: k).
SymMonoidal k =>
(a ~> a')
-> (b ~> b')
-> (c ~> c')
-> (d ~> d')
-> ((a ** b) ** (c ** d)) ~> ((a' ** c') ** (b' ** d'))
swapInner' Obj c
c Obj e
e Obj c
c' Obj e
e' (((c ** e) ** (c ** e)) ~> ((c ** c) ** (e ** e)))
-> (e ~> ((c ** e) ** (c ** e))) -> e ~> ((c ** 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)
g (a ~> (c ** e))
-> (c ~> (c ** e)) -> (a ** c) ~> ((c ** e) ** (c ** e))
forall (x1 :: j) (x2 :: j) (y1 :: j) (y2 :: j).
(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` c ~> (c ** e)
i) ((a ** c) ~> ((c ** e) ** (c ** e)))
-> (e ~> (a ** c)) -> e ~> ((c ** e) ** (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
. e ~> (a ** c)
l)
                    (((c ** c) ~> (c ** c))
-> ((d ** d) ~> (d ** d)) -> p c d -> q (c ** c) (d ** d)
forall (c :: j) (d :: k) (e :: j) (f :: k).
(e ~> (c ** c)) -> ((d ** d) ~> f) -> p c d -> q e f
pq (Obj c
c Obj c -> Obj c -> (c ** c) ~> (c ** c)
forall (x1 :: j) (x2 :: j) (y1 :: j) (y2 :: j).
(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` Obj c
c') (Obj d
d Obj d -> Obj d -> (d ** d) ~> (d ** d)
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` Obj d
d') p c d
p)
                    (((e ** e) ~> (e ** e))
-> ((f ** f) ~> (f ** f)) -> p' e f -> q' (e ** e) (f ** f)
forall (c :: j) (d :: k) (e :: j) (f :: k).
(e ~> (e ** c)) -> ((f ** d) ~> f) -> p' c d -> q' e f
pq' (Obj e
e Obj e -> Obj e -> (e ** e) ~> (e ** e)
forall (x1 :: j) (x2 :: j) (y1 :: j) (y2 :: j).
(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` Obj e
e') (Obj f
f Obj f -> Obj f -> (f ** f) ~> (f ** 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` Obj f
f') p' e f
p')
                    ((b ** d) ~> f
r ((b ** d) ~> f)
-> (((d ** d) ** (f ** f)) ~> (b ** d))
-> ((d ** d) ** (f ** f)) ~> 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 ** f) ~> b
h ((d ** f) ~> b)
-> ((d ** f) ~> d) -> ((d ** f) ** (d ** f)) ~> (b ** d)
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` (d ** f) ~> d
j) (((d ** f) ** (d ** f)) ~> (b ** d))
-> (((d ** d) ** (f ** f)) ~> ((d ** f) ** (d ** f)))
-> ((d ** d) ** (f ** f)) ~> (b ** 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
. Obj d
-> Obj d
-> Obj f
-> Obj f
-> ((d ** d) ** (f ** f)) ~> ((d ** f) ** (d ** f))
forall k (a :: k) (a' :: k) (b :: k) (b' :: k) (c :: k) (c' :: k)
       (d :: k) (d' :: k).
SymMonoidal k =>
(a ~> a')
-> (b ~> b')
-> (c ~> c')
-> (d ~> d')
-> ((a ** b) ** (c ** d)) ~> ((a' ** c') ** (b' ** d'))
swapInner' Obj d
d Obj d
d' Obj f
f Obj f
f')
      )