    {-# LANGUAGE CPP #-}
    #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
    {-# LANGUAGE Trustworthy #-}
    #endif
    {-# LANGUAGE TypeFamilies, MultiParamTypeClasses, TypeOperators, FlexibleContexts #-}
    -------------------------------------------------------------------------------------------
    -- |
    -- Module     : Control.Category.Cartesian.Closed
    -- Copyright  : 2008 Edward Kmett
    -- License    : BSD
    --
    -- Maintainer : Edward Kmett <ekmett@gmail.com>
    -- Stability  : experimental
    -- Portability: non-portable (class-associated types)
    --
    -------------------------------------------------------------------------------------------
    module Control.Category.Cartesian.Closed
        (
        -- * Cartesian Closed Category
          CCC(..)
        , unitCCC, counitCCC
        -- * Co-(Cartesian Closed Category)
        , CoCCC(..)
        , unitCoCCC, counitCoCCC
        ) where

    import Prelude ()
    import qualified Prelude

    import Control.Category
    import Control.Category.Braided
    import Control.Category.Cartesian

    -- * Closed Cartesian Category

    -- | A 'CCC' has full-fledged monoidal finite products and exponentials

    -- Ideally you also want an instance for @'Bifunctor' ('Exp' hom) ('Dual' hom) hom hom@.
    -- or at least @'Functor' ('Exp' hom a) hom hom@, which cannot be expressed in the constraints here.

    class Cartesian k => CCC k where
        type Exp k :: * -> * -> *
        apply :: Product k (Exp k a b) a `k` b
        curry :: Product k a b `k` c -> a `k` Exp k b c
        uncurry :: a `k` Exp k b c -> Product k a b `k` c

    instance CCC (->) where
      type Exp (->) = (->)
      apply :: forall a b. Product (->) (Exp (->) a b) a -> b
    apply (a -> b
    f,a
    a) = a -> b
    f a
    a
      curry :: forall a b c. (Product (->) a b -> c) -> a -> Exp (->) b c
    curry = ((a, b) -> c) -> a -> b -> c
    (Product (->) a b -> c) -> a -> Exp (->) b c
    forall a b c. ((a, b) -> c) -> a -> b -> c
    Prelude.curry
      uncurry :: forall a b c. (a -> Exp (->) b c) -> Product (->) a b -> c
    uncurry = (a -> Exp (->) b c) -> Product (->) a b -> c
    (a -> b -> c) -> (a, b) -> c
    forall a b c. (a -> b -> c) -> (a, b) -> c
    Prelude.uncurry

    {-# RULES
    "curry apply"         curry apply = id
    -- "curry . uncurry"     curry . uncurry = id
    -- "uncurry . curry"     uncurry . curry = id
     #-}

    -- * Free @'Adjunction' (Product (<=) a) (Exp (<=) a) (<=) (<=)@
    unitCCC :: CCC k => a `k` Exp k b (Product k b a)
    unitCCC :: forall (k :: * -> * -> *) a b.
    CCC k =>
    k a (Exp k b (Product k b a))
    unitCCC = k (Product k a b) (Product k b a) -> k a (Exp k b (Product k b a))
    forall a b c. k (Product k a b) c -> k a (Exp k b c)
    forall (k :: * -> * -> *) a b c.
    CCC k =>
    k (Product k a b) c -> k a (Exp k b c)
    curry k (Product k a b) (Product k b a)
    forall a b. k (Product k a b) (Product k b a)
    forall (k :: * -> * -> *) (p :: * -> * -> *) a b.
    Braided k p =>
    k (p a b) (p b a)
    braid

    counitCCC :: CCC k => Product k b (Exp k b a) `k` a
    counitCCC :: forall (k :: * -> * -> *) b a.
    CCC k =>
    k (Product k b (Exp k b a)) a
    counitCCC = k (Product k (Exp k b a) b) a
    forall a b. k (Product k (Exp k a b) a) b
    forall (k :: * -> * -> *) a b.
    CCC k =>
    k (Product k (Exp k a b) a) b
    apply k (Product k (Exp k b a) b) a
    -> k (Product k b (Exp k b a)) (Product k (Exp k b a) b)
    -> k (Product k b (Exp k b a)) a
    forall b c a. k b c -> k a b -> k a c
    forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . k (Product k b (Exp k b a)) (Product k (Exp k b a) b)
    forall a b. k (Product k a b) (Product k b a)
    forall (k :: * -> * -> *) (p :: * -> * -> *) a b.
    Braided k p =>
    k (p a b) (p b a)
    braid

    -- * A Co-(Closed Cartesian Category)

    -- | A Co-CCC has full-fledged comonoidal finite coproducts and coexponentials

    -- You probably also want an instance for @'Bifunctor' ('coexp' hom) ('Dual' hom) hom hom@.

    class CoCartesian k => CoCCC k where
        type Coexp k :: * -> * -> *
        coapply :: b `k` Sum k (Coexp k a b) a
        cocurry :: c `k` Sum k a b -> Coexp k b c `k` a
        uncocurry :: Coexp k b c `k` a -> c `k` Sum k a b

    {-# RULES
    "cocurry coapply" cocurry coapply = id
    -- "cocurry . uncocurry"   cocurry . uncocurry = id
    -- "uncocurry . cocurry"   uncocurry . cocurry = id
     #-}

    -- * Free @'Adjunction' ('Coexp' (<=) a) ('Sum' (<=) a) (<=) (<=)@
    unitCoCCC :: CoCCC k => a `k` Sum k b (Coexp k b a)
    unitCoCCC :: forall (k :: * -> * -> *) a b.
    CoCCC k =>
    k a (Sum k b (Coexp k b a))
    unitCoCCC = k (Sum k (Coexp k b a) b) (Sum k b (Coexp k b a))
    forall (k :: * -> * -> *) (p :: * -> * -> *) a b.
    Symmetric k p =>
    k (p a b) (p b a)
    swap k (Sum k (Coexp k b a) b) (Sum k b (Coexp k b a))
    -> k a (Sum k (Coexp k b a) b) -> k a (Sum k b (Coexp k b a))
    forall b c a. k b c -> k a b -> k a c
    forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
    Category cat =>
    cat b c -> cat a b -> cat a c
    . k a (Sum k (Coexp k b a) b)
    forall b a. k b (Sum k (Coexp k a b) a)
    forall (k :: * -> * -> *) b a.
    CoCCC k =>
    k b (Sum k (Coexp k a b) a)
    coapply

    counitCoCCC :: CoCCC k => Coexp k b (Sum k b a) `k` a
    counitCoCCC :: forall (k :: * -> * -> *) b a.
    CoCCC k =>
    k (Coexp k b (Sum k b a)) a
    counitCoCCC = k (Sum k b a) (Sum k a b) -> k (Coexp k b (Sum k b a)) a
    forall c a b. k c (Sum k a b) -> k (Coexp k b c) a
    forall (k :: * -> * -> *) c a b.
    CoCCC k =>
    k c (Sum k a b) -> k (Coexp k b c) a
    cocurry k (Sum k b a) (Sum k a b)
    forall (k :: * -> * -> *) (p :: * -> * -> *) a b.
    Symmetric k p =>
    k (p a b) (p b a)
    swap