diff --git a/Control/Categorical/Bifunctor.hs b/Control/Categorical/Bifunctor.hs
new file mode 100644
--- /dev/null
+++ b/Control/Categorical/Bifunctor.hs
@@ -0,0 +1,71 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts #-}
+-------------------------------------------------------------------------------------------
+-- |
+-- Module   : Control.Categorical.Bifunctor
+-- Copyright: 2008-2010 Edward Kmett
+-- License  : BSD3
+--
+-- Maintainer : Edward Kmett <ekmett@gmail.com>
+-- Stability  : experimental
+-- Portability: non-portable (functional-dependencies)
+--
+-- A more categorical definition of 'Bifunctor'
+-------------------------------------------------------------------------------------------
+module Control.Categorical.Bifunctor
+    ( PFunctor (first), firstDefault
+    , QFunctor (second), secondDefault
+    , Bifunctor (bimap)
+    , dimap
+    , difirst
+    ) where
+
+import Prelude hiding (id, (.))
+import Control.Category
+import Control.Category.Dual
+
+class (Category r, Category t) => PFunctor p r t | p r -> t, p t -> r where
+    first :: r a b -> t (p a c) (p b c)
+
+instance PFunctor (,) (->) (->) where
+    first f ~(a, b) = (f a, b)
+
+instance PFunctor Either (->) (->) where
+    first f (Left a)  = Left (f a)
+    first _ (Right b) = Right b
+
+{-# INLINE firstDefault #-}
+firstDefault :: Bifunctor p r s t => r a b -> t (p a c) (p b c)
+firstDefault f = bimap f id
+
+difirst :: PFunctor f (Dual s) t => s b a -> t (f a c) (f b c)
+difirst = first . Dual
+
+class (Category s, Category t) => QFunctor q s t | q s -> t, q t -> s where
+    second :: s a b -> t (q c a) (q c b)
+
+{-# INLINE secondDefault #-}
+secondDefault :: Bifunctor p r s t => s a b -> t (p c a) (p c b)
+secondDefault = bimap id
+
+instance QFunctor Either (->) (->) where
+    second = secondDefault
+
+instance Bifunctor Either (->) (->) (->) where
+    bimap f _ (Left a) = Left (f a)
+    bimap _ g (Right a) = Right (g a)
+
+instance QFunctor (->) (->) (->) where
+    second = (.)
+
+instance QFunctor (,) (->) (->) where
+    second = secondDefault
+
+instance Bifunctor (,) (->) (->) (->) where
+    bimap f g ~(a,b)= (f a, g b)
+
+class (PFunctor p r t, QFunctor p s t) => Bifunctor p r s t | p r -> s t, p s -> r t, p t -> r s where
+    bimap :: r a b -> s c d -> t (p a c) (p b d)
+
+dimap :: Bifunctor f (Dual s) t u => s b a -> t c d -> u (f a c) (f b d)
+dimap = bimap . Dual
+
diff --git a/Control/Categorical/Functor.hs b/Control/Categorical/Functor.hs
new file mode 100644
--- /dev/null
+++ b/Control/Categorical/Functor.hs
@@ -0,0 +1,113 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveDataTypeable, FlexibleContexts, UndecidableInstances, FlexibleInstances #-}
+-------------------------------------------------------------------------------------------
+-- |
+-- Module     : Control.Categorical.Functor
+-- Copyright : 2008-2010 Edward Kmett
+-- License     : BSD3
+--
+-- Maintainer   : Edward Kmett <ekmett@gmail.com>
+-- Stability    : experimental
+-- Portability    : non-portable (functional-dependencies)
+--
+-- A more categorical definition of 'Functor'
+-------------------------------------------------------------------------------------------
+module Control.Categorical.Functor 
+    ( Functor(fmap) 
+    , EndoFunctor
+    , LiftedFunctor(..)
+    , LoweredFunctor(..)
+    ) where
+
+import Control.Category
+import Prelude hiding (id, (.), Functor(..))
+import qualified Prelude
+import Data.Data (Data(..), mkDataType, DataType, mkConstr, Constr, constrIndex, Fixity(..))
+import Data.Typeable (Typeable1(..), TyCon, mkTyCon, mkTyConApp, gcast1)
+
+-- TODO Data, Typeable
+newtype LiftedFunctor f a = LiftedFunctor (f a)
+    deriving (Show, Read)
+
+liftedTyCon :: TyCon
+liftedTyCon = mkTyCon "Control.Categorical.Functor.LiftedFunctor"
+{-# NOINLINE liftedTyCon #-}
+
+liftedConstr :: Constr
+liftedConstr = mkConstr liftedDataType "LiftedFunctor" [] Prefix
+{-# NOINLINE liftedConstr #-}
+
+liftedDataType :: DataType
+liftedDataType = mkDataType "Control.Categorical.Fucntor.LiftedFunctor" [liftedConstr]
+{-# NOINLINE liftedDataType #-}
+
+instance Typeable1 f => Typeable1 (LiftedFunctor f) where
+    typeOf1 tfa = mkTyConApp liftedTyCon [typeOf1 (undefined `asArgsType` tfa)]
+        where asArgsType :: f a -> t f a -> f a
+              asArgsType = const
+
+instance (Typeable1 f, Data (f a), Data a) => Data (LiftedFunctor f a) where
+    gfoldl f z (LiftedFunctor a) = z LiftedFunctor `f` a
+    toConstr _ = liftedConstr
+    gunfold k z c = case constrIndex c of
+        1 -> k (z LiftedFunctor)
+        _ -> error "gunfold"
+    dataTypeOf _ = liftedDataType
+    dataCast1 f = gcast1 f
+
+newtype LoweredFunctor f a = LoweredFunctor (f a)
+    deriving (Show, Read)
+
+loweredTyCon :: TyCon
+loweredTyCon = mkTyCon "Control.Categorical.Functor.LoweredFunctor"
+{-# NOINLINE loweredTyCon #-}
+
+loweredConstr :: Constr
+loweredConstr = mkConstr loweredDataType "LoweredFunctor" [] Prefix
+{-# NOINLINE loweredConstr #-}
+
+loweredDataType :: DataType
+loweredDataType = mkDataType "Control.Categorical.Fucntor.LoweredFunctor" [loweredConstr]
+{-# NOINLINE loweredDataType #-}
+
+instance Typeable1 f => Typeable1 (LoweredFunctor f) where
+    typeOf1 tfa = mkTyConApp loweredTyCon [typeOf1 (undefined `asArgsType` tfa)]
+        where asArgsType :: f a -> t f a -> f a
+              asArgsType = const
+
+instance (Typeable1 f, Data (f a), Data a) => Data (LoweredFunctor f a) where
+    gfoldl f z (LoweredFunctor a) = z LoweredFunctor `f` a
+    toConstr _ = loweredConstr
+    gunfold k z c = case constrIndex c of
+        1 -> k (z LoweredFunctor)
+        _ -> error "gunfold"
+    dataTypeOf _ = loweredDataType
+    dataCast1 f = gcast1 f
+
+class (Category r, Category t) => Functor f r t | f r -> t, f t -> r where
+    fmap :: r a b -> t (f a) (f b)
+
+instance Functor f (->) (->) => Prelude.Functor (LoweredFunctor f) where
+    fmap f (LoweredFunctor a) = LoweredFunctor (Control.Categorical.Functor.fmap f a)
+
+instance Prelude.Functor f => Functor (LiftedFunctor f) (->) (->) where
+    fmap f (LiftedFunctor a) = LiftedFunctor (Prelude.fmap f a)
+
+instance Functor ((,) a) (->) (->) where
+    fmap f ~(a, b) = (a, f b)
+
+instance Functor (Either a) (->) (->) where
+    fmap _ (Left a) = Left a 
+    fmap f (Right a) = Right (f a)
+
+instance Functor Maybe (->) (->) where
+    fmap = Prelude.fmap
+
+instance Functor [] (->) (->) where
+    fmap = Prelude.fmap
+
+instance Functor IO (->) (->) where
+    fmap = Prelude.fmap
+
+class (Functor f (~>) (~>)) => EndoFunctor f (~>)
+instance (Functor f (~>) (~>)) => EndoFunctor f (~>)
+    
diff --git a/Control/Categorical/Object.hs b/Control/Categorical/Object.hs
new file mode 100644
--- /dev/null
+++ b/Control/Categorical/Object.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE TypeFamilies, TypeOperators #-}
+-------------------------------------------------------------------------------------------
+-- |
+-- Module   : Control.Category.Object
+-- Copyright: 2010 Edward Kmett
+-- License  : BSD
+--
+-- Maintainer : Edward Kmett <ekmett@gmail.com>
+-- Stability  : experimental
+-- Portability: non-portable (either class-associated types or MPTCs with fundeps)
+--
+-- This module declares the 'HasTerminalObject' and 'HasInitialObject' classes.
+-- 
+-- These are both special cases of the idea of a (co)limit.
+-------------------------------------------------------------------------------------------
+
+module Control.Categorical.Object 
+    ( HasTerminalObject(..)
+    , HasInitialObject(..)
+    ) where
+
+import Control.Category
+
+-- | The @Category (~>)@ has a terminal object @Terminal (~>)@ such that for all objects @a@ in @(~>)@, 
+-- there exists a unique morphism from @a@ to @Terminal (~>)@.
+class Category (~>) => HasTerminalObject (~>) where
+    type Terminal (~>) :: *
+    terminate :: a ~> Terminal (~>)
+
+-- | The @Category (~>)@ has an initial (coterminal) object @Initial (~>)@ such that for all objects 
+-- @a@ in @(~>)@, there exists a unique morphism from @Initial (~>) @ to @a@.
+
+class Category (~>) => HasInitialObject (~>) where
+    type Initial (~>) :: *
+    initiate :: Initial (~>) ~> a
diff --git a/Control/Category/Associative.hs b/Control/Category/Associative.hs
new file mode 100644
--- /dev/null
+++ b/Control/Category/Associative.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+-------------------------------------------------------------------------------------------
+-- |
+-- Module    : Control.Category.Associative
+-- Copyright : 2008 Edward Kmett
+-- License   : BSD
+--
+-- Maintainer  : Edward Kmett <ekmett@gmail.com>
+-- Stability   : experimental
+-- Portability : portable
+--
+-- NB: this contradicts another common meaning for an 'Associative' 'Category', which is one 
+-- where the pentagonal condition does not hold, but for which there is an identity.
+--
+-------------------------------------------------------------------------------------------
+module Control.Category.Associative 
+    ( Associative(..)
+    , Disassociative(..)
+    ) where
+
+import Control.Categorical.Bifunctor
+
+{- | A category with an associative bifunctor satisfying Mac Lane\'s pentagonal coherence identity law:
+
+> bimap id associate . associate . bimap associate id = associate . associate
+-}
+class Bifunctor p k k k => Associative k p where
+    associate :: k (p (p a b) c) (p a (p b c))
+
+{- | A category with a disassociative bifunctor satisyfing the dual of Mac Lane's pentagonal coherence identity law:
+
+> bimap disassociate id . disassociate . bimap id disassociate = disassociate . disassociate
+-}
+class Bifunctor s k k k => Disassociative k s where
+    disassociate :: k (s a (s b c)) (s (s a b) c)
+
+{-# RULES
+"copentagonal coherence" first disassociate . disassociate . second disassociate = disassociate . disassociate
+"pentagonal coherence"   second associate . associate . first associate = associate . associate
+ #-}
+
+instance Associative (->) (,) where
+        associate ((a,b),c) = (a,(b,c))
+
+instance Disassociative (->) (,) where
+        disassociate (a,(b,c)) = ((a,b),c)
+
+instance Associative (->) Either where
+        associate (Left (Left a)) = Left a
+        associate (Left (Right b)) = Right (Left b)
+        associate (Right c) = Right (Right c)
+
+instance Disassociative (->) Either where
+        disassociate (Left a) = Left (Left a)
+        disassociate (Right (Left b)) = Left (Right b)
+        disassociate (Right (Right c)) = Right c
diff --git a/Control/Category/Braided.hs b/Control/Category/Braided.hs
new file mode 100644
--- /dev/null
+++ b/Control/Category/Braided.hs
@@ -0,0 +1,65 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+-------------------------------------------------------------------------------------------
+-- |
+-- Module	 : Control.Category.Braided
+-- Copyright : 2008 Edward Kmett
+-- License	 : BSD
+--
+-- Maintainer	: Edward Kmett <ekmett@gmail.com>
+-- Stability	: experimental
+-- Portability	: portable
+--
+-------------------------------------------------------------------------------------------
+module Control.Category.Braided 
+	( Braided(..)
+	, Symmetric
+	, swap
+	) where
+
+import Control.Categorical.Bifunctor
+import Control.Category.Associative
+
+{- | A braided (co)(monoidal or associative) category can commute the arguments of its bi-endofunctor. Obeys the laws:
+
+> idr . braid = idl 
+> idl . braid = idr 
+> braid . coidr = coidl 
+> braid . coidl = coidr 
+> associate . braid . associate = second braid . associate . first braid 
+> disassociate . braid . disassociate = first braid . disassociate . second braid 
+
+-}
+
+class Braided k p where
+	braid :: k (p a b) (p b a)
+
+instance Braided (->) Either where
+        braid (Left a) = Right a
+        braid (Right b) = Left b
+
+instance Braided (->) (,) where
+        braid ~(a,b) = (b,a)
+
+{-# RULES
+"braid/associate/braid"         second braid . associate . first braid    = associate . braid . associate
+"braid/disassociate/braid"      first braid . disassociate . second braid = disassociate . braid . disassociate
+  #-}
+
+{- |
+If we have a symmetric (co)'Monoidal' category, you get the additional law:
+
+> swap . swap = id
+ -}
+class Braided k p => Symmetric k p
+
+swap :: Symmetric k p => k (p a b) (p b a)
+swap = braid
+
+{-# RULES
+"swap/swap" swap . swap = id
+  #-}
+
+
+instance Symmetric (->) Either 
+
+instance Symmetric (->) (,)
diff --git a/Control/Category/Cartesian.hs b/Control/Category/Cartesian.hs
new file mode 100644
--- /dev/null
+++ b/Control/Category/Cartesian.hs
@@ -0,0 +1,163 @@
+{-# 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
+    ( 
+    -- * Pre-(Co)Cartesian categories
+      PreCartesian(..)
+    , bimapProduct, braidProduct, associateProduct, disassociateProduct
+    , PreCoCartesian(..)
+    , bimapSum, braidSum, associateSum, disassociateSum
+    -- * (Co)Cartesian categories
+    , Cartesian
+    , CoCartesian
+    ) where
+
+import Control.Category.Associative
+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 |||
+
+{- |
+NB: This is weaker than traditional category with products! That is Cartesian, below.
+The problem is @(->)@ lacks an initial object, since every type is inhabited in Haskell.
+Consequently its coproduct is merely a semigroup, not a monoid (as it has no identity), and 
+since we want to be able to describe its dual category, which has this non-traditional 
+form being built over a category with an associative bifunctor rather than as a monoidal category
+for the product monoid.
+
+Minimum definition: 
+
+> fst, snd, diag 
+> fst, snd, (&&&)
+-}
+class ( Associative (~>) (Product (~>))
+      , Disassociative (~>) (Product (~>))
+      , Symmetric (~>) (Product (~>))
+      , Braided (~>) (Product (~>))
+      ) => PreCartesian (~>) where
+    type Product (~>) :: * -> * -> *
+    fst :: Product (~>) a b ~> a
+    snd :: Product (~>) a b ~> b
+    diag :: a ~> Product (~>) a a
+    (&&&) :: (a ~> b) -> (a ~> c) -> a ~> Product (~>) b c
+
+    diag = id &&& id
+    f &&& g = bimap f g . 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 PreCartesian (->) where
+    type Product (->) = (,)
+    fst = Prelude.fst
+    snd = Prelude.snd
+    diag a = (a,a)
+    (f &&& g) a = (f a, g a)
+
+-- alias
+class ( Monoidal (~>) (Product (~>))
+      , PreCartesian (~>)
+      ) => Cartesian (~>)
+instance ( Monoidal (~>) (Product (~>))
+         , PreCartesian (~>)
+         ) => Cartesian (~>)
+
+-- | free construction of 'Bifunctor' for the product 'Bifunctor' @Product k@ if @(&&&)@ is known
+bimapProduct :: (PreCartesian (~>), (<*>) ~ Product (~>)) => (a ~> c) -> (b ~> d) -> (a <*> b) ~> (c <*> d)
+bimapProduct f g = (f . fst) &&& (g . snd)
+    
+-- | free construction of 'Braided' for the product 'Bifunctor' @Product k@
+-- braidProduct :: (PreCartesian (~>), Product (~>) ~ (<*>))  => a <*> b ~> b <*> a
+braidProduct :: (PreCartesian (~>)) => Product (~>) a b ~> Product (~>) b a
+braidProduct = snd &&& fst
+
+-- | free construction of 'Associative' for the product 'Bifunctor' @Product k@
+-- associateProduct :: (PreCartesian (~>), (<*>) ~ Product (~>))  => (a <*> b) <*> c ~> (a <*> (b <*> c))
+associateProduct :: (PreCartesian (~>)) => Product (~>) (Product (~>) a b) c ~> Product (~>) a (Product (~>) b c)
+associateProduct = (fst . fst) &&& first snd
+
+-- | free construction of 'Disassociative' for the product 'Bifunctor' @Product k@
+-- disassociateProduct:: (PreCartesian (~>),  (<*>) ~ Product (~>)) => a <*> (b <*> c) ~> (a <*> b) <*> c
+disassociateProduct:: (PreCartesian (~>)) => Product (~>) a (Product (~>) b c) ~> Product (~>) (Product (~>) a b) c
+disassociateProduct= braid . second braid . associateProduct . first braid . braid 
+
+-- * Co-PreCartesian categories
+
+-- a category that has finite coproducts, wea(~>)ened the same way as PreCartesian above was wea(~>)ened
+class ( Associative (~>) (Sum (~>))
+      , Disassociative (~>) (Sum (~>))
+      , Symmetric (~>) (Product (~>))
+      , Braided (~>) (Sum (~>))
+      ) => PreCoCartesian (~>) where
+    type Sum (~>) :: * -> * -> *
+    inl :: a ~> Sum (~>) a b
+    inr :: b ~> Sum (~>) a b
+    codiag :: Sum (~>) a a ~> a
+    (|||) :: (a ~> c) -> (b ~> c) -> Sum (~>) a b ~> c
+
+    codiag = id ||| id
+    f ||| g = codiag . bimap f 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 PreCoCartesian (->) where
+    type Sum (->) = Either
+    inl = Left
+    inr = Right
+    codiag (Left a) = a
+    codiag (Right a) = a
+    (f ||| _) (Left a) = f a 
+    (_ ||| g) (Right a) = g a
+
+-- | free construction of 'Bifunctor' for the coproduct 'Bifunctor' @Sum (~>)@ if @(|||)@ is known
+bimapSum :: (PreCoCartesian (~>), Sum (~>) ~ (+)) => (a ~> c) -> (b ~> d) -> (a + b) ~> (c + d)
+bimapSum f g = (inl . f) ||| (inr . g)
+
+-- | free construction of 'Braided' for the coproduct 'Bifunctor' @Sum (~>)@
+braidSum :: (PreCoCartesian (~>), (+) ~ Sum (~>)) => (a + b) ~> (b + a)
+braidSum = inr ||| inl
+
+-- | free construction of 'Associative' for the coproduct 'Bifunctor' @Sum (~>)@
+-- associateSum :: (PreCoCartesian (~>), (+) ~ Sum (~>)) => ((a + b) + c) ~> (a + (b + c))
+associateSum :: (PreCoCartesian (~>)) => Sum (~>) (Sum (~>) a b) c ~> Sum (~>) a (Sum (~>) b c)
+associateSum = braid . first braid . disassociateSum . second braid . braid
+
+-- | free construction of 'Disassociative' for the coproduct 'Bifunctor' @Sum (~>)@
+-- disassociateSum :: (PreCoCartesian (~>), (+) ~ Sum (~>)) => (a + (b + c)) ~> ((a + b) + c)
+disassociateSum :: (PreCoCartesian (~>)) => Sum (~>) a (Sum (~>) b c) ~> Sum (~>) (Sum (~>) a b) c
+disassociateSum = (inl . inl) ||| first inr
+
+class 
+    ( Comonoidal (~>) (Sum (~>))
+    , PreCoCartesian (~>)
+    ) => CoCartesian (~>)
+instance 
+    ( Comonoidal (~>) (Sum (~>))
+    , PreCoCartesian (~>)
+    ) => CoCartesian (~>)
diff --git a/Control/Category/Cartesian/Closed.hs b/Control/Category/Cartesian/Closed.hs
new file mode 100644
--- /dev/null
+++ b/Control/Category/Cartesian/Closed.hs
@@ -0,0 +1,91 @@
+{-# 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 () -- hiding ((.), id, fst, snd, curry, uncurry)
+
+import Control.Category
+import Control.Category.Braided
+import Control.Category.Cartesian
+import Control.Category.Monoidal
+
+-- * 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 (<=)
+      , Symmetric (<=) (Product (<=))
+      , Monoidal (<=) (Product (<=)) 
+      ) => CCC (<=) where
+    type Exp (<=) :: * -> * -> *
+    -- apply :: (<\>) ~ Exp (<=), (<*>) ~ Product (<=) => ((a <\> b) <*> a) <= b
+    apply :: (Product (<=) (Exp (<=) a b) a) <= b
+    curry :: ((Product (<=) a b) <= c) -> a <= Exp (<=) b c
+    uncurry :: (a <= (Exp (<=) b c)) -> (Product (<=>) a b <= c)
+
+{-# RULES
+"curry apply"         curry apply = id
+-- "curry . uncurry"     curry . uncurry = id
+-- "uncurry . curry"     uncurry . curry = id
+ #-}
+
+-- * Free @'Adjunction' (Product (<=) a) (Exp (<=) a) (<=) (<=)@
+
+-- unitCCC :: (CCC (<=), (<*>) ~ Product (<=), (<\>) ~ Exp (<=)) => a <= b <\> (b <*> a)
+unitCCC :: CCC (<=) => a <= Exp (<=) b (Product (<=) b a)
+unitCCC = curry braid
+
+-- counitCCC :: (CCC (<=), (<*>) ~ Product (<=), (<\>) ~ Exp (<=)) => (b <*> (b <\> a)) <= a
+counitCCC :: CCC (<=) => (Product (<=) b (Exp (<=) b a)) <= a
+counitCCC = apply . 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 (<=)
+    , Symmetric (<=) (Sum (<=))
+    , Comonoidal (<=) (Sum (<=))
+    ) => CoCCC (<=) where
+    type Coexp (<=) :: * -> * -> *
+    coapply :: b <= Sum (<=) (Coexp (<=) a b) a
+    cocurry :: (c <= Sum (<=) a b) -> (Coexp (<=) b c <= a)
+    uncocurry :: (Coexp (<=) b c <= a) -> (c <= Sum (<=) 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 (<=), subtract ~ Coexp (<=), (+) ~ Sum (<=)) => a <= b + subtract b a
+unitCoCCC :: (CoCCC (<=)) => a <= Sum (<=) b (Coexp (<=) b a)
+unitCoCCC = swap . coapply
+
+counitCoCCC :: (CoCCC (<=), subtract ~ Coexp (<=), (+) ~ Sum (<=)) => subtract b (b + a) <= a
+counitCoCCC = cocurry swap
diff --git a/Control/Category/Discrete.hs b/Control/Category/Discrete.hs
new file mode 100644
--- /dev/null
+++ b/Control/Category/Discrete.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE GADTs, TypeOperators #-}
+-------------------------------------------------------------------------------------------
+-- |
+-- Module    : Control.Category.Discrete
+-- Copyright : 2008-2010 Edward Kmett
+-- License   : BSD
+--
+-- Maintainer  : Edward Kmett <ekmett@gmail.com>
+-- Stability   : experimental
+-- Portability : portable
+--
+-------------------------------------------------------------------------------------------
+module Control.Category.Discrete
+    ( Discrete(Refl)
+    , liftDiscrete
+    , cast
+    , inverse
+    ) where
+
+import Prelude ()
+import Control.Category
+-- import Unsafe.Coerce (unsafeCoerce)
+
+-- | Category of discrete objects. The only arrows are identity arrows.
+data Discrete a b where 
+    Refl :: Discrete a a
+
+instance Category Discrete where
+    id = Refl
+    Refl . Refl = Refl
+
+-- | Discrete a b acts as a proof that a = b, lift that proof into something of kind * -> *
+liftDiscrete :: Discrete a b -> Discrete (f a) (f b)
+liftDiscrete Refl = Refl
+
+-- | Lower the proof that a ~ b to an arbitrary category.
+cast :: Category (~>) => Discrete a b -> (a ~> b)
+cast Refl = id
+
+-- | 
+inverse :: Discrete a b -> Discrete b a
+inverse Refl = Refl
diff --git a/Control/Category/Distributive.hs b/Control/Category/Distributive.hs
new file mode 100644
--- /dev/null
+++ b/Control/Category/Distributive.hs
@@ -0,0 +1,54 @@
+{-# 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
+import Control.Category.Cartesian
+
+-- | the canonical factoring morphism 
+-- 
+-- > factor :: ( PreCartesian (~>)
+-- >         , (*) ~ Product (~>)
+-- >         , PreCoCartesian (~>)
+-- >         , (+) ~ Sum (~>) 
+-- >         ) => ((a * b) + (a * c)) ~> (a * (b + c))
+
+factor :: ( PreCartesian (~>)
+          , PreCoCartesian (~>)
+          ) => Sum (~>) (Product (~>) a b) (Product (~>) a c) ~> Product (~>) a (Sum (~>) b c)
+factor = second inl ||| second inr
+
+-- | A category in which 'factor' is an isomorphism
+-- > class ( PreCartesian (~>) 
+-- >       , (*) ~ Product (~>)
+-- >       , PreCoCartesian (~>)
+-- >       , (+) ~ Sum (~>) 
+-- >       ) => Distributive (~>) where
+class (PreCartesian (~>), PreCoCartesian (~>)) => Distributive (~>) where
+    distribute :: Product (~>) a (Sum (~>) b c) ~> Sum (~>) (Product (~>) a b) (Product (~>) a c)
+
+instance Distributive (->) where
+    distribute (a, Left b) = Left (a,b)
+    distribute (a, Right c) = Right (a,c)
+
+{-# RULES
+"factor . distribute" factor . distribute = id
+"distribute . factor" distribute . factor = id
+ #-}
diff --git a/Control/Category/Dual.hs b/Control/Category/Dual.hs
new file mode 100644
--- /dev/null
+++ b/Control/Category/Dual.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE DeriveDataTypeable, TypeOperators, FlexibleContexts #-}
+-------------------------------------------------------------------------------------------
+-- |
+-- Module	 : Control.Category.Dual
+-- Copyright : 2008-2010 Edward Kmett
+-- License	 : BSD
+--
+-- Maintainer	: Edward Kmett <ekmett@gmail.com>
+-- Stability	: experimental
+-- Portability	: portable
+--
+-------------------------------------------------------------------------------------------
+module Control.Category.Dual
+	( Dual(..)
+	) where
+
+import Prelude hiding ((.), id)
+import Control.Category
+import Data.Data (Data(..), mkDataType, DataType, mkConstr, Constr, constrIndex, Fixity(..))
+import Data.Typeable (Typeable2(..), TyCon, mkTyCon, mkTyConApp, gcast1)
+
+data Dual k a b = Dual { runDual :: k b a } 
+
+instance Category k => Category (Dual k) where
+	id = Dual id
+	Dual f . Dual g = Dual (g . f)
+
+instance Typeable2 (~>) => Typeable2 (Dual (~>)) where
+    typeOf2 tfab = mkTyConApp dataTyCon [typeOf2 (undefined `asDualArgsType` tfab)]
+        where asDualArgsType :: f b a -> t f a b -> f b a
+              asDualArgsType = const
+
+dataTyCon :: TyCon
+dataTyCon = mkTyCon "Control.Category.Dual.Dual"
+{-# NOINLINE dataTyCon #-}
+
+dualConstr :: Constr
+dualConstr = mkConstr dataDataType "Dual" [] Prefix
+{-# NOINLINE dualConstr #-}
+
+dataDataType :: DataType
+dataDataType = mkDataType "Control.Category.Dual.Dual" [dualConstr]
+{-# NOINLINE dataDataType #-}
+
+instance (Typeable2 (~>), Data a, Data b, Data (b ~> a)) => Data (Dual (~>) a b) where
+    gfoldl f z (Dual a) = z Dual `f` a
+    toConstr _ = dualConstr
+    gunfold k z c = case constrIndex c of
+        1 -> k (z Dual)
+        _ -> error "gunfold"
+    dataTypeOf _ = dataDataType
+    dataCast1 f = gcast1 f
diff --git a/Control/Category/Monoidal.hs b/Control/Category/Monoidal.hs
new file mode 100644
--- /dev/null
+++ b/Control/Category/Monoidal.hs
@@ -0,0 +1,89 @@
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}
+-------------------------------------------------------------------------------------------
+-- |
+-- Module	 : Control.Category.Monoidal
+-- Copyright : 2008 Edward Kmett
+-- License	 : BSD
+--
+-- Maintainer	: Edward Kmett <ekmett@gmail.com>
+-- Stability	: experimental
+-- Portability	: non-portable (class-associated types)
+--
+-- A 'Monoidal' category is a category with an associated biendofunctor that has an identity,
+-- which satisfies Mac Lane''s pentagonal and triangular coherence conditions
+-- Technically we usually say that category is 'Monoidal', but since
+-- most interesting categories in our world have multiple candidate bifunctors that you can 
+-- use to enrich their structure, we choose here to think of the bifunctor as being 
+-- monoidal. This lets us reuse the same 'Bifunctor' over different categories without 
+-- painful newtype wrapping.
+
+-- The use of class associated types here makes Control.Category.Cartesian FAR more palatable
+-------------------------------------------------------------------------------------------
+
+module Control.Category.Monoidal 
+	( HasIdentity(..)
+	, Monoidal(..)
+	, Comonoidal(..)
+	) where
+
+import Control.Category.Braided
+import Control.Category.Associative
+import Control.Categorical.Bifunctor
+import Data.Void
+
+-- | Denotes that we have some reasonable notion of 'Identity' for a particular 'Bifunctor' in this 'Category'. This
+-- notion is currently used by both 'Monoidal' and 'Comonoidal'
+class Bifunctor p k k k => HasIdentity k p where
+    type Id k p :: *
+
+{- | A monoidal category. 'idl' and 'idr' are traditionally denoted lambda and rho
+ the triangle identity holds:
+
+> first idr = second idl . associate 
+> second idl = first idr . associate
+-}
+
+class (Associative k p, HasIdentity k p) => Monoidal k p where
+	idl :: k (p (Id k p) a) a
+	idr :: k (p a (Id k p)) a
+
+{- | A comonoidal category satisfies the dual form of the triangle identities
+
+> first idr = disassociate . second idl
+> second idl = disassociate . first idr
+
+This type class is also (ab)used for the inverse operations needed for a strict (co)monoidal category.
+A strict (co)monoidal category is one that is both 'Monoidal' and 'Comonoidal' and satisfies the following laws:
+
+> idr . coidr = id 
+> idl . coidl = id 
+> coidl . idl = id 
+> coidr . idr = id 
+
+-}
+class (Disassociative k p, HasIdentity k p) => Comonoidal k p where
+	coidl :: k a (p (Id k p) a)
+	coidr :: k a (p a (Id k p))
+
+{-# RULES
+-- "bimap id idl/associate" 	second idl . associate = first idr
+-- "bimap idr id/associate" 	first idr . associate = second idl
+-- "disassociate/bimap id idl"  disassociate . second idl = first idr
+-- "disassociate/bimap idr id"  disassociate . first idr = second idl
+"idr/coidr" idr . coidr = id
+"idl/coidl"	idl . coidl = id
+"coidl/idl"	coidl . idl = id
+"coidr/idr"	coidr . idr = id
+"idr/braid" idr . braid = idl
+"idl/braid" idl . braid = idr
+"braid/coidr" braid . coidr = coidl
+"braid/coidl" braid . coidl = coidr
+ #-}
+
+instance HasIdentity (->) (,) where
+    type Id (->) (,) = Void
+
+instance Monoidal (->) (,) where
+        idl = snd
+        idr = fst
+
diff --git a/Data/Void.hs b/Data/Void.hs
new file mode 100644
--- /dev/null
+++ b/Data/Void.hs
@@ -0,0 +1,18 @@
+{-# OPTIONS_GHC -fglasgow-exts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Void
+-- Copyright   :  (C) 2008 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable (empty data declaration)
+--
+----------------------------------------------------------------------------
+module Data.Void where
+
+data Void
+
+void :: Void -> a
+void = undefined
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright 2008-2010 Edward Kmett
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR
+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/categories.cabal b/categories.cabal
new file mode 100644
--- /dev/null
+++ b/categories.cabal
@@ -0,0 +1,37 @@
+name:          categories
+category:      Control
+version:       0.54.0
+license:       BSD3
+cabal-version: >= 1.2
+license-file:  LICENSE
+author:        Edward A. Kmett
+maintainer:    Edward A. Kmett <ekmett@gmail.com>
+stability:     experimental
+homepage:      http://comonad.com/reader/
+synopsis:      categories from category-extras
+copyright:     Copyright (C) 2008-2010, Edward A. Kmett
+description:   categories from category-extras
+build-type:    Simple
+
+flag Optimize
+  description: Enable optimizations
+  default:     False
+
+library
+  exposed-modules:
+    Control.Categorical.Functor,
+    Control.Categorical.Bifunctor,
+    Control.Categorical.Object,
+    Control.Category.Monoidal,
+    Control.Category.Cartesian,
+    Control.Category.Cartesian.Closed,
+    Control.Category.Associative,
+    Control.Category.Braided,
+    Control.Category.Discrete,
+    Control.Category.Distributive,
+    Control.Category.Dual,
+    Data.Void
+  build-depends: base >= 4 && < 5
+  ghc-options: -Wall 
+  if flag(Optimize)
+    ghc-options: -funbox-strict-fields -O2