{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Closed monoidal categories: 'Closed' provides the internal hom @a '~~>' b@, right adjoint to
-- tensoring, with 'curry', 'apply' and functoriality @('^^^')@. Also defines cartesian closed
-- ('CCC') and bicartesian closed ('BiCCC') categories.
module Proarrow.Category.Monoidal.Closed where

import Data.Kind (Constraint, Type)
import Prelude (($))
import Prelude qualified as P

import Proarrow.Category.Instance.Bool (BOOL (..), BoolLeq, Booleans (..))
import Proarrow.Category.Instance.Free
  ( Elem (..)
  , Elems
  , FREE (..)
  , Free (..)
  , HasStructure (..)
  , IsFreeOb (..)
  , Lower
  , WithShow
  , withLowerOb
  )
import Proarrow.Category.Instance.Opposite (OPPOSITE (..), Op (..))
import Proarrow.Category.Instance.Product ((:**:) (..))
import Proarrow.Category.Instance.Unit qualified as U
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..), type (**!))
import Proarrow.Category.Monoidal.Strictified (Fold, Strictified (..), concatMany, obj1, singleton, splitMany, (==))
import Proarrow.Core (CAT, CategoryOf (..), Kind, Profunctor (..), Promonad (..), obj, (//), type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Limit.BinaryProduct ()
import Proarrow.Profunctor.Corepresentable (Corepresentable (..))
import Proarrow.Profunctor.Representable (Rep (..))
import Proarrow.Tools.Laws (Bijection (..), Law (..), Laws (..), bijection, (===))

infixr 2 ~~>

-- | A (right) closed monoidal category: every @b '~~>' c@ is an internal hom, right adjoint to
-- tensoring with @b@. 'curry' and 'Proarrow.Category.Monoidal.Closed.uncurry' witness the
-- adjunction @Hom(a '**' b, c) ≅ Hom(a, b '~~>' c)@.
--
-- __Laws:__
--
-- * @'curry'@ and @'Proarrow.Category.Monoidal.Closed.uncurry'@ are mutually inverse:
--   @'Proarrow.Category.Monoidal.Closed.uncurry' ('curry' f) = f@ and
--   @'curry' ('Proarrow.Category.Monoidal.Closed.uncurry' g) = g@
-- * and natural in all three variables: for @f :: a' '~>' a@, @g :: b' '~>' b@, @h :: c '~>' c'@,
--   @'curry' . 'dimap' (f '**' g) h = 'dimap' f (h '^^^' g) . 'curry'@
--
-- Together these say @'curry'@ is a natural isomorphism, which also forces the familiar
-- @'apply' . ('curry' f '**' 'id') = f@. The exponential is thereby functorial: @'(^^^)'@ is
-- contravariant in its second argument and covariant in its first.
--
-- Checked by 'Proarrow.Testing.Laws.testClosed'.
class (Monoidal k) => Closed k where
  -- | The internal hom (exponential) object.
  type (a :: k) ~~> (b :: k) :: k

  -- | Recovers @'Ob' (a '~~>' b)@ from the objecthood of the ends.
  withObExp :: (Ob (a :: k), Ob b) => ((Ob (a ~~> b)) => r) -> r

  -- | Transposes an arrow out of a tensor into one into an exponential.
  curry :: (Ob (a :: k), Ob b) => a ** b ~> c -> a ~> b ~~> c

  -- | Evaluation: the counit of the adjunction.
  apply :: (Ob (a :: k), Ob b) => (a ~~> b) ** a ~> b

  -- | The exponential's action on arrows: covariant in the result, contravariant in the argument.
  (^^^) :: 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
$
          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 :: CAT 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 :: CAT 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)
** 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 :: CAT 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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b)

