    {-# LANGUAGE CPP #-}
    #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
    {-# LANGUAGE Trustworthy #-}
    #endif
    {-# LANGUAGE TypeFamilies, MultiParamTypeClasses, TypeOperators, FlexibleContexts, FlexibleInstances, UndecidableInstances #-}
    -------------------------------------------------------------------------------------------
    -- |
    -- Module    : Control.Category.Cartesian
    -- Copyright : 2008-2010 Edward Kmett
    -- License   : BSD
    --
    -- Maintainer  : Edward Kmett <ekmett@gmail.com>
    -- Stability   : experimental
    -- Portability : non-portable (class-associated types)
    --
    -------------------------------------------------------------------------------------------
    module Control.Category.Cartesian
        (
        -- * (Co)Cartesian categories
          Cartesian(..)
        , bimapProduct, braidProduct, associateProduct, disassociateProduct
        , CoCartesian(..)
        , bimapSum, braidSum, associateSum, disassociateSum
        ) where

    import Control.Category.Braided
    import Control.Category.Monoidal
    import Prelude hiding (Functor, map, (.), id, fst, snd, curry, uncurry)
    import qualified Prelude (fst,snd)
    import Control.Categorical.Bifunctor
    import Control.Category

    infixr 3 &&&
    infixr 2 |||

    {- |
    Minimum definition:

    > fst, snd, diag
    > fst, snd, (&&&)
    -}
    class (Symmetric k (Product k), Monoidal k (Product k)) => Cartesian k where
        type Product k :: * -> * -> *
        fst :: Product k a b `k` a
        snd :: Product k a b `k` b
        diag :: a `k` Product k a a
        (&&&) :: (a `k` b) -> (a `k` c) -> a `k` Product k b c

        diag = k a a
    forall a. k a a
    forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id k a a -> k a a -> k a (Product k a a)
    forall a b c. k a b -> k a c -> k a (Product k b c)
    forall (k :: * -> * -> *) a b c.
    Cartesian k =>
    k a b -> k a c -> k a (Product k b c)
    &&& k a a
    forall a. k a a
    forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id
        k a b
    f &&& k a c
    g = k a b -> k a c -> k (Product k a a) (Product k b c)
    forall a b c d. k a b -> k c d -> k (Product k a c) (Product k b d)
    forall (p :: * -> * -> *) (r :: * -> * -> *) (s :: * -> * -> *)
           (t :: * -> * -> *) a b c d.
    Bifunctor p r s t =>
    r a b -> s c d -> t (p a c) (p b d)
    bimap k a b
    f k a c
    g k (Product k a a) (Product k b c)
    -> k a (Product k a a) -> k a (Product k b c)
    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 (Product k a a)
    forall a. k a (Product k a a)
    forall (k :: * -> * -> *) a. Cartesian k => k a (Product k a a)
    diag

    {-- RULES
    "fst . diag"      fst . diag = id
    "snd . diag"    snd . diag = id
    "fst . f &&& g" forall f g. fst . (f &&& g) = f
    "snd . f &&& g" forall f g. snd . (f &&& g) = g
     --}

    instance Cartesian (->) where
        type Product (->) = (,)
        fst :: forall a b. Product (->) a b -> a
    fst = (a, b) -> a
    Product (->) a b -> a
    forall a b. (a, b) -> a
    Prelude.fst
        snd :: forall a b. Product (->) a b -> b
    snd = (a, b) -> b
    Product (->) a b -> b
    forall a b. (a, b) -> b
    Prelude.snd
        diag :: forall a. a -> Product (->) a a
    diag a
    a = (a
    a,a
    a)
        (a -> b
    f &&& :: forall a b c. (a -> b) -> (a -> c) -> a -> Product (->) b c
    &&& a -> c
    g) a
    a = (a -> b
    f a
    a, a -> c
    g a
    a)

    -- | free construction of 'Bifunctor' for the product 'Bifunctor' @Product k@ if @(&&&)@ is known
    bimapProduct :: Cartesian k => k a c -> k b d -> Product k a b `k` Product k c d
    bimapProduct :: forall (k :: * -> * -> *) a c b d.
    Cartesian k =>
    k a c -> k b d -> k (Product k a b) (Product k c d)
    bimapProduct k a c
    f k b d
    g = (k a c
    f k a c -> k (Product k a b) a -> k (Product k a b) c
    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 a b) a
    forall a b. k (Product k a b) a
    forall (k :: * -> * -> *) a b. Cartesian k => k (Product k a b) a
    fst) k (Product k a b) c
    -> k (Product k a b) d -> k (Product k a b) (Product k c d)
    forall a b c. k a b -> k a c -> k a (Product k b c)
    forall (k :: * -> * -> *) a b c.
    Cartesian k =>
    k a b -> k a c -> k a (Product k b c)
    &&& (k b d
    g k b d -> k (Product k a b) b -> k (Product k a b) d
    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 a b) b
    forall a b. k (Product k a b) b
    forall (k :: * -> * -> *) a b. Cartesian k => k (Product k a b) b
    snd)

    -- | free construction of 'Braided' for the product 'Bifunctor' @Product k@
    braidProduct :: Cartesian k => k (Product k a b) (Product k b a)
    braidProduct :: forall (k :: * -> * -> *) a b.
    Cartesian k =>
    k (Product k a b) (Product k b a)
    braidProduct = k (Product k a b) b
    forall a b. k (Product k a b) b
    forall (k :: * -> * -> *) a b. Cartesian k => k (Product k a b) b
    snd k (Product k a b) b
    -> k (Product k a b) a -> k (Product k a b) (Product k b a)
    forall a b c. k a b -> k a c -> k a (Product k b c)
    forall (k :: * -> * -> *) a b c.
    Cartesian k =>
    k a b -> k a c -> k a (Product k b c)
    &&& k (Product k a b) a
    forall a b. k (Product k a b) a
    forall (k :: * -> * -> *) a b. Cartesian k => k (Product k a b) a
    fst

    -- | free construction of 'Associative' for the product 'Bifunctor' @Product k@
    associateProduct :: Cartesian k => Product k (Product k a b) c `k` Product k a (Product k b c)
    associateProduct :: forall (k :: * -> * -> *) a b c.
    Cartesian k =>
    k (Product k (Product k a b) c) (Product k a (Product k b c))
    associateProduct = (k (Product k a b) a
    forall a b. k (Product k a b) a
    forall (k :: * -> * -> *) a b. Cartesian k => k (Product k a b) a
    fst k (Product k a b) a
    -> k (Product k (Product k a b) c) (Product k a b)
    -> k (Product k (Product k a b) c) 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 (Product k a b) c) (Product k a b)
    forall a b. k (Product k a b) a
    forall (k :: * -> * -> *) a b. Cartesian k => k (Product k a b) a
    fst) k (Product k (Product k a b) c) a
    -> k (Product k (Product k a b) c) (Product k b c)
    -> k (Product k (Product k a b) c) (Product k a (Product k b c))
    forall a b c. k a b -> k a c -> k a (Product k b c)
    forall (k :: * -> * -> *) a b c.
    Cartesian k =>
    k a b -> k a c -> k a (Product k b c)
    &&& k (Product k a b) b
    -> k (Product k (Product k a b) c) (Product k b c)
    forall a b c. k a b -> k (Product k a c) (Product k b c)
    forall (p :: * -> * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b
           c.
    PFunctor p r t =>
    r a b -> t (p a c) (p b c)
    first k (Product k a b) b
    forall a b. k (Product k a b) b
    forall (k :: * -> * -> *) a b. Cartesian k => k (Product k a b) b
    snd

    -- | free construction of 'Disassociative' for the product 'Bifunctor' @Product k@
    disassociateProduct:: Cartesian k => Product k a (Product k b c) `k` Product k (Product k a b) c
    disassociateProduct :: forall (k :: * -> * -> *) a b c.
    Cartesian k =>
    k (Product k a (Product k b c)) (Product k (Product k a b) c)
    disassociateProduct= k (Product k c (Product k a b)) (Product k (Product k a b) c)
    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 k (Product k c (Product k a b)) (Product k (Product k a b) c)
    -> k (Product k a (Product k b c)) (Product k c (Product k a b))
    -> k (Product k a (Product k b c)) (Product k (Product k a b) c)
    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 a) (Product k a b)
    -> k (Product k c (Product k b a)) (Product k c (Product k a b))
    forall a b c. k a b -> k (Product k c a) (Product k c b)
    forall (q :: * -> * -> *) (s :: * -> * -> *) (t :: * -> * -> *) a b
           c.
    QFunctor q s t =>
    s a b -> t (q c a) (q c b)
    second k (Product k b a) (Product k 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 k (Product k c (Product k b a)) (Product k c (Product k a b))
    -> k (Product k a (Product k b c)) (Product k c (Product k b a))
    -> k (Product k a (Product k b c)) (Product k c (Product k a b))
    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 (Product k c b) a) (Product k c (Product k b a))
    forall (k :: * -> * -> *) a b c.
    Cartesian k =>
    k (Product k (Product k a b) c) (Product k a (Product k b c))
    associateProduct k (Product k (Product k c b) a) (Product k c (Product k b a))
    -> k (Product k a (Product k b c)) (Product k (Product k c b) a)
    -> k (Product k a (Product k b c)) (Product k c (Product 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 (Product k b c) (Product k c b)
    -> k (Product k (Product k b c) a) (Product k (Product k c b) a)
    forall a b c. k a b -> k (Product k a c) (Product k b c)
    forall (p :: * -> * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b
           c.
    PFunctor p r t =>
    r a b -> t (p a c) (p b c)
    first k (Product k b c) (Product k c 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 k (Product k (Product k b c) a) (Product k (Product k c b) a)
    -> k (Product k a (Product k b c)) (Product k (Product k b c) a)
    -> k (Product k a (Product k b c)) (Product k (Product k c 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 (Product k a (Product k b c)) (Product k (Product k b c) 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

    -- * Co-Cartesian categories

    -- a category that has finite coproducts, weakened the same way as PreCartesian above was weakened
    class (Monoidal k (Sum k), Symmetric k (Sum k)) => CoCartesian k where
        type Sum k :: * -> * -> *
        inl :: a `k` Sum k a b
        inr :: b `k` Sum k a b
        codiag :: Sum k a a `k` a
        (|||) :: k a c -> k b c -> Sum k a b `k` c

        codiag = k a a
    forall a. k a a
    forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id k a a -> k a a -> k (Sum k a a) a
    forall a c b. k a c -> k b c -> k (Sum k a b) c
    forall (k :: * -> * -> *) a c b.
    CoCartesian k =>
    k a c -> k b c -> k (Sum k a b) c
    ||| k a a
    forall a. k a a
    forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
    id
        k a c
    f ||| k b c
    g = k (Sum k c c) c
    forall a. k (Sum k a a) a
    forall (k :: * -> * -> *) a. CoCartesian k => k (Sum k a a) a
    codiag k (Sum k c c) c -> k (Sum k a b) (Sum k c c) -> k (Sum k a b) c
    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 c -> k b c -> k (Sum k a b) (Sum k c c)
    forall a b c d. k a b -> k c d -> k (Sum k a c) (Sum k b d)
    forall (p :: * -> * -> *) (r :: * -> * -> *) (s :: * -> * -> *)
           (t :: * -> * -> *) a b c d.
    Bifunctor p r s t =>
    r a b -> s c d -> t (p a c) (p b d)
    bimap k a c
    f k b c
    g

    {-- RULES
    "codiag . inl"  codiag . inl = id
    "codiag . inr"    codiag . inr = id
    "(f ||| g) . inl" forall f g. (f ||| g) . inl = f
    "(f ||| g) . inr" forall f g. (f ||| g) . inr = g
     --}

    instance CoCartesian (->) where
        type Sum (->) = Either
        inl :: forall a b. a -> Sum (->) a b
    inl = a -> Either a b
    a -> Sum (->) a b
    forall a b. a -> Either a b
    Left
        inr :: forall b a. b -> Sum (->) a b
    inr = b -> Either a b
    b -> Sum (->) a b
    forall a b. b -> Either a b
    Right
        codiag :: forall a. Sum (->) a a -> a
    codiag (Left a
    a) = a
    a
        codiag (Right a
    a) = a
    a
        (a -> c
    f ||| :: forall a c b. (a -> c) -> (b -> c) -> Sum (->) a b -> c
    ||| b -> c
    _) (Left a
    a) = a -> c
    f a
    a
        (a -> c
    _ ||| b -> c
    g) (Right b
    a) = b -> c
    g b
    a

    -- | free construction of 'Bifunctor' for the coproduct 'Bifunctor' @Sum k@ if @(|||)@ is known
    bimapSum :: CoCartesian k => k a c -> k b d -> Sum k a b `k` Sum k c d
    bimapSum :: forall (k :: * -> * -> *) a c b d.
    CoCartesian k =>
    k a c -> k b d -> k (Sum k a b) (Sum k c d)
    bimapSum k a c
    f k b d
    g = (k c (Sum k c d)
    forall a b. k a (Sum k a b)
    forall (k :: * -> * -> *) a b. CoCartesian k => k a (Sum k a b)
    inl k c (Sum k c d) -> k a c -> k a (Sum k c d)
    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 c
    f) k a (Sum k c d) -> k b (Sum k c d) -> k (Sum k a b) (Sum k c d)
    forall a c b. k a c -> k b c -> k (Sum k a b) c
    forall (k :: * -> * -> *) a c b.
    CoCartesian k =>
    k a c -> k b c -> k (Sum k a b) c
    ||| (k d (Sum k c d)
    forall b a. k b (Sum k a b)
    forall (k :: * -> * -> *) b a. CoCartesian k => k b (Sum k a b)
    inr k d (Sum k c d) -> k b d -> k b (Sum k c d)
    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 b d
    g)

    -- | free construction of 'Braided' for the coproduct 'Bifunctor' @Sum k@
    braidSum :: CoCartesian k => Sum k a b `k` Sum k b a
    braidSum :: forall (k :: * -> * -> *) a b.
    CoCartesian k =>
    k (Sum k a b) (Sum k b a)
    braidSum = k a (Sum k b a)
    forall b a. k b (Sum k a b)
    forall (k :: * -> * -> *) b a. CoCartesian k => k b (Sum k a b)
    inr k a (Sum k b a) -> k b (Sum k b a) -> k (Sum k a b) (Sum k b a)
    forall a c b. k a c -> k b c -> k (Sum k a b) c
    forall (k :: * -> * -> *) a c b.
    CoCartesian k =>
    k a c -> k b c -> k (Sum k a b) c
    ||| k b (Sum k b a)
    forall a b. k a (Sum k a b)
    forall (k :: * -> * -> *) a b. CoCartesian k => k a (Sum k a b)
    inl

    -- | free construction of 'Associative' for the coproduct 'Bifunctor' @Sum k@
    associateSum :: CoCartesian k => Sum k (Sum k a b) c `k` Sum k a (Sum k b c)
    associateSum :: forall (k :: * -> * -> *) a b c.
    CoCartesian k =>
    k (Sum k (Sum k a b) c) (Sum k a (Sum k b c))
    associateSum = k (Sum k (Sum k b c) a) (Sum k a (Sum k b c))
    forall a b. k (Sum k a b) (Sum k b a)
    forall (k :: * -> * -> *) (p :: * -> * -> *) a b.
    Braided k p =>
    k (p a b) (p b a)
    braid k (Sum k (Sum k b c) a) (Sum k a (Sum k b c))
    -> k (Sum k (Sum k a b) c) (Sum k (Sum k b c) a)
    -> k (Sum k (Sum k a b) c) (Sum k a (Sum k b c))
    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 (Sum k c b) (Sum k b c)
    -> k (Sum k (Sum k c b) a) (Sum k (Sum k b c) a)
    forall a b c. k a b -> k (Sum k a c) (Sum k b c)
    forall (p :: * -> * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b
           c.
    PFunctor p r t =>
    r a b -> t (p a c) (p b c)
    first k (Sum k c b) (Sum k b c)
    forall a b. k (Sum k a b) (Sum k b a)
    forall (k :: * -> * -> *) (p :: * -> * -> *) a b.
    Braided k p =>
    k (p a b) (p b a)
    braid k (Sum k (Sum k c b) a) (Sum k (Sum k b c) a)
    -> k (Sum k (Sum k a b) c) (Sum k (Sum k c b) a)
    -> k (Sum k (Sum k a b) c) (Sum k (Sum k b c) 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 (Sum k c (Sum k b a)) (Sum k (Sum k c b) a)
    forall (k :: * -> * -> *) a b c.
    CoCartesian k =>
    k (Sum k a (Sum k b c)) (Sum k (Sum k a b) c)
    disassociateSum k (Sum k c (Sum k b a)) (Sum k (Sum k c b) a)
    -> k (Sum k (Sum k a b) c) (Sum k c (Sum k b a))
    -> k (Sum k (Sum k a b) c) (Sum k (Sum k c 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 (Sum k a b) (Sum k b a)
    -> k (Sum k c (Sum k a b)) (Sum k c (Sum k b a))
    forall a b c. k a b -> k (Sum k c a) (Sum k c b)
    forall (q :: * -> * -> *) (s :: * -> * -> *) (t :: * -> * -> *) a b
           c.
    QFunctor q s t =>
    s a b -> t (q c a) (q c b)
    second k (Sum k a b) (Sum k b a)
    forall a b. k (Sum k a b) (Sum k b a)
    forall (k :: * -> * -> *) (p :: * -> * -> *) a b.
    Braided k p =>
    k (p a b) (p b a)
    braid k (Sum k c (Sum k a b)) (Sum k c (Sum k b a))
    -> k (Sum k (Sum k a b) c) (Sum k c (Sum k a b))
    -> k (Sum k (Sum k a b) c) (Sum k c (Sum 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 (Sum k (Sum k a b) c) (Sum k c (Sum k a b))
    forall a b. k (Sum k a b) (Sum k b a)
    forall (k :: * -> * -> *) (p :: * -> * -> *) a b.
    Braided k p =>
    k (p a b) (p b a)
    braid

    -- | free construction of 'Disassociative' for the coproduct 'Bifunctor' @Sum k@
    disassociateSum :: CoCartesian k => Sum k a (Sum k b c) `k` Sum k (Sum k a b) c
    disassociateSum :: forall (k :: * -> * -> *) a b c.
    CoCartesian k =>
    k (Sum k a (Sum k b c)) (Sum k (Sum k a b) c)
    disassociateSum = (k (Sum k a b) (Sum k (Sum k a b) c)
    forall a b. k a (Sum k a b)
    forall (k :: * -> * -> *) a b. CoCartesian k => k a (Sum k a b)
    inl k (Sum k a b) (Sum k (Sum k a b) c)
    -> k a (Sum k a b) -> k a (Sum k (Sum k a b) c)
    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 a b)
    forall a b. k a (Sum k a b)
    forall (k :: * -> * -> *) a b. CoCartesian k => k a (Sum k a b)
    inl) k a (Sum k (Sum k a b) c)
    -> k (Sum k b c) (Sum k (Sum k a b) c)
    -> k (Sum k a (Sum k b c)) (Sum k (Sum k a b) c)
    forall a c b. k a c -> k b c -> k (Sum k a b) c
    forall (k :: * -> * -> *) a c b.
    CoCartesian k =>
    k a c -> k b c -> k (Sum k a b) c
    ||| k b (Sum k a b) -> k (Sum k b c) (Sum k (Sum k a b) c)
    forall a b c. k a b -> k (Sum k a c) (Sum k b c)
    forall (p :: * -> * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b
           c.
    PFunctor p r t =>
    r a b -> t (p a c) (p b c)
    first k b (Sum k a b)
    forall b a. k b (Sum k a b)
    forall (k :: * -> * -> *) b a. CoCartesian k => k b (Sum k a b)
    inr