    {-# LANGUAGE CPP #-}
    #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
    {-# LANGUAGE Trustworthy #-}
    #endif
    {-# LANGUAGE TypeOperators #-}
    -------------------------------------------------------------------------------------------
    -- |
    -- Module   : Control.Category.Distributive
    -- Copyright: 2008 Edward Kmett
    -- License  : BSD
    --
    -- Maintainer : Edward Kmett <ekmett@gmail.com>
    -- Stability  : experimental
    -- Portability: non-portable (class-associated types)
    --
    -------------------------------------------------------------------------------------------
    module Control.Category.Distributive
        (
        -- * Distributive Categories
          factor
        , Distributive(..)
        ) where

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

    -- | The canonical factoring morphism.

    factor :: (Cartesian k, CoCartesian k) => Sum k (Product k a b) (Product k a c) `k` Product k a (Sum k b c)
    factor :: forall (k :: * -> * -> *) a b c.
    (Cartesian k, CoCartesian k) =>
    k (Sum k (Product k a b) (Product k a c)) (Product k a (Sum k b c))
    factor = k b (Sum k b c) -> k (Product k a b) (Product k a (Sum k b c))
    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 b (Sum k 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 (Product k a b) (Product k a (Sum k b c))
    -> k (Product k a c) (Product k a (Sum k b c))
    -> k (Sum k (Product k a b) (Product k a c))
         (Product k a (Sum k 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 c (Sum k b c) -> k (Product k a c) (Product k a (Sum k b c))
    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 c (Sum k b c)
    forall b a. k b (Sum k a b)
    forall (k :: * -> * -> *) b a. CoCartesian k => k b (Sum k a b)
    inr

    -- | A category in which 'factor' is an isomorphism

    class (Cartesian k, CoCartesian k) => Distributive k where
        distribute :: Product k a (Sum k b c) `k` Sum k (Product k a b) (Product k a c)

    instance Distributive (->) where
        distribute :: forall a b c.
    Product (->) a (Sum (->) b c)
    -> Sum (->) (Product (->) a b) (Product (->) a c)
    distribute (a
    a, Left b
    b) = (a, b) -> Either (a, b) (a, c)
    forall a b. a -> Either a b
    Left (a
    a,b
    b)
        distribute (a
    a, Right c
    c) = (a, c) -> Either (a, b) (a, c)
    forall a b. b -> Either a b
    Right (a
    a,c
    c)

    {-- RULES
    "factor . distribute" factor . distribute = id
    "distribute . factor" distribute . factor = id
      --}