{-# LANGUAGE
  TypeOperators,
  TypeFamilies,
  GADTs,
  PolyKinds,
  DataKinds,
  Rank2Types,
  PatternSynonyms,
  ScopedTypeVariables,
  UndecidableInstances,
  TypeSynonymInstances,
  FlexibleInstances,
  NoImplicitPrelude #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.CartesianClosed
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
-----------------------------------------------------------------------------
module Data.Category.CartesianClosed where

import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
import Data.Category.Product
import Data.Category.Limit
import Data.Category.Adjunction
import Data.Category.Monoidal as M
import Data.Category.Yoneda
import qualified Data.Category.Unit as U


-- | A category is cartesian closed if it has all products and exponentials for all objects.
class (HasTerminalObject k, HasBinaryProducts k) => CartesianClosed k where
  type Exponential k (y :: Kind k) (z :: Kind k) :: Kind k

  apply :: Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z
  tuple :: Obj k y -> Obj k z -> k z (Exponential k y (BinaryProduct k z y))
  (^^^) :: k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)


data ExpFunctor (k :: * -> * -> *) = ExpFunctor
-- | The exponential as a bifunctor.
instance CartesianClosed k => Functor (ExpFunctor k) where
  type Dom (ExpFunctor k) = Op k :**: k
  type Cod (ExpFunctor k) = k
  type ExpFunctor k :% (y, z) = Exponential k y z

  ExpFunctor k
ExpFunctor % :: ExpFunctor k
-> Dom (ExpFunctor k) a b
-> Cod (ExpFunctor k) (ExpFunctor k :% a) (ExpFunctor k :% b)
% (Op y :**: z) = k a2 b2
z k a2 b2 -> k b1 a1 -> k (Exponential k a1 a2) (Exponential k b1 b2)
forall k (k :: k -> k -> *) (z1 :: k) (z2 :: k) (y2 :: k)
       (y1 :: k).
CartesianClosed k =>
k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)
^^^ k b1 a1
y


flip :: CartesianClosed k => Obj k a -> Obj k b -> Obj k c -> k (Exponential k a (Exponential k b c)) (Exponential k b (Exponential k a c))
flip :: Obj k a
-> Obj k b
-> Obj k c
-> k (Exponential k a (Exponential k b c))
     (Exponential k b (Exponential k a c))
flip Obj k a
a Obj k b
b Obj k c
c = Obj k a
-> Obj k b
-> Obj k c
-> k (Exponential k a (Exponential k b c))
     (Exponential k b (Exponential k a c))
forall k (k :: k -> k -> *) (a :: k) (b :: k) (c :: k).
CartesianClosed k =>
Obj k a
-> Obj k b
-> Obj k c
-> k (Exponential k a (Exponential k b c))
     (Exponential k b (Exponential k a c))
flip Obj k a
a Obj k b
b Obj k c
c -- TODO


-- | Exponentials in @Hask@ are functions.
instance CartesianClosed (->) where
  type Exponential (->) y z = y -> z

  apply :: Obj (->) y
-> Obj (->) z -> BinaryProduct (->) (Exponential (->) y z) y -> z
apply Obj (->) y
_ Obj (->) z
_ (f, y) = y -> z
f y
y
  tuple :: Obj (->) y
-> Obj (->) z -> z -> Exponential (->) y (BinaryProduct (->) z y)
tuple Obj (->) y
_ Obj (->) z
_ z
z      = \y
y -> (z
z, y
y)
  z1 -> z2
f ^^^ :: (z1 -> z2)
-> (y2 -> y1) -> Exponential (->) y1 z1 -> Exponential (->) y2 z2
^^^ y2 -> y1
h          = \Exponential (->) y1 z1
g -> z1 -> z2
f (z1 -> z2) -> (y2 -> z1) -> y2 -> z2
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Exponential (->) y1 z1
y1 -> z1
g (y1 -> z1) -> (y2 -> y1) -> y2 -> z1
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. y2 -> y1
h


instance CartesianClosed U.Unit where
  type Exponential U.Unit () () = ()
  apply :: Obj Unit y
-> Obj Unit z
-> Unit (BinaryProduct Unit (Exponential Unit y z) y) z
apply Obj Unit y
U.Unit Obj Unit z
U.Unit = Unit () ()
Unit (BinaryProduct Unit (Exponential Unit y z) y) z
U.Unit
  tuple :: Obj Unit y
-> Obj Unit z
-> Unit z (Exponential Unit y (BinaryProduct Unit z y))
tuple Obj Unit y
U.Unit Obj Unit z
U.Unit = Unit z (Exponential Unit y (BinaryProduct Unit z y))
Unit () ()
U.Unit
  Unit z1 z2
