{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Object.Exponential where

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

import Proarrow.Category.Instance.Free
  ( Elem
  , FREE (..)
  , Free (..)
  , HasStructure (..)
  , IsFreeOb (..)
  , Ok
  , WithEq
  , WithShow
  )
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), associator, leftUnitor, type (**!))
import Proarrow.Category.Opposite (OPPOSITE (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), obj, (//), type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Object.BinaryCoproduct (HasCoproducts)
import Proarrow.Object.BinaryProduct (Cartesian, diag)
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Profunctor.Representable (Rep (..))

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
  apply :: (Ob (a :: k), Ob b) => (a ~~> b) ** a ~> b
  (^^^) :: 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 :: k1 +-> k2) (a :: k2) (b :: k1) 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 :: k1 +-> k2) (a :: k2) (b :: k1) 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 :: 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).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @a @b (((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 :: 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))

uncurry :: forall {k} b c (a :: k). (Closed k) => (Ob b, Ob c) => a ~> b ~~> c -> a ** b ~> c
uncurry :: forall {k} (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry a ~> (b ~~> c)
f = forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @b @c (((b ~~> c) ** b) ~> c)
-> ((a ** b) ~> ((b ~~> c) ** b)) -> (a ** b) ~> c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ~> (b ~~> c)
f (a ~> (b ~~> c)) -> (b ~> b) -> (a ** b) ~> ((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). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b)

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 k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @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 :: 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 k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @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 :: 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 :: 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 :: j +-> k) (a :: k) (b :: j) 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 (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
forall {k} (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry @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 :: 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

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
  apply :: forall a b. (Ob a, Ob b) => ((a ~~> b) ** a) ~> b
apply = ((a -> b) -> a -> b) -> (a -> b, a) -> b
forall a b c. (a -> b -> c) -> (a, b) -> c
P.uncurry (a -> b) -> a -> b
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  ^^^ :: 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 :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
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
  apply :: forall (a :: ()) (b :: ()). (Ob a, Ob b) => ((a ~~> b) ** a) ~> b
apply = ((a ~~> b) ** a) ~> b
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 (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
  apply :: forall (a :: (j, k)) (b :: (j, k)).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @'(a1, a2) @'(b1, b2) = forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @j @a1 @b1 (((Fst a ~~> Fst b) ** Fst a) ~> Fst b)
-> (((Snd a ~~> Snd b) ** Snd a) ~> Snd b)
-> (:**:)
     (~>)
     (~>)
     '((Fst a ~~> Fst b) ** Fst a, (Snd a ~~> Snd b) ** Snd a)
     '(Fst b, Snd b)
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).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @a2 @b2
  (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)

data family Exponential :: OPPOSITE k -> k +-> k
instance (Closed k, Ob (a :: k)) => FunctorForRep (Exponential (OP a)) where
  type Exponential (OP a) @ b = a ~~> b
  fmap :: forall (a :: k) (b :: k).
(a ~> b) -> (Exponential ('OP a) @ a) ~> (Exponential ('OP a) @ b)
fmap a ~> b
f = a ~> b
f (a ~> b) -> (a ~> a) -> (a ~~> a) ~> (a ~~> b)
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)
^^^ forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a

-- | The curry/uncurry adjunction.
instance (Closed k, Ob (a :: k)) => Corepresentable (Rep (Exponential (OP a))) where
  type Rep (Exponential (OP a)) %% b = b ** a
  coindex :: forall (a :: k) (b :: k).
Rep (Exponential ('OP a)) a b
-> (Rep (Exponential ('OP a)) %% a) ~> b
coindex (Rep a ~> (Exponential ('OP a) @ b)
f) = forall (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
forall {k} (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> (a ** b) ~> c
uncurry @a a ~> (Exponential ('OP a) @ b)
a ~> (a ~~> b)
f
  cotabulate :: forall (a :: k) (b :: k).
Ob a =>
((Rep (Exponential ('OP a)) %% a) ~> b)
-> Rep (Exponential ('OP a)) a b
cotabulate @c (Rep (Exponential ('OP a)) %% a) ~> b
f = (a ~> (Exponential ('OP a) @ b)) -> Rep (Exponential ('OP a)) a b
forall {j} {k} (f :: j +-> k) (a :: k) (b :: j).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @c @a (Rep (Exponential ('OP a)) %% a) ~> b
(a ** a) ~> b
f) ((Ob (a ** a), Ob b) => Rep (Exponential ('OP a)) a b)
-> ((a ** a) ~> b) -> Rep (Exponential ('OP a)) a b
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ (Rep (Exponential ('OP a)) %% a) ~> b
(a ** a) ~> b
f
  corepMap :: forall (a :: k) (b :: k).
(a ~> b)
-> (Rep (Exponential ('OP a)) %% a)
   ~> (Rep (Exponential ('OP a)) %% b)
corepMap a ~> b
f = a ~> b
f (a ~> b) -> (a ~> a) -> (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` forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a

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
   . (Closed j, Cartesian k, MonoidalProfunctor (p :: j +-> k), Ob y)
  => p a (x ~~> y)
  -> p a x
  -> p a y
ap :: forall {j} {k} (y :: j) (a :: k) (x :: j) (p :: j +-> k).
(Closed j, Cartesian 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 :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
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 k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @j @x @y) (p a (x ~~> y)
pf p a (x ~~> y) -> p a x -> p (a ** a) ((x ~~> y) ** x)
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 a x
px) ((Ob a, Ob x) => p a y) -> p a x -> p a y
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a x
px

data family (-->) (a :: k) (b :: k) :: k
instance (Ob (a :: FREE cs p), Ob b, Closed `Elem` cs, Monoidal `Elem` cs) => IsFreeOb (a --> b) where
  type Lower f (a --> b) = Lower f a ~~> Lower f b
  withLowerOb :: forall {k} (f :: j +-> k) r.
(Representable f, All cs k) =>
(Ob (Lower f (a --> b)) => r) -> r
withLowerOb @f Ob (Lower f (a --> b)) => r
r = forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @a @f (forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @b @f (forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @_ @(Lower f a) @(Lower f b) r
Ob (Lower f (a --> b)) => r
Ob (Lower f a ~~> Lower f b) => r
r))
instance (Closed `Elem` cs, Monoidal `Elem` cs) => HasStructure cs p Closed where
  data Struct Closed a b where
    Apply :: (Ob a, Ob b) => Struct Closed ((a --> b) **! a) b
    Curry :: forall a b c. (Ob a, Ob b) => (a **! b) ~> c -> Struct Closed a (b --> c)
  foldStructure :: forall {k} (f :: j +-> k) (a :: FREE cs p) (b :: FREE cs p).
(All cs k, Representable f) =>
(forall (x :: FREE cs p) (y :: FREE cs p).
 (x ~> y) -> Lower f x ~> Lower f y)
-> Struct Closed a b -> Lower f a ~> Lower f b
foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
_ (Apply @a @b) = forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @a @f (forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @b @f (forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @_ @(Lower f a) @(Lower f b)))
  foldStructure @f forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go (Curry @a @b (a **! b) ~> c
f) = forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @a @f (forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
forall (a :: FREE cs p) {k} (f :: j +-> k) r.
(IsFreeOb a, Representable f, All cs k) =>
(Ob (Lower f a) => r) -> r
withLowerOb @b @f (forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @_ @(Lower f a) @(Lower f b) (((a **! b) ~> c) -> Lower f (a **! b) ~> Lower f c
forall (x :: FREE cs p) (y :: FREE cs p).
(x ~> y) -> Lower f x ~> Lower f y
go (a **! b) ~> c
f)))
deriving instance (WithEq a) => P.Eq (Struct Closed a b)
deriving instance (WithShow a) => P.Show (Struct Closed a b)
instance (Ok cs p, Closed `Elem` cs, Monoidal `Elem` cs) => Closed (FREE cs p) where
  type a ~~> b = a --> b
  withObExp :: forall (a :: FREE cs p) (b :: FREE cs p) 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 :: FREE cs p) (b :: FREE cs p) (c :: FREE cs p).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry (a ** b) ~> c
f = Struct Closed a (b --> c) -> Free a a -> Free a (b --> c)
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
Str (((a **! b) ~> c) -> Struct Closed a (b --> c)
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) (a :: FREE cs p) (c :: FREE cs p).
(Ob a, Ob a) =>
((a **! a) ~> c) -> Struct Closed a (a --> c)
Curry (a **! b) ~> c
(a ** b) ~> c
f) Free a a
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id ((Ob (a **! b), Ob c) => Free a (b --> c))
-> Free (a **! b) c -> Free a (b --> c)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
forall (a :: FREE cs p) (b :: FREE cs p) r.
((Ob a, Ob b) => r) -> Free a b -> r
\\ (a ** b) ~> c
Free (a **! b) c
f
  apply :: forall (a :: FREE cs p) (b :: FREE cs p).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply = Struct Closed ((a --> b) **! a) b
-> Free ((a --> b) **! a) ((a --> b) **! a)
-> Free ((a --> b) **! a) b
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (c :: Type -> Constraint) (a1 :: FREE cs p) (b :: FREE cs p)
       (a :: FREE cs p).
(HasStructure cs p c, Ob a1, Ob b) =>
Struct c a1 b -> Free a a1 -> Free a b
Str Struct Closed ((a --> b) **! a) b
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p) (b :: FREE cs p).
(Ob a, Ob b) =>
Struct Closed ((a --> b) **! a) b
Apply Free ((a --> b) **! a) ((a --> b) **! a)
forall {j} {cs :: [Type -> Constraint]} {p :: CAT j}
       (a :: FREE cs p).
Ob a =>
Free a a
Id