{-# 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, (//)) 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 (Monoidal k) => Closed k where type (a :: k) ~~> (b :: k) :: k withObExp :: (Ob (a :: k), Ob b) => ((Ob (a ~~> b)) => r) -> r curry :: (Ob (a :: k), Ob b) => a ** b ~> c -> a ~> b ~~> c uncurry :: (Ob (b :: k), Ob c) => a ~> b ~~> c -> a ** b ~> c (^^^) :: forall (a :: k) b x y. b ~> y -> x ~> a -> a ~~> b ~> x ~~> y b ~> y f ^^^ x ~> a g = b ~> y f (b ~> y) -> ((Ob b, Ob y) => (a ~~> b) ~> (x ~~> y)) -> (a ~~> b) ~> (x ~~> y) forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r. Profunctor p => p a b -> ((Ob a, Ob b) => r) -> r // x ~> a g (x ~> a) -> ((Ob x, Ob a) => (a ~~> b) ~> (x ~~> y)) -> (a ~~> b) ~> (x ~~> y) forall {k1} {k2} (p :: PRO k1 k2) (a :: k1) (b :: k2) r. Profunctor p => p a b -> ((Ob a, Ob b) => r) -> r // forall k (a :: k) (b :: k) r. (Closed k, Ob a, Ob b) => (Ob (a ~~> b) => r) -> r withObExp @k @a @b ((Ob (a ~~> b) => (a ~~> b) ~> (x ~~> y)) -> (a ~~> b) ~> (x ~~> y)) -> (Ob (a ~~> b) => (a ~~> b) ~> (x ~~> y)) -> (a ~~> b) ~> (x ~~> y) forall a b. (a -> b) -> a -> b P.$ let ab :: Obj (a ~~> b) ab = forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @(a ~~> b) in forall k (a :: k) (b :: k) (c :: k). (Closed k, Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) curry @k @(a ~~> b) @x (b ~> y f (b ~> y) -> (((a ~~> b) ** x) ~> b) -> ((a ~~> b) ** x) ~> y 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 (b :: k) (c :: k) (a :: k). (Closed k, Ob b, Ob c) => (a ~> (b ~~> c)) -> (a ** b) ~> c uncurry @_ @a @b Obj (a ~~> b) ab (((a ~~> b) ** a) ~> b) -> (((a ~~> b) ** x) ~> ((a ~~> b) ** a)) -> ((a ~~> b) ** x) ~> 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 . (Obj (a ~~> b) ab Obj (a ~~> b) -> (x ~> a) -> ((a ~~> b) ** x) ~> ((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` x ~> a g)) curry' :: forall {k} a b c. (Closed k) => Obj (a :: k) -> Obj b -> a ** b ~> c -> a ~> b ~~> c curry' :: forall {k} (a :: k) (b :: k) (c :: k). Closed k => Obj a -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> c) curry' Obj a a Obj b b = forall k (a :: k) (b :: k) (c :: k). (Closed k, Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) curry @k @a @b ((Ob a, Ob a) => ((a ** b) ~> c) -> a ~> (b ~~> c)) -> Obj a -> ((a ** b) ~> c) -> a ~> (b ~~> 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 \\ Obj a a ((Ob b, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c)) -> Obj b -> ((a ** b) ~> c) -> a ~> (b ~~> 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 \\ Obj b b uncurry' :: forall {k} b c a. (Closed k) => Obj (b :: k) -> Obj c -> a ~> b ~~> c -> a ** b ~> c uncurry' :: forall {k} (b :: k) (c :: k) (a :: k). Closed k => Obj b -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> c uncurry' Obj b b Obj c c = forall k (b :: k) (c :: k) (a :: k). (Closed k, Ob b, Ob c) => (a ~> (b ~~> c)) -> (a ** b) ~> c uncurry @k @b @c ((Ob b, Ob b) => (a ~> (b ~~> c)) -> (a ** b) ~> c) -> Obj b -> (a ~> (b ~~> c)) -> (a ** b) ~> 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 \\ Obj b b ((Ob c, Ob c) => (a ~> (b ~~> c)) -> (a ** b) ~> c) -> Obj c -> (a ~> (b ~~> c)) -> (a ** b) ~> 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 \\ Obj c 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 = forall k (a :: k) (b :: k) r. (Closed k, Ob a, Ob b) => (Ob (a ~~> b) => r) -> r withObExp @k @b @c ((Ob (b ~~> c) => ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c)) -> ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c)) -> (Ob (b ~~> c) => ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c)) -> ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c) forall a b. (a -> b) -> a -> b P.$ forall k (a :: k) (b :: k) r. (Closed k, Ob a, Ob b) => (Ob (a ~~> b) => r) -> r withObExp @k @a @b ((Ob (a ~~> b) => ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c)) -> ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c)) -> (Ob (a ~~> b) => ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c)) -> ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c) forall a b. (a -> b) -> a -> b P.$ forall k (a :: k) (b :: k) r. (Monoidal k, Ob a, Ob b) => (Ob (a ** b) => r) -> r withOb2 @k @(b ~~> c) @(a ~~> b) ((Ob ((b ~~> c) ** (a ~~> b)) => ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c)) -> ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c)) -> (Ob ((b ~~> c) ** (a ~~> b)) => ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c)) -> ((b ~~> c) ** (a ~~> b)) ~> (a ~~> c) forall a b. (a -> b) -> a -> b P.$ forall k (a :: k) (b :: k) (c :: k). (Closed k, Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) curry @_ @_ @a (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 . (forall (a :: k). (CategoryOf k, Ob a) => Obj a forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a obj @(b ~~> c) Obj (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) 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 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 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 k (b :: k) (c :: k) (a :: k). (Closed k, Ob b, Ob c) => (a ~> (b ~~> c)) -> (a ** b) ~> c uncurry @k @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 :: 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 = forall k (a :: k) (b :: k) r. (Closed k, Ob a, Ob b) => (Ob (a ~~> b) => r) -> r withObExp @k @a @b (forall k (b :: k) (c :: k) (a :: k). (Closed k, Ob b, Ob c) => (a ~> (b ~~> c)) -> (a ** b) ~> c uncurry @k @a @b @(a ~~> b) (a ~~> b) ~> (a ~~> b) forall (a :: k). Ob a => a ~> a forall {k} (p :: PRO k k) (a :: k). (Promonad p, Ob a) => p a a id) instance Closed Type where type a ~~> b = a -> b withObExp :: forall a b r. (Ob a, Ob b) => (Ob (a ~~> b) => r) -> r withObExp Ob (a ~~> b) => r r = r Ob (a ~~> b) => r r curry :: forall a b c. (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) curry = ((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. (Ob b, Ob c) => (a ~> (b ~~> c)) -> (a ** b) ~> c uncurry = (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 a b x y. (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 '() ~~> '() = '() withObExp :: forall (a :: ()) (b :: ()) r. (Ob a, Ob b) => (Ob (a ~~> b) => r) -> r withObExp Ob (a ~~> b) => r r = r Ob (a ~~> b) => r r curry :: forall (a :: ()) (b :: ()) (c :: ()). (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) curry (a ** b) ~> c Unit '() c U.Unit = a ~> (b ~~> c) Unit '() '() U.Unit uncurry :: forall (b :: ()) (c :: ()) (a :: ()). (Ob b, Ob c) => (a ~> (b ~~> c)) -> (a ** b) ~> c uncurry a ~> (b ~~> c) Unit a '() U.Unit = (a ** b) ~> c Unit '() '() U.Unit b ~> y Unit b y U.Unit ^^^ :: forall (a :: ()) (b :: ()) (x :: ()) (y :: ()). (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) withObExp :: forall (a :: PROD (PRO j k)) (b :: PROD (PRO j k)) r. (Ob a, Ob b) => (Ob (a ~~> b) => r) -> r withObExp Ob (a ~~> b) => r r = r Ob (a ~~> b) => r r curry :: forall (a :: PROD (PRO j k)) (b :: PROD (PRO j k)) (c :: PROD (PRO j k)). (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) curry (Prod (Prof (UN 'PR a :*: UN 'PR b) :~> b1 n)) = Prof (UN 'PR a) (UN 'PR b :~>: b1) -> Prod Prof ('PR (UN 'PR a)) ('PR (UN 'PR b :~>: b1)) forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j). p a1 b1 -> Prod p ('PR a1) ('PR b1) Prod ((UN 'PR a :~> (UN 'PR b :~>: b1)) -> Prof (UN 'PR a) (UN 'PR b :~>: b1) forall {k} {j} (p :: j +-> k) (q :: j +-> k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \UN 'PR a a b p -> UN 'PR a a b p UN 'PR a a b -> ((Ob a, Ob b) => (:~>:) (UN 'PR b) b1 a b) -> (:~>:) (UN 'PR b) 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) -> UN 'PR b c d -> b1 c d) -> (:~>:) (UN 'PR b) 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 UN 'PR b c d q -> (:*:) (UN 'PR a) (UN 'PR b) c d -> b1 c d (UN 'PR a :*: UN 'PR b) :~> b1 n ((c ~> a) -> (b ~> d) -> UN 'PR a a b -> UN 'PR a c d forall (c :: j) (a :: j) (b :: k) (d :: k). (c ~> a) -> (b ~> d) -> UN 'PR a a b -> UN 'PR 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 ~> a ca b ~> d bd UN 'PR a a b p UN 'PR a c d -> UN 'PR b c d -> (:*:) (UN 'PR a) (UN 'PR b) 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 :*: UN 'PR b c d q)) uncurry :: forall (b :: PROD (PRO j k)) (c :: PROD (PRO j k)) (a :: PROD (PRO j k)). (Ob b, Ob c) => (a ~> (b ~~> c)) -> (a ** b) ~> c uncurry (Prod (Prof a1 :~> (UN 'PR b :~>: UN 'PR c) n)) = Prof (a1 :*: UN 'PR b) (UN 'PR c) -> Prod Prof ('PR (a1 :*: UN 'PR b)) ('PR (UN 'PR c)) forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j). p a1 b1 -> Prod p ('PR a1) ('PR b1) Prod (((a1 :*: UN 'PR b) :~> UN 'PR c) -> Prof (a1 :*: UN 'PR b) (UN 'PR c) forall {k} {j} (p :: j +-> k) (q :: j +-> k). (Profunctor p, Profunctor q) => (p :~> q) -> Prof p q Prof \(a1 a b p :*: UN 'PR b a b q) -> case a1 a b -> (:~>:) (UN 'PR b) (UN 'PR c) a b a1 :~> (UN 'PR b :~>: UN 'PR c) n a1 a b p of Exp forall (c :: j) (d :: k). (c ~> a) -> (b ~> d) -> UN 'PR b c d -> UN 'PR c c d f -> (a ~> a) -> (b ~> b) -> UN 'PR b a b -> UN 'PR c a b forall (c :: j) (d :: k). (c ~> a) -> (b ~> d) -> UN 'PR b c d -> UN 'PR c 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 UN 'PR b a b q ((Ob a, Ob b) => UN 'PR c a b) -> UN 'PR b a b -> UN 'PR c a b forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> UN 'PR 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 \\ UN 'PR b a b q) Prod (Prof a1 :~> b1 m) ^^^ :: forall (a :: PROD (PRO j k)) (b :: PROD (PRO j k)) (x :: PROD (PRO j k)) (y :: 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) withObExp :: forall (a :: (j, k)) (b :: (j, k)) r. (Ob a, Ob b) => (Ob (a ~~> b) => r) -> r withObExp @'(a1, a2) @'(b1, b2) Ob (a ~~> b) => r r = forall k (a :: k) (b :: k) r. (Closed k, Ob a, Ob b) => (Ob (a ~~> b) => r) -> r withObExp @j @a1 @b1 (forall k (a :: k) (b :: k) r. (Closed k, Ob a, Ob b) => (Ob (a ~~> b) => r) -> r withObExp @k @a2 @b2 r Ob (Snd a ~~> Snd b) => r Ob (a ~~> b) => r r) curry :: forall (a :: (j, k)) (b :: (j, k)) (c :: (j, k)). (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) curry @'(a1, a2) @'(b1, b2) (a1 ~> b1 f1 :**: a2 ~> b2 f2) = forall k (a :: k) (b :: k) (c :: k). (Closed k, Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) curry @j @a1 @b1 a1 ~> b1 (Fst a ** Fst b) ~> b1 f1 (Fst a ~> (Fst b ~~> b1)) -> (Snd a ~> (Snd b ~~> b2)) -> (:**:) (~>) (~>) '(Fst a, Snd a) '(Fst b ~~> b1, Snd b ~~> 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) :**: forall k (a :: k) (b :: k) (c :: k). (Closed k, Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) curry @k @a2 @b2 a2 ~> b2 (Snd a ** Snd b) ~> b2 f2 uncurry :: forall (b :: (j, k)) (c :: (j, k)) (a :: (j, k)). (Ob b, Ob c) => (a ~> (b ~~> c)) -> (a ** b) ~> c uncurry @'(a1, a2) @'(b1, b2) (a1 ~> b1 f1 :**: a2 ~> b2 f2) = forall k (b :: k) (c :: k) (a :: k). (Closed k, Ob b, Ob c) => (a ~> (b ~~> c)) -> (a ** b) ~> c uncurry @j @a1 @b1 a1 ~> b1 a1 ~> (Fst b ~~> Fst c) f1 ((a1 ** Fst b) ~> Fst c) -> ((a2 ** Snd b) ~> Snd c) -> (:**:) (~>) (~>) '(a1 ** Fst b, a2 ** Snd b) '(Fst c, Snd c) 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) :**: forall k (b :: k) (c :: k) (a :: k). (Closed k, Ob b, Ob c) => (a ~> (b ~~> c)) -> (a ** b) ~> c uncurry @k @a2 @b2 a2 ~> b2 a2 ~> (Snd b ~~> Snd c) f2 (a1 ~> b1 f1 :**: a2 ~> b2 f2) ^^^ :: forall (a :: (j, k)) (b :: (j, k)) (x :: (j, k)) (y :: (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 (a :: j) (b :: j) (x :: j) (y :: j). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) forall k (a :: k) (b :: k) (x :: k) (y :: 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 (a :: k) (b :: k) (x :: k) (y :: k). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) forall k (a :: k) (b :: k) (x :: k) (y :: 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 (a :: k) (b :: k) (x :: k) (y :: k). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) forall k (a :: k) (b :: k) (x :: k) (y :: 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 (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 @x @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) => p a y) -> p a x -> 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 px