curryS :: forall {k} b c (a :: k). (Closed k) => [a, b] ~> '[c] -> '[a] ~> '[b ~~> c]
curryS :: forall {k} (b :: k) (c :: k) (a :: k).
Closed k =>
('[a, b] ~> '[c]) -> '[a] ~> '[b ~~> c]
curryS (Str Fold '[a, b] ~> Fold '[c]
f) = 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) => '[a] ~> '[b ~~> c]) -> '[a] ~> '[b ~~> c])
-> (Ob (b ~~> c) => '[a] ~> '[b ~~> c]) -> '[a] ~> '[b ~~> c]
forall a b. (a -> b) -> a -> b
$ (Fold '[a] ~> Fold '[b ~~> c]) -> Strictified '[a] '[b ~~> c]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str (forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @a @b @c (a ** b) ~> c
Fold '[a, b] ~> Fold '[c]
f)

curryS'
  :: forall {k} as c (b :: k). (Closed k, Ob as, Ob b) => (as ** '[b]) ~> '[c] -> as ~> '[b ~~> c]
curryS' :: forall {k} (as :: [k]) (c :: k) (b :: k).
(Closed k, Ob as, Ob b) =>
((as ** '[b]) ~> '[c]) -> as ~> '[b ~~> c]
curryS' (as ** '[b]) ~> '[c]
f = as ~> '[Fold as]
forall {k} (as :: [k]). (Ob as, Monoidal k) => as ~> '[Fold as]
concatMany (as ~> '[Fold as])
-> ('[Fold as] ~> '[b ~~> c]) -> as ~> '[b ~~> c]
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== forall (b :: k) (c :: k) (a :: k).
Closed k =>
('[a, b] ~> '[c]) -> '[a] ~> '[b ~~> c]
forall {k} (b :: k) (c :: k) (a :: k).
Closed k =>
('[a, b] ~> '[c]) -> '[a] ~> '[b ~~> c]
curryS @b @c @(Fold as) (forall (as :: [k]). (Ob as, Monoidal k) => '[Fold as] ~> as
forall {k} (as :: [k]). (Ob as, Monoidal k) => '[Fold as] ~> as
splitMany @as Strictified '[Fold as] as
-> Strictified '[b] '[b]
-> Strictified ('[Fold as] ** '[b]) (as ** '[b])
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (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)
** Obj '[b]
Strictified '[b] '[b]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 ('[Fold as, b] ~> (as ++ '[b]))
-> ((as ++ '[b]) ~> '[c]) -> '[Fold as, b] ~> '[c]
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== (as ** '[b]) ~> '[c]
(as ++ '[b]) ~> '[c]
f)

applyS :: forall {k} (a :: k) b. (Closed k, Ob a, Ob b) => '[a ~~> b, a] ~> '[b]
applyS :: forall {k} (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
'[a ~~> b, a] ~> '[b]
applyS = 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, a] ~> '[b]) -> '[a ~~> b, a] ~> '[b])
-> (Ob (a ~~> b) => '[a ~~> b, a] ~> '[b]) -> '[a ~~> b, a] ~> '[b]
forall a b. (a -> b) -> a -> b
$ (Fold '[a ~~> b, a] ~> Fold '[b]) -> Strictified '[a ~~> b, a] '[b]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str (forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @k @a @b)

uncurryS :: forall {k} b c (a :: k). (Closed k, Ob b, Ob c) => '[a] ~> '[b ~~> c] -> '[a, b] ~> '[c]
uncurryS :: forall {k} (b :: k) (c :: k) (a :: k).
(Closed k, Ob b, Ob c) =>
('[a] ~> '[b ~~> c]) -> '[a, b] ~> '[c]
uncurryS '[a] ~> '[b ~~> c]
f = '[a] ~> '[b ~~> c]
Strictified '[a] '[b ~~> c]
f Strictified '[a] '[b ~~> c]
-> Strictified '[b] '[b]
-> Strictified ('[a] ** '[b]) ('[b ~~> c] ** '[b])
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (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)
** Obj '[b]
Strictified '[b] '[b]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 ('[a, b] ~> ('[b ~~> c] ++ '[b]))
-> (('[b ~~> c] ++ '[b]) ~> '[c]) -> '[a, b] ~> '[c]
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== '[b ~~> c, b] ~> '[c]
('[b ~~> c] ++ '[b]) ~> '[c]
forall {k} (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
'[a ~~> b, a] ~> '[b]
applyS

uncurryS' :: forall {k} as b (c :: k). (Closed k, Ob b, Ob c) => as ~> '[b ~~> c] -> (as ** '[b]) ~> '[c]
uncurryS' :: forall {k} (as :: [k]) (b :: k) (c :: k).
(Closed k, Ob b, Ob c) =>
(as ~> '[b ~~> c]) -> (as ** '[b]) ~> '[c]
uncurryS' f :: as ~> '[b ~~> c]
f@Str{} = forall (as :: [k]). (Ob as, Monoidal k) => as ~> '[Fold as]
forall {k} (as :: [k]). (Ob as, Monoidal k) => as ~> '[Fold as]
concatMany @as Strictified as '[Fold as]
-> Strictified '[b] '[b]
-> Strictified (as ** '[b]) ('[Fold as] ** '[b])
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (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)
** Obj '[b]
Strictified '[b] '[b]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 ((as ++ '[b]) ~> ('[Fold as] ++ '[b]))
-> (('[Fold as] ++ '[b]) ~> '[c]) -> (as ++ '[b]) ~> '[c]
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== 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]
uncurryS @b @c @(Fold as) ('[Fold as] ~> as
forall {k} (as :: [k]). (Ob as, Monoidal k) => '[Fold as] ~> as
splitMany ('[Fold as] ~> as)
-> (as ~> '[b ~~> c]) -> '[Fold as] ~> '[b ~~> c]
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> a ~> c
== as ~> '[b ~~> c]
f)

compS :: forall {k} (a :: k) b c. (Closed k, Ob a, Ob b, Ob c) => '[b ~~> c, a ~~> b] ~> '[a ~~> c]
compS :: forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b, Ob c) =>
'[b ~~> c, a ~~> b] ~> '[a ~~> c]
compS =
  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
$
    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
$
      (('[b ~~> c, a ~~> b] ** '[a]) ~> '[c])
-> '[b ~~> c, a ~~> b] ~> '[a ~~> c]
forall {k} (as :: [k]) (c :: k) (b :: k).
(Closed k, Ob as, Ob b) =>
((as ** '[b]) ~> '[c]) -> as ~> '[b ~~> c]
curryS' (Obj '[b ~~> c]
Strictified '[b ~~> c] '[b ~~> c]
forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
obj1 Strictified '[b ~~> c] '[b ~~> c]
-> Strictified '[a ~~> b, a] '[b]
-> Strictified ('[b ~~> c] ** '[a ~~> b, a]) ('[b ~~> c] ** '[b])
forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]).
Strictified x1 x2
-> Strictified y1 y2 -> Strictified (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)
** 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]
applyS @a @b ('[b ~~> c, a ~~> b, a] ~> ('[b ~~> c] ++ '[b]))
-> (('[b ~~> c] ++ '[b]) ~> '[c]) -> '[b ~~> c, a ~~> b, a] ~> '[c]
forall k (a :: k) (b :: k) (c :: k).
CategoryOf k =>
(a ~> b) -> (b ~> c) -> 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]
applyS @b @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 = Strictified '[b ~~> c, a ~~> b] '[a ~~> c]
-> Fold '[b ~~> c, a ~~> b] ~> Fold '[a ~~> c]
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
unStr (forall (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b, Ob c) =>
'[b ~~> c, a ~~> b] ~> '[a ~~> c]
forall {k} (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b, Ob c) =>
'[b ~~> c, a ~~> b] ~> '[a ~~> c]
compS @a @b @c)

mkExponentialS :: forall {k} (a :: k) b. (Closed k) => '[a] ~> '[b] -> '[] ~> '[a ~~> b]
mkExponentialS :: forall {k} (a :: k) (b :: k).
Closed k =>
('[a] ~> '[b]) -> '[] ~> '[a ~~> b]
mkExponentialS f :: '[a] ~> '[b]
f@Str{} = (('[] ** '[a]) ~> '[b]) -> '[] ~> '[a ~~> b]
forall {k} (as :: [k]) (c :: k) (b :: k).
(Closed k, Ob as, Ob b) =>
((as ** '[b]) ~> '[c]) -> as ~> '[b ~~> c]
curryS' '[a] ~> '[b]
('[] ** '[a]) ~> '[b]
f

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 = Strictified '[] '[a ~~> b] -> Fold '[] ~> Fold '[a ~~> b]
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
unStr (('[a] ~> '[b]) -> '[] ~> '[a ~~> b]
forall {k} (a :: k) (b :: k).
Closed k =>
('[a] ~> '[b]) -> '[] ~> '[a ~~> b]
mkExponentialS ((a ~> b) -> '[a] ~> '[b]
forall k (a :: k) (b :: k).
CategoryOf k =>
(a ~> b) -> '[a] ~> '[b]
singleton a ~> b
ab))

lowerS :: forall {k} (a :: k) b. (Closed k, Ob a, Ob b) => ('[] ~> '[a ~~> b]) -> '[a] ~> '[b]
lowerS :: forall {k} (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
('[] ~> '[a ~~> b]) -> '[a] ~> '[b]
lowerS = ('[] ~> '[a ~~> b]) -> '[a] ~> '[b]
('[] ~> '[a ~~> b]) -> ('[] ** '[a]) ~> '[b]
forall {k} (as :: [k]) (b :: k) (c :: k).
(Closed k, Ob b, Ob c) =>
(as ~> '[b ~~> c]) -> (as ** '[b]) ~> '[c]
uncurryS'

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 = Strictified '[a] '[b] -> Fold '[a] ~> Fold '[b]
forall {k} (as :: [k]) (bs :: [k]).
Strictified as bs -> Fold as ~> Fold bs
unStr (('[] ~> '[a ~~> b]) -> '[a] ~> '[b]
forall {k} (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
('[] ~> '[a ~~> b]) -> '[a] ~> '[b]
lowerS ((Fold '[] ~> Fold '[a ~~> b]) -> Strictified '[] '[a ~~> b]
forall {k} (as :: [k]) (bs :: [k]).
(Ob as, Ob bs) =>
(Fold as ~> Fold bs) -> Strictified as bs
Str Unit ~> (a ~~> b)
Fold '[] ~> Fold '[a ~~> b]
f)) ((Ob Unit, Ob (a ~~> b)) => a ~> b)
-> (Unit ~> (a ~~> b)) -> 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
\\ Unit ~> (a ~~> b)
f

toEl :: forall {k} (a :: k). (Closed k, Ob a) => a ~> Unit ~~> a
toEl :: forall {k} (a :: k). (Closed k, Ob a) => a ~> (Unit ~~> a)
toEl = forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @a @Unit @a (a ** Unit) ~> a
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor

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 :: CAT 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

-- | Implication is the internal hom of the walking arrow: @a ~~> b@ is @'BoolLeq' a b@.
instance Closed BOOL where
  type a ~~> b = BoolLeq a b
  withObExp :: forall (a :: BOOL) (b :: BOOL) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @a @b Ob (a ~~> b) => r
r = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @b) of
    (Booleans a a
Fls, Booleans b b
Fls) -> r
Ob (a ~~> b) => r
r
    (Booleans a a
Fls, Booleans b b
Tru) -> r
Ob (a ~~> b) => r
r
    (Booleans a a
Tru, Booleans b b
Fls) -> r
Ob (a ~~> b) => r
r
    (Booleans a a
Tru, Booleans b b
Tru) -> r
Ob (a ~~> b) => r
r
  curry :: forall (a :: BOOL) (b :: BOOL) (c :: BOOL).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @a @b @c (a ** b) ~> c
f =
    ( case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @b, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @c) of
        (Booleans a a
Fls, Booleans b b
Fls, Booleans c c
Fls) -> Booleans a (BoolLeq b c)
Booleans 'FLS 'TRU
F2T
        (Booleans a a
Fls, Booleans b b
Fls, Booleans c c
Tru) -> Booleans a (BoolLeq b c)
Booleans 'FLS 'TRU
F2T
        (Booleans a a
Fls, Booleans b b
Tru, Booleans c c
Fls) -> Booleans a (BoolLeq b c)
Booleans 'FLS 'FLS
Fls
        (Booleans a a
Fls, Booleans b b
Tru, Booleans c c
Tru) -> Booleans a (BoolLeq b c)
Booleans 'FLS 'TRU
F2T
        (Booleans a a
Tru, Booleans b b
Fls, Booleans c c
Fls) -> Booleans a (BoolLeq b c)
Booleans 'TRU 'TRU
Tru
        (Booleans a a
Tru, Booleans b b
Fls, Booleans c c
Tru) -> Booleans a (BoolLeq b c)
Booleans 'TRU 'TRU
Tru
        (Booleans a a
Tru, Booleans b b
Tru, Booleans c c
Fls) -> case (a ** b) ~> c
f of {}
        (Booleans a a
Tru, Booleans b b
Tru, Booleans c c
Tru) -> Booleans a (BoolLeq b c)
Booleans 'TRU 'TRU
Tru
    )
      ((Ob (a && b), Ob c) => Booleans a (BoolLeq b c))
-> Booleans (a && b) c -> Booleans a (BoolLeq 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 :: BOOL) (b :: BOOL) r.
((Ob a, Ob b) => r) -> Booleans a b -> r
\\ (a ** b) ~> c
Booleans (a && b) c
f
  apply :: forall (a :: BOOL) (b :: BOOL).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @a @b = case (forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @a, forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
forall (a :: BOOL). (CategoryOf BOOL, Ob a) => Obj a
obj @b) of
    (Booleans a a
Fls, Booleans b b
Fls) -> ((a ~~> b) ** a) ~> b
Booleans 'FLS 'FLS
Fls
    (Booleans a a
Fls, Booleans b b
Tru) -> ((a ~~> b) ** a) ~> b
Booleans 'FLS 'TRU
F2T
    (Booleans a a
Tru, Booleans b b
Fls) -> ((a ~~> b) ** a) ~> b
Booleans 'FLS 'FLS
Fls
    (Booleans a a
Tru, Booleans b b
Tru) -> ((a ~~> b) ** a) ~> b
Booleans 'TRU 'TRU
Tru

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 ExpRep :: (OPPOSITE k, k) +-> k
instance (Closed k) => FunctorForRep (ExpRep :: (OPPOSITE k, k) +-> k) where
  type ExpRep @ '(OP a, b) = a ~~> b
  fmap :: forall (a :: (OPPOSITE k, k)) (b :: (OPPOSITE k, k)).
(a ~> b) -> (ExpRep @ a) ~> (ExpRep @ b)
fmap (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

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

-- | The "reader"\/exponential-by-@m@ functor, covariant unlike 'Not' (which fixes the codomain).
data family Exp (m :: k) :: k +-> k

instance (Closed k, Ob m) => FunctorForRep (Exp m :: k +-> k) where
  type Exp m @ a = m ~~> a
  fmap :: forall (a :: k) (b :: k). (a ~> b) -> (Exp m @ a) ~> (Exp m @ b)
fmap a ~> b
f = a ~> b
f (a ~> b) -> (m ~> m) -> (m ~~> a) ~> (m ~~> 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 @m

-- | The Op-Op adjunction, giving rise to the continuation monad.
instance (Closed k, SymMonoidal k, Ob r) => Corepresentable (Rep (Not (r :: k))) where
  type Rep (Not r) %% a = OP (a ~~> r)
  cotabulate :: forall (a :: k) (b :: OPPOSITE k).
Ob a =>
((Rep (Not r) %% a) ~> b) -> Rep (Not r) a b
cotabulate (Op b1 ~> a1
f) = (a ~> (Not r @ b)) -> Rep (Not r) a b
forall {j} {k} (b :: j) (f :: j +-> k) (a :: k).
Ob b =>
(a ~> (f @ b)) -> Rep f a b
Rep (forall (c :: k) (a :: k) (b :: k).
(Closed k, SymMonoidal k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> b ~> (a ~~> c)
forall {k} (c :: k) (a :: k) (b :: k).
(Closed k, SymMonoidal k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> b ~> (a ~~> c)
swapClosed @r b1 ~> a1
b1 ~> (a ~~> r)
f) ((Ob b1, Ob a1) => Rep (Not r) a b)
-> (b1 ~> a1) -> Rep (Not r) 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
\\ b1 ~> a1
f
  coindex :: forall (a :: k) (b :: OPPOSITE k).
Rep (Not r) a b -> (Rep (Not r) %% a) ~> b
coindex (Rep a ~> (Not r @ b)
f) = (UN OP b ~> (a ~~> r)) -> Op (~>) (OP (a ~~> r)) (OP (UN OP b))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op (forall (c :: k) (a :: k) (b :: k).
(Closed k, SymMonoidal k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> b ~> (a ~~> c)
forall {k} (c :: k) (a :: k) (b :: k).
(Closed k, SymMonoidal k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> b ~> (a ~~> c)
swapClosed @r a ~> (Not r @ b)
a ~> (UN OP b ~~> r)
f)
  corepMap :: forall (a :: k) (b :: k).
(a ~> b) -> (Rep (Not r) %% a) ~> (Rep (Not r) %% b)
corepMap a ~> b
f = ((b ~~> r) ~> (a ~~> r)) -> Op (~>) (OP (a ~~> r)) (OP (b ~~> r))
forall {j} {k} (p :: j +-> k) (b1 :: k) (a1 :: j).
p b1 a1 -> Op p (OP a1) (OP b1)
Op (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @r Obj r -> (a ~> b) -> (b ~~> r) ~> (a ~~> r)
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)
^^^ a ~> b
f)

swapClosed :: forall {k} (c :: k) a b. (Closed k, SymMonoidal k, Ob b, Ob c) => a ~> b ~~> c -> b ~> a ~~> c
swapClosed :: forall {k} (c :: k) (a :: k) (b :: k).
(Closed k, SymMonoidal k, Ob b, Ob c) =>
(a ~> (b ~~> c)) -> b ~> (a ~~> c)
swapClosed a ~> (b ~~> c)
f = forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @k @b @a (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 @b @c a ~> (b ~~> c)
f ((a ** b) ~> c) -> ((b ** a) ~> (a ** b)) -> (b ** a) ~> c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @b @a) ((Ob a, Ob (b ~~> c)) => b ~> (a ~~> c))
-> (a ~> (b ~~> c)) -> b ~> (a ~~> c)
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 ~~> c)
f

data family (-->) (a :: k) (b :: k) :: k

-- | The structures the free category needs for 'Closed', and those its laws are stated for.
type ClosedStructures :: [Kind -> Constraint]
type ClosedStructures = '[Monoidal, Closed]

instance (IsFreeOb (a :: FREE cs p), IsFreeOb b, ClosedStructures `Elems` cs) => IsFreeOb (a --> b) where
  type Lower f (a --> b) = Lower f a ~~> Lower f b
  lowerOb :: forall k' (f :: k +-> k') r.
(Representable f, All cs k') =>
(Ob (Lower f (a --> b)) => r) -> r
lowerOb @k' @f Ob (Lower f (a --> b)) => r
r = forall (c :: Type -> Constraint) (cs :: [Type -> Constraint]) k r.
(Elem c cs, All cs k) =>
(c k => r) -> r
fromAll @Closed @cs @k' (forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @b (forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @k' @(Lower f a) @(Lower f b) r
Ob (Lower f (a --> b)) => r
Ob (Lower f a ~~> Lower f b) => r
r)))
instance (ClosedStructures `Elems` cs) => HasStructure cs (p :: CAT k) 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 :: k +-> k') (a :: FREE cs p) (b :: FREE cs p).
(Closed k', 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 {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @b (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 {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @a (forall {k} {k'} {cs :: [Type -> Constraint]} {p :: CAT k}
       (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
forall (f :: k +-> k') (a :: FREE cs p) r.
(IsFreeOb a, Representable f, All cs k') =>
(Ob (Lower f a) => r) -> r
withLowerOb @f @b (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)))
instance (WithShow a) => P.Show (Struct Closed a b) where
  showsPrec :: Int -> Struct Closed a b -> ShowS
showsPrec Int
_ Struct Closed a b
R:StructkcspClosedab k cs p a b
Apply = String -> ShowS
P.showString String
"apply"
  showsPrec Int
d (Curry (a **! b) ~> c
f) = Bool -> ShowS -> ShowS
P.showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
P.> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
P.showString String
"curry " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Int -> Free (a **! b) c -> ShowS
forall a. Show a => Int -> a -> ShowS
P.showsPrec Int
11 (a **! b) ~> c
Free (a **! b) c
f

instance (ClosedStructures `Elems` cs) => Closed (FREE cs (p :: CAT k)) 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 {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (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
St (((a **! b) ~> c) -> Struct Closed a (b --> c)
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (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 {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil ((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 {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (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
St Struct Closed ((a --> b) **! a) b
forall {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (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 {k} {cs :: [Type -> Constraint]} {p :: CAT k}
       (a :: FREE cs p).
Ob a =>
Free a a
Nil

-- | 'apply' undoes 'curry' and every arrow into an exponential is the 'curry' of one ('curry' is
-- a bijection with inverse @f |-> 'apply' . (f '**' 'id')@), 'curry' is natural in all three
-- objects, and '^^^' is the exponential's action on arrows defined from 'curry' and 'apply'.
-- Together these make @(- ** b)@ left adjoint to @(b ~~> -)@, and '^^^' a profunctor.
instance Laws ClosedStructures where
  laws :: [Law ClosedStructures]
laws =
    String -> BijectionBody ClosedStructures -> [Law ClosedStructures]
forall (cs :: [Type -> Constraint]).
String -> BijectionBody cs -> [Law cs]
bijection
      String
"curry"
      ( \ @a @b @c forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor ->
          forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @b ((Ob (a ** b) => Bijection m k) -> Bijection m k)
-> (Ob (a ** b) => Bijection m k) -> Bijection m k
forall a b. (a -> b) -> a -> b
$
            forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @_ @b @c ((Ob (b ~~> c) => Bijection m k) -> Bijection m k)
-> (Ob (b ~~> c) => Bijection m k) -> Bijection m k
forall a b. (a -> b) -> a -> b
$
              m ((a ** b) ~> c)
-> m (a ~> (b ~~> c))
-> (((a ** b) ~> c) -> a ~> (b ~~> c))
-> ((a ~> (b ~~> c)) -> (a ** b) ~> c)
-> Bijection m k
forall {k} (m :: Type -> Type) (a :: k) (b :: k) (c :: k) (d :: k).
m (a ~> b)
-> m (c ~> d)
-> ((a ~> b) -> c ~> d)
-> ((c ~> d) -> a ~> b)
-> Bijection m k
Bijection (forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @(a ** b) @c String
"p") (forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @a @(b ~~> c) String
"q") (forall k (a :: k) (b :: k) (c :: k).
(Closed k, Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @_ @a @b) (\a ~> (b ~~> c)
q -> forall k (a :: k) (b :: k).
(Closed k, Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @_ @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 :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ~> (b ~~> c)
q (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)
** forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b))
      )
      [Law ClosedStructures]
-> [Law ClosedStructures] -> [Law ClosedStructures]
forall a. [a] -> [a] -> [a]
P.++ [ String -> LawBody ClosedStructures -> Law ClosedStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"curry naturality" \ @a @b @c @d @e forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @a @b ((Ob (a ** b) => m (Equation k)) -> m (Equation k))
-> (Ob (a ** b) => m (Equation k)) -> m (Equation k)
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @d @d do
               p <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @(a ** b) @c String
"p"
               f <- mor @d @a "f"
               g <- mor @d @b "g"
               h <- mor @c @e "h"
               (h ^^^ g) . curry @_ @a @b p . f === curry @_ @d @d (h . p . (f ** g))
           , String -> LawBody ClosedStructures -> Law ClosedStructures
forall (cs :: [Type -> Constraint]). String -> LawBody cs -> Law cs
Law String
"internal hom on arrows" \ @a @b @c @d forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor -> do
               f <- forall (x :: k) (y :: k). (Ob x, Ob y) => String -> m (x ~> y)
mor @b @d String
"f"
               g <- mor @c @a "g"
               withObExp @_ @a @b (f ^^^ g === curry @_ @(a ~~> b) @c (f . apply @_ @a @b . (obj @(a ~~> b) ** g)))
           ]