{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Object.Exponential where

import Data.Kind (Type)
import Prelude qualified as P

import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), associator, leftUnitor)
import Proarrow.Category.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Core (CategoryOf (..), PRO, Profunctor (..), Promonad (..), UN, tgt, (//))
import Proarrow.Object (Obj, obj)
import Proarrow.Object.BinaryCoproduct (HasCoproducts)
import Proarrow.Object.BinaryProduct (Cartesian, PROD (..), Prod (..), diag)
import Proarrow.Profunctor.Exponential ((:~>:) (..))
import Proarrow.Profunctor.Product ((:*:) (..))
import Proarrow.Profunctor.Representable (Representable (..), dimapRep)

infixr 2 ~~>

class Ob (a ~~> b) => ObExp' a b
instance Ob (a ~~> b) => ObExp' a b
class (forall (a :: k) b. (Ob a, Ob b) => ObExp' a b) => ObExp k
instance (forall (a :: k) b. (Ob a, Ob b) => ObExp' a b) => ObExp k

class (Monoidal k) => Closed k where
  type (a :: k) ~~> (b :: k) :: k
  curry' :: Obj (a :: k) -> Obj b -> a ** b ~> c -> a ~> b ~~> c
  uncurry' :: Obj (b :: k) -> Obj c -> a ~> b ~~> c -> a ** b ~> c
  (^^^) :: (b :: k) ~> y -> x ~> a -> a ~~> b ~> x ~~> y

curry :: forall {k} (a :: k) b c. (Closed k, Ob a, Ob b) => a ** b ~> c -> a ~> b ~~> c
curry :: forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry = Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
forall k (a :: k) (b :: k) (c :: k).
Closed k =>
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b)

uncurry :: forall {k} (a :: k) b c. (Closed k, Ob b, Ob c) => a ~> b ~~> c -> a ** b ~> c
uncurry :: forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry = Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
forall (b :: k) (c :: k) (a :: k).
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
forall k (b :: k) (c :: k) (a :: k).
Closed k =>
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c)

comp :: forall {k} (a :: k) b c. (Closed k, Ob a, Ob b, Ob c) => (b ~~> c) ** (a ~~> b) ~> a ~~> c
comp :: forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b, Ob c) =>
((b ~~> c) ** (a ~~> b)) ~> (a ~~> c)
comp =
  let a :: Obj a
a = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a; b :: Obj b
b = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b; b2c :: (b ~~> c) ~> (b ~~> c)
b2c = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c Obj c -> Obj b -> (b ~~> c) ~> (b ~~> c)
forall (b :: k) (y :: k) (x :: k) (a :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (b :: k) (y :: k) (x :: k) (a :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ Obj b
b; a2b :: (a ~~> b) ~> (a ~~> b)
a2b = Obj b
b Obj b -> Obj a -> (a ~~> b) ~> (a ~~> b)
forall (b :: k) (y :: k) (x :: k) (a :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (b :: k) (y :: k) (x :: k) (a :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ Obj a
a
  in forall (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @_ @a @c (forall (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
forall {k} (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
eval @b @c (((b ~~> c) ** b) ~> c)
-> ((((b ~~> c) ** (a ~~> b)) ** a) ~> ((b ~~> c) ** b))
-> (((b ~~> c) ** (a ~~> b)) ** a) ~> c
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 ~~> c) ~> (b ~~> c)
b2c ((b ~~> c) ~> (b ~~> c))
-> (((a ~~> b) ** a) ~> b)
-> ((b ~~> c) ** ((a ~~> b) ** a)) ~> ((b ~~> c) ** 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` forall (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
forall {k} (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
eval @a @b) (((b ~~> c) ** ((a ~~> b) ** a)) ~> ((b ~~> c) ** b))
-> ((((b ~~> c) ** (a ~~> b)) ** a)
    ~> ((b ~~> c) ** ((a ~~> b) ** a)))
-> (((b ~~> c) ** (a ~~> b)) ** a) ~> ((b ~~> c) ** 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 k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @(b ~~> c) @(a ~~> b) @a)
      ((Ob (a ~~> b), Ob (a ~~> b)) =>
 ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c))
-> ((a ~~> b) ~> (a ~~> b))
-> ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c)
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
\\ (a ~~> b) ~> (a ~~> b)
a2b
      ((Ob (b ~~> c), Ob (b ~~> c)) =>
 ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c))
-> ((b ~~> c) ~> (b ~~> c))
-> ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c)
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
\\ (b ~~> c) ~> (b ~~> c)
b2c
      ((Ob ((b ~~> c) ** (a ~~> b)), Ob ((b ~~> c) ** (a ~~> b))) =>
 ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c))
-> (((b ~~> c) ** (a ~~> b)) ~> ((b ~~> c) ** (a ~~> b)))
-> ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c)
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
\\ ((b ~~> c) ~> (b ~~> c)
b2c ((b ~~> c) ~> (b ~~> c))
-> ((a ~~> b) ~> (a ~~> b))
-> ((b ~~> c) ** (a ~~> b)) ~> ((b ~~> c) ** (a ~~> 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` (a ~~> b) ~> (a ~~> b)
a2b)

mkExponential :: forall {k} a b. (Closed k) => (a :: k) ~> b -> Unit ~> (a ~~> b)
mkExponential :: forall {k} (a :: k) (b :: k).
Closed k =>
(a ~> b) -> Unit ~> (a ~~> b)
mkExponential a ~> b
ab = forall (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @_ @a (a ~> b
ab (a ~> b) -> ((Unit ** a) ~> a) -> (Unit ** a) ~> 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 ** a) ~> a
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor) ((Ob a, Ob b) => Unit ~> (a ~~> b))
-> (a ~> b) -> Unit ~> (a ~~> b)
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
\\ a ~> b
ab ((Ob Unit, Ob Unit) => Unit ~> (a ~~> b))
-> (Unit ~> Unit) -> Unit ~> (a ~~> b)
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 ~> Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0 :: (Unit :: k) ~> Unit)

lower :: forall {k} (a :: k) b. (Closed k, Ob a, Ob b) => (Unit ~> (a ~~> b)) -> a ~> b
lower :: forall {k} (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
(Unit ~> (a ~~> b)) -> a ~> b
lower Unit ~> (a ~~> b)
f = forall (a :: k) (b :: k) (c :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry @Unit @a @b Unit ~> (a ~~> b)
f ((Unit ** a) ~> b) -> (a ~> (Unit ** a)) -> a ~> 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 ~> (Unit ** a)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv

eval' :: (Closed k) => a ~> a' -> b ~> b' -> ((a' :: k) ~~> b) ** a ~> b'
eval' :: forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
Closed k =>
(a ~> a') -> (b ~> b') -> ((a' ~~> b) ** a) ~> b'
eval' a ~> a'
a b ~> b'
b = let ab :: (a' ~~> b) ~> (a' ~~> b')
ab = b ~> b'
b (b ~> b') -> (a' ~> a') -> (a' ~~> b) ~> (a' ~~> b')
forall (b :: k) (y :: k) (x :: k) (a :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (b :: k) (y :: k) (x :: k) (a :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ (a ~> a') -> a' ~> a'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt a ~> a'
a in (a' ~> a')
-> Obj b'
-> ((a' ~~> b') ~> (a' ~~> b'))
-> ((a' ~~> b') ** a') ~> b'
forall (b :: k) (c :: k) (a :: k).
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
forall k (b :: k) (c :: k) (a :: k).
Closed k =>
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' ((a ~> a') -> a' ~> a'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt a ~> a'
a) ((b ~> b') -> Obj b'
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt b ~> b'
b) (((a' ~~> b) ~> (a' ~~> b')) -> (a' ~~> b') ~> (a' ~~> b')
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt (a' ~~> b) ~> (a' ~~> b')
ab) (((a' ~~> b') ** a') ~> b')
-> (((a' ~~> b) ** a) ~> ((a' ~~> b') ** a'))
-> ((a' ~~> b) ** a) ~> 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' ~~> b) ~> (a' ~~> b')
ab ((a' ~~> b) ~> (a' ~~> b'))
-> (a ~> a') -> ((a' ~~> b) ** a) ~> ((a' ~~> b') ** a')
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 ~> a'
a)

eval :: forall {k} a b. (Closed k, Ob a, Ob b) => ((a :: k) ~~> b) ** a ~> b
eval :: forall {k} (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
eval = (a ~> a) -> (b ~> b) -> ((a ~~> b) ** a) ~> b
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
Closed k =>
(a ~> a') -> (b ~> b') -> ((a' ~~> b) ** a) ~> b'
eval' (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b)

instance Closed Type where
  type a ~~> b = a -> b
  curry' :: forall a b c. Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' Obj a
_ Obj b
_ = ((a ** b) ~> c) -> a ~> (b ~~> c)
((a, b) -> c) -> a -> b -> c
forall a b c. ((a, b) -> c) -> a -> b -> c
P.curry
  uncurry' :: forall b c a. Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' Obj b
_ Obj c
_ = (a ~> (b ~~> c)) -> (a ** b) ~> c
(a -> b -> c) -> (a, b) -> c
forall a b c. (a -> b -> c) -> (a, b) -> c
P.uncurry
  ^^^ :: forall b y x a. (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
(^^^) = ((x -> a) -> (b -> y) -> (a -> b) -> x -> y)
-> (b -> y) -> (x -> a) -> (a -> b) -> x -> y
forall a b c. (a -> b -> c) -> b -> a -> c
P.flip (x ~> a) -> (b ~> y) -> (a -> b) -> x -> y
(x -> a) -> (b -> y) -> (a -> b) -> x -> y
forall c a b d. (c ~> a) -> (b ~> d) -> (a -> b) -> 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

instance Closed () where
  type '() ~~> '() = '()
  curry' :: forall (a :: ()) (b :: ()) (c :: ()).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' Obj a
Unit a a
U.Unit Obj b
Unit b b
U.Unit (a ** b) ~> c
Unit '() c
U.Unit = a ~> (b ~~> c)
Unit '() '()
U.Unit
  uncurry' :: forall (b :: ()) (c :: ()) (a :: ()).
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' Obj b
Unit b b
U.Unit Obj c
Unit c c
U.Unit a ~> (b ~~> c)
Unit a '()
U.Unit = (a ** b) ~> c
Unit '() '()
U.Unit
  b ~> y
Unit b y
U.Unit ^^^ :: forall (b :: ()) (y :: ()) (x :: ()) (a :: ()).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ x ~> a
Unit x a
U.Unit = (a ~~> b) ~> (x ~~> y)
Unit '() '()
U.Unit

instance (CategoryOf j, CategoryOf k) => Closed (PROD (PRO j k)) where
  type p ~~> q = PR (UN PR p :~>: UN PR q)
  curry' :: forall (a :: PROD (PRO j k)) (b :: PROD (PRO j k))
       (c :: PROD (PRO j k)).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' (Prod Prof{}) (Prod Prof{}) (Prod (Prof (b1 :*: b1) :~> b1
n)) = Prof b1 (b1 :~>: b1) -> Prod Prof ('PR b1) ('PR (b1 :~>: b1))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod ((b1 :~> (b1 :~>: b1)) -> Prof b1 (b1 :~>: b1)
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \b1 a b
p -> b1 a b
p b1 a b -> ((Ob a, Ob b) => (:~>:) b1 b1 a b) -> (:~>:) b1 b1 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).
 (c ~> a) -> (b ~> d) -> b1 c d -> b1 c d)
-> (:~>:) b1 b1 a b
forall {k} {k1} (a :: k) (b :: k1) (p :: k -> k1 -> Type)
       (q :: k -> k1 -> Type).
(Ob a, Ob b) =>
(forall (c :: k) (d :: k1). (c ~> a) -> (b ~> d) -> p c d -> q c d)
-> (:~>:) p q a b
Exp \c ~> a
ca b ~> d
bd b1 c d
q -> (:*:) b1 b1 c d -> b1 c d
(b1 :*: b1) :~> b1
n ((c ~> a) -> (b ~> d) -> b1 a b -> b1 c d
forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> b1 a b -> b1 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 ~> a
ca b ~> d
bd b1 a b
p b1 c d -> b1 c d -> (:*:) b1 b1 c d
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) (q :: PRO j k).
p a b -> q a b -> (:*:) p q a b
:*: b1 c d
q))
  uncurry' :: forall (b :: PROD (PRO j k)) (c :: PROD (PRO j k))
       (a :: PROD (PRO j k)).
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' (Prod Prof{}) (Prod Prof{}) (Prod (Prof a1 :~> (b1 :~>: b1)
n)) = Prof (a1 :*: b1) b1 -> Prod Prof ('PR (a1 :*: b1)) ('PR b1)
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod (((a1 :*: b1) :~> b1) -> Prof (a1 :*: b1) b1
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(a1 a b
p :*: b1 a b
q) -> case a1 a b -> (:~>:) b1 b1 a b
a1 :~> (b1 :~>: b1)
n a1 a b
p of Exp forall (c :: j) (d :: k). (c ~> a) -> (b ~> d) -> b1 c d -> b1 c d
f -> (a ~> a) -> (b ~> b) -> b1 a b -> b1 a b
forall (c :: j) (d :: k). (c ~> a) -> (b ~> d) -> b1 c d -> b1 c d
f a ~> a
forall (a :: j). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: k). Ob a => a ~> a
forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a
id b1 a b
q ((Ob a, Ob b) => b1 a b) -> b1 a b -> b1 a b
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> b1 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
\\ b1 a b
q)
  Prod (Prof a1 :~> b1
m) ^^^ :: forall (b :: PROD (PRO j k)) (y :: PROD (PRO j k))
       (x :: PROD (PRO j k)) (a :: PROD (PRO j k)).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ Prod (Prof a1 :~> b1
n) = Prof (b1 :~>: a1) (a1 :~>: b1)
-> Prod Prof ('PR (b1 :~>: a1)) ('PR (a1 :~>: b1))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p ('PR a1) ('PR b1)
Prod (((b1 :~>: a1) :~> (a1 :~>: b1)) -> Prof (b1 :~>: a1) (a1 :~>: b1)
forall {k} {j} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Exp forall (c :: j) (d :: k). (c ~> a) -> (b ~> d) -> b1 c d -> a1 c d
f) -> (forall (c :: j) (d :: k).
 (c ~> a) -> (b ~> d) -> a1 c d -> b1 c d)
-> (:~>:) a1 b1 a b
forall {k} {k1} (a :: k) (b :: k1) (p :: k -> k1 -> Type)
       (q :: k -> k1 -> Type).
(Ob a, Ob b) =>
(forall (c :: k) (d :: k1). (c ~> a) -> (b ~> d) -> p c d -> q c d)
-> (:~>:) p q a b
Exp \c ~> a
ca b ~> d
bd a1 c d
p -> a1 c d -> b1 c d
a1 :~> b1
m ((c ~> a) -> (b ~> d) -> b1 c d -> a1 c d
forall (c :: j) (d :: k). (c ~> a) -> (b ~> d) -> b1 c d -> a1 c d
f c ~> a
ca b ~> d
bd (a1 c d -> b1 c d
a1 :~> b1
n a1 c d
p)))

instance (Closed j, Closed k) => Closed (j, k) where
  type '(a1, a2) ~~> '(b1, b2) = '(a1 ~~> b1, a2 ~~> b2)
  curry' :: forall (a :: (j, k)) (b :: (j, k)) (c :: (j, k)).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' (a1 ~> b1
a1 :**: a2 ~> b2
a2) (a1 ~> b1
b1 :**: a2 ~> b2
b2) (a1 ~> b1
f1 :**: a2 ~> b2
f2) = Obj b1 -> Obj b1 -> ((b1 ** b1) ~> b1) -> b1 ~> (b1 ~~> b1)
forall (a :: j) (b :: j) (c :: j).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
forall k (a :: k) (b :: k) (c :: k).
Closed k =>
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' a1 ~> b1
Obj b1
a1 a1 ~> b1
Obj b1
b1 a1 ~> b1
(b1 ** b1) ~> b1
f1 (b1 ~> (b1 ~~> b1))
-> (b2 ~> (b2 ~~> b2))
-> (:**:) (~>) (~>) '(b1, b2) '(b1 ~~> b1, b2 ~~> b2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: Obj b2 -> Obj b2 -> ((b2 ** b2) ~> b2) -> b2 ~> (b2 ~~> b2)
forall (a :: k) (b :: k) (c :: k).
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
forall k (a :: k) (b :: k) (c :: k).
Closed k =>
Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c)
curry' a2 ~> b2
Obj b2
a2 a2 ~> b2
Obj b2
b2 a2 ~> b2
(b2 ** b2) ~> b2
f2
  uncurry' :: forall (b :: (j, k)) (c :: (j, k)) (a :: (j, k)).
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' (a1 ~> b1
a1 :**: a2 ~> b2
a2) (a1 ~> b1
b1 :**: a2 ~> b2
b2) (a1 ~> b1
f1 :**: a2 ~> b2
f2) = Obj b1 -> Obj b1 -> (a1 ~> (b1 ~~> b1)) -> (a1 ** b1) ~> b1
forall (b :: j) (c :: j) (a :: j).
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
forall k (b :: k) (c :: k) (a :: k).
Closed k =>
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' a1 ~> b1
Obj b1
a1 a1 ~> b1
Obj b1
b1 a1 ~> b1
a1 ~> (b1 ~~> b1)
f1 ((a1 ** b1) ~> b1)
-> ((a2 ** b2) ~> b2)
-> (:**:) (~>) (~>) '(a1 ** b1, a2 ** b2) '(b1, b2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: Obj b2 -> Obj b2 -> (a2 ~> (b2 ~~> b2)) -> (a2 ** b2) ~> b2
forall (b :: k) (c :: k) (a :: k).
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
forall k (b :: k) (c :: k) (a :: k).
Closed k =>
Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry' a2 ~> b2
Obj b2
a2 a2 ~> b2
Obj b2
b2 a2 ~> b2
a2 ~> (b2 ~~> b2)
f2
  (a1 ~> b1
f1 :**: a2 ~> b2
f2) ^^^ :: forall (b :: (j, k)) (y :: (j, k)) (x :: (j, k)) (a :: (j, k)).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ (a1 ~> b1
g1 :**: a2 ~> b2
g2) = (a1 ~> b1
f1 (a1 ~> b1) -> (a1 ~> b1) -> (b1 ~~> a1) ~> (a1 ~~> b1)
forall (b :: j) (y :: j) (x :: j) (a :: j).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (b :: k) (y :: k) (x :: k) (a :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ a1 ~> b1
g1) ((b1 ~~> a1) ~> (a1 ~~> b1))
-> ((b2 ~~> a2) ~> (a2 ~~> b2))
-> (:**:) (~>) (~>) '(b1 ~~> a1, b2 ~~> a2) '(a1 ~~> b1, a2 ~~> b2)
forall {j1} {k1} {j2} {k2} (c :: j1 +-> k1) (a1 :: k1) (b1 :: j1)
       (d :: j2 +-> k2) (a2 :: k2) (b2 :: j2).
c a1 b1 -> d a2 b2 -> (:**:) c d '(a1, a2) '(b1, b2)
:**: (a2 ~> b2
f2 (a2 ~> b2) -> (a2 ~> b2) -> (b2 ~~> a2) ~> (a2 ~~> b2)
forall (b :: k) (y :: k) (x :: k) (a :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (b :: k) (y :: k) (x :: k) (a :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ a2 ~> b2
g2)

type ExponentialFunctor :: PRO k (OPPOSITE k, k)
data ExponentialFunctor a b where
  ExponentialFunctor :: (Ob c, Ob d) => a ~> (c ~~> d) -> ExponentialFunctor a '(OP c, d)

instance (Closed k) => Profunctor (ExponentialFunctor :: PRO k (OPPOSITE k, k)) where
  dimap :: forall (c :: k) (a :: k) (b :: (OPPOSITE k, k))
       (d :: (OPPOSITE k, k)).
(c ~> a)
-> (b ~> d) -> ExponentialFunctor a b -> ExponentialFunctor c d
dimap = (c ~> a)
-> (b ~> d) -> ExponentialFunctor a b -> ExponentialFunctor c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (c :: k) (d :: j).
Representable p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimapRep
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: (OPPOSITE k, k)) r.
((Ob a, Ob b) => r) -> ExponentialFunctor a b -> r
\\ ExponentialFunctor a ~> (c ~~> d)
f = r
(Ob a, Ob (c ~~> d)) => r
(Ob a, Ob b) => r
r ((Ob a, Ob (c ~~> d)) => r) -> (a ~> (c ~~> d)) -> 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
\\ a ~> (c ~~> d)
f

instance (Closed k) => Representable (ExponentialFunctor :: PRO k (OPPOSITE k, k)) where
  type ExponentialFunctor % '(OP a, b) = a ~~> b
  index :: forall (a :: k) (b :: (OPPOSITE k, k)).
ExponentialFunctor a b -> a ~> (ExponentialFunctor % b)
index (ExponentialFunctor a ~> (c ~~> d)
f) = a ~> (ExponentialFunctor % b)
a ~> (c ~~> d)
f
  tabulate :: forall (b :: (OPPOSITE k, k)) (a :: k).
Ob b =>
(a ~> (ExponentialFunctor % b)) -> ExponentialFunctor a b
tabulate = (a ~> (ExponentialFunctor % b)) -> ExponentialFunctor a b
(a ~> (UN 'OP (Fst b) ~~> Snd b))
-> ExponentialFunctor a '( 'OP (UN 'OP (Fst b)), Snd b)
forall {k} (c :: k) (d :: k) (a :: k).
(Ob c, Ob d) =>
(a ~> (c ~~> d)) -> ExponentialFunctor a '( 'OP c, d)
ExponentialFunctor
  repMap :: forall (a :: (OPPOSITE k, k)) (b :: (OPPOSITE k, k)).
(a ~> b) -> (ExponentialFunctor % a) ~> (ExponentialFunctor % b)
repMap (Op b1 ~> a1
f :**: a2 ~> b2
g) = a2 ~> b2
g (a2 ~> b2) -> (b1 ~> a1) -> (a1 ~~> a2) ~> (b1 ~~> b2)
forall (b :: k) (y :: k) (x :: k) (a :: k).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
forall k (b :: k) (y :: k) (x :: k) (a :: k).
Closed k =>
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ b1 ~> a1
f

class (Cartesian k, Closed k) => CCC k
instance (Cartesian k, Closed k) => CCC k

class (CCC k, HasCoproducts k) => BiCCC k
instance (CCC k, HasCoproducts k) => BiCCC k

ap
  :: forall {j} {k} y a x p
   . (Cartesian j, Closed k, MonoidalProfunctor (p :: PRO j k), Ob y)
  => p a (x ~~> y)
  -> p a x
  -> p a y
ap :: forall {j} {k} (y :: k) (a :: j) (x :: k) (p :: PRO j k).
(Cartesian j, Closed k, MonoidalProfunctor p, Ob y) =>
p a (x ~~> y) -> p a x -> p a y
ap p a (x ~~> y)
pf p a x
px = (a ~> (a && a))
-> (((x ~~> y) ** x) ~> y) -> p (a && a) ((x ~~> y) ** x) -> p a y
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 ~> (a && a)
forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
diag ((x ~> x) -> (y ~> y) -> ((x ~~> y) ** x) ~> y
forall k (a :: k) (a' :: k) (b :: k) (b' :: k).
Closed k =>
(a ~> a') -> (b ~> b') -> ((a' ~~> b) ** a) ~> b'
eval' (p a x -> x ~> x
forall {k1} {k2} (a :: k2) (b :: k1) (p :: PRO k2 k1).
Profunctor p =>
p a b -> Obj b
tgt p a x
px) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @y)) (p a (x ~~> y)
pf p a (x ~~> y) -> p a x -> p (a ** a) ((x ~~> y) ** x)
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 a x
px) ((Ob a, Ob (x ~~> y)) => p a y) -> p a (x ~~> y) -> p a y
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> p 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
\\ p a (x ~~> y)
pf