U.Unit ^^^ :: Unit z1 z2
-> Unit y2 y1
-> Unit (Exponential Unit y1 z1) (Exponential Unit y2 z2)
^^^ Unit y2 y1
U.Unit = Unit () ()
Unit (Exponential Unit y1 z1) (Exponential Unit y2 z2)
U.Unit


-- | Exponentials in @Cat@ are the functor categories.
instance CartesianClosed Cat where
  type Exponential Cat c d = Nat c d

  apply :: Obj Cat y
-> Obj Cat z -> Cat (BinaryProduct Cat (Exponential Cat y z) y) z
apply CatA{} CatA{} = Apply z y -> Cat (Dom (Apply z y)) (Cod (Apply z y))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Apply z y
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Apply c1 c2
Apply
  tuple :: Obj Cat y
-> Obj Cat z -> Cat z (Exponential Cat y (BinaryProduct Cat z y))
tuple CatA{} CatA{} = Tuple z y -> Cat (Dom (Tuple z y)) (Cod (Tuple z y))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA Tuple z y
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *). Tuple c1 c2
Tuple
  CatA ftag
f ^^^ :: Cat z1 z2
-> Cat y2 y1 -> Cat (Exponential Cat y1 z1) (Exponential Cat y2 z2)
^^^ CatA ftag
h = Wrap ftag ftag -> Cat (Dom (Wrap ftag ftag)) (Cod (Wrap ftag ftag))
forall ftag.
(Functor ftag, Category (Dom ftag), Category (Cod ftag)) =>
ftag -> Cat (Dom ftag) (Cod ftag)
CatA (ftag -> ftag -> Wrap ftag ftag
forall f h. f -> h -> Wrap f h
Wrap ftag
f ftag
h)


type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite
  (   ProductFunctor (Presheaves k)
  :.: Tuple2 (Presheaves k) (Presheaves k) y
  :.: YonedaEmbedding k
  )
