module Proarrow.Profunctor.Exponential where

import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), (//))

data (p :~>: q) a b where
  Exp :: (Ob a, Ob b) => (forall c d. c ~> a -> b ~> d -> p c d -> q c d) -> (p :~>: q) a b

instance (Profunctor p, Profunctor q) => Profunctor (p :~>: q) where
  dimap :: forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> (:~>:) p q a b -> (:~>:) p q c d
dimap c ~> a
l b ~> d
r (Exp forall (c :: j) (d :: k). (c ~> a) -> (b ~> d) -> p c d -> q c d
f) = c ~> a
l (c ~> a) -> ((Ob c, Ob a) => (:~>:) p q c d) -> (:~>:) 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) => (:~>:) p q c d) -> (:~>:) 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). (c ~> c) -> (d ~> d) -> p c d -> q c d)
-> (:~>:) p q c d
forall {k} {k} (a :: k) (b :: k) (p :: k -> k -> Type)
       (q :: k -> k -> Type).
(Ob a, Ob b) =>
(forall (c :: k) (d :: k). (c ~> a) -> (b ~> d) -> p c d -> q c d)
-> (:~>:) p q a b
Exp \c ~> c
ca d ~> d
bd p c d
p -> (c ~> a) -> (b ~> d) -> p c d -> q c d
forall (c :: j) (d :: k). (c ~> a) -> (b ~> d) -> p c d -> q c d
f (c ~> a
l (c ~> a) -> (c ~> c) -> c ~> a
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
ca) (d ~> d
bd (d ~> d) -> (b ~> d) -> 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
. b ~> d
r) p c d
p
  (Ob a, Ob b) => r
r \\ :: forall (a :: j) (b :: k) r.
((Ob a, Ob b) => r) -> (:~>:) p q a b -> r
\\ Exp{} = r
(Ob a, Ob b) => r
r