pattern PshExponential :: Category k => Obj (Presheaves k) y -> Obj (Presheaves k) z -> PShExponential k y z
pattern $bPshExponential :: Obj (Presheaves k) y
-> Obj (Presheaves k) z -> PShExponential k y z
$mPshExponential :: forall r (k :: * -> * -> *) y z.
Category k =>
PShExponential k y z
-> (Obj (Presheaves k) y -> Obj (Presheaves k) z -> r)
-> (Void# -> r)
-> r
PshExponential y z = Hom_X z :.: Opposite (ProductFunctor :.: Tuple2 y :.: YonedaEmbedding)

-- | The category of presheaves on a category @C@ is cartesian closed for any @C@.
instance Category k => CartesianClosed (Presheaves k) where
  type Exponential (Presheaves k) y z = PShExponential k y z

  apply :: Obj (Presheaves k) y
-> Obj (Presheaves k) z
-> Presheaves
     k
     (BinaryProduct (Presheaves k) (Exponential (Presheaves k) y z) y)
     z
apply yn :: Obj (Presheaves k) y
yn@(Nat y
y y
_ forall z. Obj (Op k) z -> Component y y z
_) zn :: Obj (Presheaves k) z
zn@(Nat z
z z
_ forall z. Obj (Op k) z -> Component z z z
_) = (((Presheaves k :-*: z)
  :.: Opposite
        ((ProductFunctor (Presheaves k)
          :.: Tuple2 (Presheaves k) (Presheaves k) y)
         :.: ((FunctorCompose (Op k) (Op k :**: k) (->)
               :.: Tuple1
                     (Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
              :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
                    :.: Tuple1
                          (Nat (k :**: Op k) (Op k :**: k))
                          (Nat (Op k) (k :**: Op k))
                          (Swap k (Op k)))
                   :.: Tuple k (Op k)))))
 :*: y)
-> z
-> (forall z.
    Obj (Op k) z
    -> Component
         (((Presheaves k :-*: z)
           :.: Opposite
                 ((ProductFunctor (Presheaves k)
                   :.: Tuple2 (Presheaves k) (Presheaves k) y)
                  :.: ((FunctorCompose (Op k) (Op k :**: k) (->)
                        :.: Tuple1
                              (Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
                       :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
                             :.: Tuple1
                                   (Nat (k :**: Op k) (Op k :**: k))
                                   (Nat (Op k) (k :**: Op k))
                                   (Swap k (Op k)))
                            :.: Tuple k (Op k)))))
          :*: y)
         z
         z)
-> Nat
     (Op k)
     (->)
     (((Presheaves k :-*: z)
       :.: Opposite
             ((ProductFunctor (Presheaves k)
               :.: Tuple2 (Presheaves k) (Presheaves k) y)
              :.: ((FunctorCompose (Op k) (Op k :**: k) (->)
                    :.: Tuple1
                          (Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
                   :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
                         :.: Tuple1
                               (Nat (k :**: Op k) (Op k :**: k))
                               (Nat (Op k) (k :**: Op k))
                               (Swap k (Op k)))
                        :.: Tuple k (Op k)))))
      :*: y)
     z
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj (Presheaves k) y
-> Obj (Presheaves k) z -> PShExponential k y z
forall (k :: * -> * -> *) y z.
Category k =>
Obj (Presheaves k) y
-> Obj (Presheaves k) z -> PShExponential k y z
PshExponential Obj (Presheaves k) y
yn Obj (Presheaves k) z
zn ((Presheaves k :-*: z)
 :.: Opposite
       ((ProductFunctor (Presheaves k)
         :.: Tuple2 (Presheaves k) (Presheaves k) y)
        :.: ((FunctorCompose (Op k) (Op k :**: k) (->)
              :.: Tuple1
                    (Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
             :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
                   :.: Tuple1
                         (Nat (k :**: Op k) (Op k :**: k))
                         (Nat (Op k) (k :**: Op k))
                         (Swap k (Op k)))
                  :.: Tuple k (Op k)))))
-> y
-> ((Presheaves k :-*: z)
    :.: Opposite
          ((ProductFunctor (Presheaves k)
            :.: Tuple2 (Presheaves k) (Presheaves k) y)
           :.: ((FunctorCompose (Op k) (Op k :**: k) (->)
                 :.: Tuple1
                       (Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
                :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
                      :.: Tuple1
                            (Nat (k :**: Op k) (Op k :**: k))
                            (Nat (Op k) (k :**: Op k))
                            (Swap k (Op k)))
                     :.: Tuple k (Op k)))))
   :*: y
forall p q (k :: * -> * -> *).
(Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k,
 HasBinaryProducts k) =>
p -> q -> p :*: q
:*: y
y) z
z (\(Op i) (Nat
  (Op k)
  (->)
  ((Hom k
    :.: (Swap k (Op k)
         :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
   :*: y)
  z
n, y :% z
yi) -> (Nat
  (Op k)
  (->)
  ((Hom k
    :.: (Swap k (Op k)
         :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
   :*: y)
  z
n Nat
  (Op k)
  (->)
  ((Hom k
    :.: (Swap k (Op k)
         :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
   :*: y)
  z
-> Obj (Op k) z
-> (((Hom k
      :.: (Swap k (Op k)
           :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
     :*: y)
    :% z)
-> z :% z
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! k z z -> Obj (Op k) z
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op k z z
i) (k z z
i, y :% z
yi))
  tuple :: Obj (Presheaves k) y
-> Obj (Presheaves k) z
-> Presheaves
     k
     z
     (Exponential (Presheaves k) y (BinaryProduct (Presheaves k) z y))
tuple Obj (Presheaves k) y
yn zn :: Obj (Presheaves k) z
zn@(Nat z
z z
_ forall z. Obj (Op k) z -> Component z z z
_) = z
-> ((Presheaves k :-*: (z :*: y))
    :.: Opposite
          ((ProductFunctor (Presheaves k)
            :.: Tuple2 (Presheaves k) (Presheaves k) y)
           :.: ((FunctorCompose (Op k) (Op k :**: k) (->)
                 :.: Tuple1
                       (Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
                :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
                      :.: Tuple1
                            (Nat (k :**: Op k) (Op k :**: k))
                            (Nat (Op k) (k :**: Op k))
                            (Swap k (Op k)))
                     :.: Tuple k (Op k)))))
-> (forall z.
    Obj (Op k) z
    -> Component
         z
         ((Presheaves k :-*: (z :*: y))
          :.: Opposite
                ((ProductFunctor (Presheaves k)
                  :.: Tuple2 (Presheaves k) (Presheaves k) y)
                 :.: ((FunctorCompose (Op k) (Op k :**: k) (->)
                       :.: Tuple1
                             (Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
                      :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
                            :.: Tuple1
                                  (Nat (k :**: Op k) (Op k :**: k))
                                  (Nat (Op k) (k :**: Op k))
                                  (Swap k (Op k)))
                           :.: Tuple k (Op k)))))
         z)
-> Nat
     (Op k)
     (->)
     z
     ((Presheaves k :-*: (z :*: y))
      :.: Opposite
            ((ProductFunctor (Presheaves k)
              :.: Tuple2 (Presheaves k) (Presheaves k) y)
             :.: ((FunctorCompose (Op k) (Op k :**: k) (->)
                   :.: Tuple1
                         (Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
                  :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
                        :.: Tuple1
                              (Nat (k :**: Op k) (Op k :**: k))
                              (Nat (Op k) (k :**: Op k))
                              (Swap k (Op k)))
                       :.: Tuple k (Op k)))))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat z
z (Obj (Presheaves k) y
-> Obj (Presheaves k) (z :*: y) -> PShExponential k y (z :*: y)
forall (k :: * -> * -> *) y z.
Category k =>
Obj (Presheaves k) y
-> Obj (Presheaves k) z -> PShExponential k y z
PshExponential Obj (Presheaves k) y
yn (Obj (Presheaves k) z
zn Obj (Presheaves k) z
-> Obj (Presheaves k) y
-> Nat
     (Op k)
     (->)
     (BinaryProduct (Presheaves k) z y)
     (BinaryProduct (Presheaves k) z y)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** Obj (Presheaves k) y
yn)) (\(Op i) z :% z
zi -> ((k :-*: z)
-> z
-> (forall z. Obj (Op k) z -> Component (k :-*: z) z z)
-> Nat (Op k) (->) (k :-*: z) z
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj k z -> k :-*: z
forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
Hom_X Obj k z
i) z
z (\Obj (Op k) z
_ k z z
j2i -> (z
z z -> Dom z z z -> Cod z (z :% z) (z :% z)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% k z z -> Op k z z
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op k z z
j2i) z :% z
zi) Nat (Op k) (->) (k :-*: z) z
-> Obj (Presheaves k) y
-> Nat
     (Op k)
     (->)
     (BinaryProduct (Presheaves k) (k :-*: z) y)
     (BinaryProduct (Presheaves k) z y)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** Obj (Presheaves k) y
yn))
  Presheaves k z1 z2
zn ^^^ :: Presheaves k z1 z2
-> Presheaves k y2 y1
-> Presheaves
     k
     (Exponential (Presheaves k) y1 z1)
     (Exponential (Presheaves k) y2 z2)
^^^ Presheaves k y2 y1
yn = ((Presheaves k :-*: z1)
 :.: Opposite
       ((ProductFunctor (Presheaves k)
         :.: Tuple2 (Presheaves k) (Presheaves k) y1)
        :.: ((FunctorCompose (Op k) (Op k :**: k) (->)
              :.: Tuple1
                    (Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
             :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
                   :.: Tuple1
                         (Nat (k :**: Op k) (Op k :**: k))
                         (Nat (Op k) (k :**: Op k))
                         (Swap k (Op k)))
                  :.: Tuple k (Op k)))))
-> ((Presheaves k :-*: z2)
    :.: Opposite
          ((ProductFunctor (Presheaves k)
            :.: Tuple2 (Presheaves k) (Presheaves k) y2)
           :.: ((FunctorCompose (Op k) (Op k :**: k) (->)
                 :.: Tuple1
                       (Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
                :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
                      :.: Tuple1
                            (Nat (k :**: Op k) (Op k :**: k))
                            (Nat (Op k) (k :**: Op k))
                            (Swap k (Op k)))
                     :.: Tuple k (Op k)))))
-> (forall z.
    Obj (Op k) z
    -> Component
         ((Presheaves k :-*: z1)
          :.: Opposite
                ((ProductFunctor (Presheaves k)
                  :.: Tuple2 (Presheaves k) (Presheaves k) y1)
                 :.: ((FunctorCompose (Op k) (Op k :**: k) (->)
                       :.: Tuple1
                             (Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
                      :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
                            :.: Tuple1
                                  (Nat (k :**: Op k) (Op k :**: k))
                                  (Nat (Op k) (k :**: Op k))
                                  (Swap k (Op k)))
                           :.: Tuple k (Op k)))))
         ((Presheaves k :-*: z2)
          :.: Opposite
                ((ProductFunctor (Presheaves k)
                  :.: Tuple2 (Presheaves k) (Presheaves k) y2)
                 :.: ((FunctorCompose (Op k) (Op k :**: k) (->)
                       :.: Tuple1
                             (Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
                      :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
                            :.: Tuple1
                                  (Nat (k :**: Op k) (Op k :**: k))
                                  (Nat (Op k) (k :**: Op k))
                                  (Swap k (Op k)))
                           :.: Tuple k (Op k)))))
         z)
-> Nat
     (Op k)
     (->)
     ((Presheaves k :-*: z1)
      :.: Opposite
            ((ProductFunctor (Presheaves k)
              :.: Tuple2 (Presheaves k) (Presheaves k) y1)
             :.: ((FunctorCompose (Op k) (Op k :**: k) (->)
                   :.: Tuple1
                         (Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
                  :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
                        :.: Tuple1
                              (Nat (k :**: Op k) (Op k :**: k))
                              (Nat (Op k) (k :**: Op k))
                              (Swap k (Op k)))
                       :.: Tuple k (Op k)))))
     ((Presheaves k :-*: z2)
      :.: Opposite
            ((ProductFunctor (Presheaves k)
              :.: Tuple2 (Presheaves k) (Presheaves k) y2)
             :.: ((FunctorCompose (Op k) (Op k :**: k) (->)
                   :.: Tuple1
                         (Nat (Op k :**: k) (->)) (Nat (Op k) (Op k :**: k)) (Hom k))
                  :.: ((FunctorCompose (Op k) (k :**: Op k) (Op k :**: k)
                        :.: Tuple1
                              (Nat (k :**: Op k) (Op k :**: k))
                              (Nat (Op k) (k :**: Op k))
                              (Swap k (Op k)))
                       :.: Tuple k (Op k)))))
forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (Obj (Presheaves k) y1
-> Obj (Presheaves k) z1 -> PShExponential k y1 z1
forall (k :: * -> * -> *) y z.
Category k =>
Obj (Presheaves k) y
-> Obj (Presheaves k) z -> PShExponential k y z
PshExponential (Presheaves k y2 y1 -> Obj (Presheaves k) y1
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Presheaves k y2 y1
yn) (Presheaves k z1 z2 -> Obj (Presheaves k) z1
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Presheaves k z1 z2
zn)) (Obj (Presheaves k) y2
-> Obj (Presheaves k) z2 -> PShExponential k y2 z2
forall (k :: * -> * -> *) y z.
Category k =>
Obj (Presheaves k) y
-> Obj (Presheaves k) z -> PShExponential k y z
PshExponential (Presheaves k y2 y1 -> Obj (Presheaves k) y2
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src Presheaves k y2 y1
yn) (Presheaves k z1 z2 -> Obj (Presheaves k) z2
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt Presheaves k z1 z2
zn)) (\(Op i) Nat
  (Op k)
  (->)
  ((Hom k
    :.: (Swap k (Op k)
         :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
   :*: y1)
  z1
n -> Presheaves k z1 z2
zn Presheaves k z1 z2
-> Nat
     (Op k)
     (->)
     ((Hom k
       :.: (Swap k (Op k)
            :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
      :*: y2)
     z1
-> Nat
     (Op k)
     (->)
     ((Hom k
       :.: (Swap k (Op k)
            :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
      :*: y2)
     z2
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Nat
  (Op k)
  (->)
  ((Hom k
    :.: (Swap k (Op k)
         :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
   :*: y1)
  z1
n Nat
  (Op k)
  (->)
  ((Hom k
    :.: (Swap k (Op k)
         :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
   :*: y1)
  z1
-> Nat
     (Op k)
     (->)
     ((Hom k
       :.: (Swap k (Op k)
            :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
      :*: y2)
     ((Hom k
       :.: (Swap k (Op k)
            :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
      :*: y1)
-> Nat
     (Op k)
     (->)
     ((Hom k
       :.: (Swap k (Op k)
            :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
      :*: y2)
     z1
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. ((Hom k
 :.: (Swap k (Op k)
      :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
-> Nat
     (Dom
        (Hom k
         :.: (Swap k (Op k)
              :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k)))))
     (Cod
        (Hom k
         :.: (Swap k (Op k)
              :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k)))))
     (Hom k
      :.: (Swap k (Op k)
           :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
     (Hom k
      :.: (Swap k (Op k)
           :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId (Obj k z
-> Hom k
   :.: (Swap k (Op k)
        :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k)))
forall (k :: * -> * -> *) x. Category k => Obj k x -> k :-*: x
Hom_X Obj k z
i) Nat
  (Op k)
  (->)
  (Hom k
   :.: (Swap k (Op k)
        :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
  (Hom k
   :.: (Swap k (Op k)
        :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
-> Presheaves k y2 y1
-> Nat
     (Op k)
     (->)
     (BinaryProduct
        (Presheaves k)
        (Hom k
         :.: (Swap k (Op k)
              :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
        y2)
     (BinaryProduct
        (Presheaves k)
        (Hom k
         :.: (Swap k (Op k)
              :.: ((Const (Op k) k z :***: Id (Op k)) :.: DiagProd (Op k))))
        y1)
forall k (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** Presheaves k y2 y1
yn))



-- | The product functor is left adjoint the the exponential functor.
curryAdj :: CartesianClosed k
         => Obj k y
         -> Adjunction k k
              (ProductFunctor k :.: Tuple2 k k y)
              (ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj :: Obj k y
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k y)
     (ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k y
y = (ProductFunctor k :.: Tuple2 k k y)
-> (ExpFunctor k :.: Tuple1 (Op k) k y)
-> (forall a.
    Obj k a
    -> Component
         (Id k)
         ((ExpFunctor k :.: Tuple1 (Op k) k y)
          :.: (ProductFunctor k :.: Tuple2 k k y))
         a)
-> (forall a.
    Obj k a
    -> Component
         ((ProductFunctor k :.: Tuple2 k k y)
          :.: (ExpFunctor k :.: Tuple1 (Op k) k y))
         (Id k)
         a)
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k y)
     (ExpFunctor k :.: Tuple1 (Op k) k y)
forall f g (d :: * -> * -> *) (c :: * -> * -> *).
(Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c,
 Cod g ~ d) =>
f
-> g
-> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
-> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
-> Adjunction c d f g
mkAdjunctionUnits (ProductFunctor k
forall (k :: * -> * -> *). ProductFunctor k
ProductFunctor ProductFunctor k
-> Tuple2 k k y -> ProductFunctor k :.: Tuple2 k k y
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: Obj k y -> Tuple2 k k y
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a.
(Category c1, Category c2) =>
Obj c2 a -> Tuple2 c1 c2 a
Tuple2 Obj k y
y) (ExpFunctor k
forall (k :: * -> * -> *). ExpFunctor k
ExpFunctor ExpFunctor k
-> Tuple1 (Op k) k y -> ExpFunctor k :.: Tuple1 (Op k) k y
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: Obj (Op k) y -> Tuple1 (Op k) k y
forall (c1 :: * -> * -> *) (c2 :: * -> * -> *) a.
(Category c1, Category c2) =>
Obj c1 a -> Tuple1 c1 c2 a
Tuple1 (Obj k y -> Obj (Op k) y
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op Obj k y
y)) (Obj k y -> k a a -> k a (Exponential k y (BinaryProduct k a y))
forall k (k :: k -> k -> *) (y :: k) (z :: k).
CartesianClosed k =>
Obj k y -> Obj k z -> k z (Exponential k y (BinaryProduct k z y))
tuple Obj k y
y) (Obj k y -> k a a -> k (BinaryProduct k (Exponential k y a) y) a
forall k (k :: k -> k -> *) (y :: k) (z :: k).
CartesianClosed k =>
Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z
apply Obj k y
y)

-- | From the adjunction between the product functor and the exponential functor we get the curry and uncurry functions,
--   generalized to any cartesian closed category.
curry :: (CartesianClosed k, Kind k ~ *) => Obj k x -> Obj k y -> Obj k z -> k (BinaryProduct k x y) z -> k x (Exponential k y z)
curry :: Obj k x
-> Obj k y
-> Obj k z
-> k (BinaryProduct k x y) z
-> k x (Exponential k y z)
curry Obj k x
x Obj k y
y Obj k z
_ = Adjunction
  k
  k
  (ProductFunctor k :.: Tuple2 k k y)
  (ExpFunctor k :.: Tuple1 (Op k) k y)
-> Obj k x
-> k ((ProductFunctor k :.: Tuple2 k k y) :% x) z
-> k x ((ExpFunctor k :.: Tuple1 (Op k) k y) :% z)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
Adjunction c d f g -> Obj d a -> c (f :% a) b -> d a (g :% b)
leftAdjunct (Obj k y
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k y)
     (ExpFunctor k :.: Tuple1 (Op k) k y)
forall (k :: * -> * -> *) y.
CartesianClosed k =>
Obj k y
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k y)
     (ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k y
y) Obj k x
x

uncurry :: (CartesianClosed k, Kind k ~ *) => Obj k x -> Obj k y -> Obj k z -> k x (Exponential k y z) -> k (BinaryProduct k x y) z
uncurry :: Obj k x
-> Obj k y
-> Obj k z
-> k x (Exponential k y z)
-> k (BinaryProduct k x y) z
uncurry Obj k x
_ Obj k y
y Obj k z
z = Adjunction
  k
  k
  (ProductFunctor k :.: Tuple2 k k y)
  (ExpFunctor k :.: Tuple1 (Op k) k y)
-> Obj k z
-> k x ((ExpFunctor k :.: Tuple1 (Op k) k y) :% z)
-> k ((ProductFunctor k :.: Tuple2 k k y) :% x) z
forall (c :: * -> * -> *) (d :: * -> * -> *) f g b a.
Adjunction c d f g -> Obj c b -> d a (g :% b) -> c (f :% a) b
rightAdjunct (Obj k y
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k y)
     (ExpFunctor k :.: Tuple1 (Op k) k y)
forall (k :: * -> * -> *) y.
CartesianClosed k =>
Obj k y
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k y)
     (ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k y
y) Obj k z
z

-- | From every adjunction we get a monad, in this case the State monad.
type State k s a = Exponential k s (BinaryProduct k a s)

stateMonadReturn :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k a (State k s a)
stateMonadReturn :: Obj k s -> Obj k a -> k a (State k s a)
stateMonadReturn Obj k s
s Obj k a
a = MonoidObject
  (EndoFunctorCompose k)
  ((ExpFunctor k :.: Tuple1 (Op k) k s)
   :.: (ProductFunctor k :.: Tuple2 k k s))
-> Cod
     (EndoFunctorCompose k)
     (Unit (EndoFunctorCompose k))
     ((ExpFunctor k :.: Tuple1 (Op k) k s)
      :.: (ProductFunctor k :.: Tuple2 k k s))
forall f a. MonoidObject f a -> Cod f (Unit f) a
M.unit (Adjunction
  k
  k
  (ProductFunctor k :.: Tuple2 k k s)
  (ExpFunctor k :.: Tuple1 (Op k) k s)
-> Monad
     ((ExpFunctor k :.: Tuple1 (Op k) k s)
      :.: (ProductFunctor k :.: Tuple2 k k s))
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Monad (g :.: f)
adjunctionMonad (Obj k s
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k s)
     (ExpFunctor k :.: Tuple1 (Op k) k s)
forall (k :: * -> * -> *) y.
CartesianClosed k =>
Obj k y
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k y)
     (ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k s
s)) Nat
  k
  k
  (Id k)
  ((ExpFunctor k :.: Tuple1 (Op k) k s)
   :.: (ProductFunctor k :.: Tuple2 k k s))
-> Obj k a
-> k (Id k :% a)
     (((ExpFunctor k :.: Tuple1 (Op k) k s)
       :.: (ProductFunctor k :.: Tuple2 k k s))
      :% a)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj k a
a

stateMonadJoin :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k (State k s (State k s a)) (State k s a)
stateMonadJoin :: Obj k s -> Obj k a -> k (State k s (State k s a)) (State k s a)
stateMonadJoin Obj k s
s Obj k a
a = MonoidObject
  (EndoFunctorCompose k)
  ((ExpFunctor k :.: Tuple1 (Op k) k s)
   :.: (ProductFunctor k :.: Tuple2 k k s))
-> Cod
     (EndoFunctorCompose k)
     (EndoFunctorCompose k
      :% ((ExpFunctor k :.: Tuple1 (Op k) k s)
          :.: (ProductFunctor k :.: Tuple2 k k s),
          (ExpFunctor k :.: Tuple1 (Op k) k s)
          :.: (ProductFunctor k :.: Tuple2 k k s)))
     ((ExpFunctor k :.: Tuple1 (Op k) k s)
      :.: (ProductFunctor k :.: Tuple2 k k s))
forall f a. MonoidObject f a -> Cod f (f :% (a, a)) a
M.multiply (Adjunction
  k
  k
  (ProductFunctor k :.: Tuple2 k k s)
  (ExpFunctor k :.: Tuple1 (Op k) k s)
-> Monad
     ((ExpFunctor k :.: Tuple1 (Op k) k s)
      :.: (ProductFunctor k :.: Tuple2 k k s))
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Monad (g :.: f)
adjunctionMonad (Obj k s
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k s)
     (ExpFunctor k :.: Tuple1 (Op k) k s)
forall (k :: * -> * -> *) y.
CartesianClosed k =>
Obj k y
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k y)
     (ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k s
s)) Nat
  k
  k
  (((ExpFunctor k :.: Tuple1 (Op k) k s)
    :.: (ProductFunctor k :.: Tuple2 k k s))
   :.: ((ExpFunctor k :.: Tuple1 (Op k) k s)
        :.: (ProductFunctor k :.: Tuple2 k k s)))
  ((ExpFunctor k :.: Tuple1 (Op k) k s)
   :.: (ProductFunctor k :.: Tuple2 k k s))
-> Obj k a
-> k ((((ExpFunctor k :.: Tuple1 (Op k) k s)
        :.: (ProductFunctor k :.: Tuple2 k k s))
       :.: ((ExpFunctor k :.: Tuple1 (Op k) k s)
            :.: (ProductFunctor k :.: Tuple2 k k s)))
      :% a)
     (((ExpFunctor k :.: Tuple1 (Op k) k s)
       :.: (ProductFunctor k :.: Tuple2 k k s))
      :% a)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj k a
a

-- ! From every adjunction we also get a comonad, the Context comonad in this case.
type Context k s a = BinaryProduct k (Exponential k s a) s

contextComonadExtract :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k (Context k s a) a
contextComonadExtract :: Obj k s -> Obj k a -> k (Context k s a) a
contextComonadExtract Obj k s
s Obj k a
a = ComonoidObject
  (EndoFunctorCompose k)
  ((ProductFunctor k :.: Tuple2 k k s)
   :.: (ExpFunctor k :.: Tuple1 (Op k) k s))
-> Cod
     (EndoFunctorCompose k)
     ((ProductFunctor k :.: Tuple2 k k s)
      :.: (ExpFunctor k :.: Tuple1 (Op k) k s))
     (Unit (EndoFunctorCompose k))
forall f a. ComonoidObject f a -> Cod f a (Unit f)
M.counit (Adjunction
  k
  k
  (ProductFunctor k :.: Tuple2 k k s)
  (ExpFunctor k :.: Tuple1 (Op k) k s)
-> Comonad
     ((ProductFunctor k :.: Tuple2 k k s)
      :.: (ExpFunctor k :.: Tuple1 (Op k) k s))
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Comonad (f :.: g)
adjunctionComonad (Obj k s
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k s)
     (ExpFunctor k :.: Tuple1 (Op k) k s)
forall (k :: * -> * -> *) y.
CartesianClosed k =>
Obj k y
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k y)
     (ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k s
s)) Nat
  k
  k
  ((ProductFunctor k :.: Tuple2 k k s)
   :.: (ExpFunctor k :.: Tuple1 (Op k) k s))
  (Id k)
-> Obj k a
-> k (((ProductFunctor k :.: Tuple2 k k s)
       :.: (ExpFunctor k :.: Tuple1 (Op k) k s))
      :% a)
     (Id k :% a)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj k a
a

contextComonadDuplicate :: (CartesianClosed k, Kind k ~ *) => Obj k s -> Obj k a -> k (Context k s a) (Context k s (Context k s a))
contextComonadDuplicate :: Obj k s
-> Obj k a -> k (Context k s a) (Context k s (Context k s a))
contextComonadDuplicate Obj k s
s Obj k a
a = ComonoidObject
  (EndoFunctorCompose k)
  ((ProductFunctor k :.: Tuple2 k k s)
   :.: (ExpFunctor k :.: Tuple1 (Op k) k s))
-> Cod
     (EndoFunctorCompose k)
     ((ProductFunctor k :.: Tuple2 k k s)
      :.: (ExpFunctor k :.: Tuple1 (Op k) k s))
     (EndoFunctorCompose k
      :% ((ProductFunctor k :.: Tuple2 k k s)
          :.: (ExpFunctor k :.: Tuple1 (Op k) k s),
          (ProductFunctor k :.: Tuple2 k k s)
          :.: (ExpFunctor k :.: Tuple1 (Op k) k s)))
forall f a. ComonoidObject f a -> Cod f a (f :% (a, a))
M.comultiply (Adjunction
  k
  k
  (ProductFunctor k :.: Tuple2 k k s)
  (ExpFunctor k :.: Tuple1 (Op k) k s)
-> Comonad
     ((ProductFunctor k :.: Tuple2 k k s)
      :.: (ExpFunctor k :.: Tuple1 (Op k) k s))
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Comonad (f :.: g)
adjunctionComonad (Obj k s
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k s)
     (ExpFunctor k :.: Tuple1 (Op k) k s)
forall (k :: * -> * -> *) y.
CartesianClosed k =>
Obj k y
-> Adjunction
     k
     k
     (ProductFunctor k :.: Tuple2 k k y)
     (ExpFunctor k :.: Tuple1 (Op k) k y)
curryAdj Obj k s
s)) Nat
  k
  k
  ((ProductFunctor k :.: Tuple2 k k s)
   :.: (ExpFunctor k :.: Tuple1 (Op k) k s))
  (((ProductFunctor k :.: Tuple2 k k s)
    :.: (ExpFunctor k :.: Tuple1 (Op k) k s))
   :.: ((ProductFunctor k :.: Tuple2 k k s)
        :.: (ExpFunctor k :.: Tuple1 (Op k) k s)))
-> Obj k a
-> k (((ProductFunctor k :.: Tuple2 k k s)
       :.: (ExpFunctor k :.: Tuple1 (Op k) k s))
      :% a)
     ((((ProductFunctor k :.: Tuple2 k k s)
        :.: (ExpFunctor k :.: Tuple1 (Op k) k s))
       :.: ((ProductFunctor k :.: Tuple2 k k s)
            :.: (ExpFunctor k :.: Tuple1 (Op k) k s)))
      :% a)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Obj k a
a