diff --git a/Control/Categorical/Bifunctor.hs b/Control/Categorical/Bifunctor.hs
--- a/Control/Categorical/Bifunctor.hs
+++ b/Control/Categorical/Bifunctor.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts #-}
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts, DefaultSignatures #-}
 -------------------------------------------------------------------------------------------
 -- |
 -- Module   : Control.Categorical.Bifunctor
@@ -12,8 +12,8 @@
 -- A more categorical definition of 'Bifunctor'
 -------------------------------------------------------------------------------------------
 module Control.Categorical.Bifunctor
-    ( PFunctor (first), firstDefault
-    , QFunctor (second), secondDefault
+    ( PFunctor (first)
+    , QFunctor (second)
     , Bifunctor (bimap)
     , dimap
     , difirst
@@ -25,31 +25,28 @@
 
 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
+    default first :: Bifunctor p r s t => r a b -> t (p a c) (p b c)
+    first f = bimap f id
 
 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)
+    default second :: Bifunctor q r s t => s a b -> t (q c a) (q c b)
+    second = bimap id
 
-{-# INLINE secondDefault #-}
-secondDefault :: Bifunctor p r s t => s a b -> t (p c a) (p c b)
-secondDefault = bimap id
+-- | Minimal definition: @bimap@ 
 
-instance QFunctor Either (->) (->) where
-    second = secondDefault
+-- or both @first@ and @second@
+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)
+    -- bimap f g = second g . first f
 
+instance PFunctor (,) (->) (->)
+instance QFunctor (,) (->) (->)
+instance Bifunctor (,) (->) (->) (->) where
+    bimap f g (a,b)= (f a, g b)
+
+instance PFunctor Either (->) (->)
+instance QFunctor Either (->) (->)
 instance Bifunctor Either (->) (->) (->) where
     bimap f _ (Left a) = Left (f a)
     bimap _ g (Right a) = Right (g a)
@@ -57,15 +54,8 @@
 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)
+difirst :: PFunctor f (Dual s) t => s b a -> t (f a c) (f b c)
+difirst = first . Dual
 
 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
--- a/Control/Categorical/Functor.hs
+++ b/Control/Categorical/Functor.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts, UndecidableInstances, FlexibleInstances #-}
+{-# LANGUAGE ConstraintKinds, MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts, UndecidableInstances, FlexibleInstances, DefaultSignatures #-}
 -------------------------------------------------------------------------------------------
 -- |
 -- Module      : Control.Categorical.Functor
@@ -11,9 +11,9 @@
 --
 -- A more categorical definition of 'Functor'
 -------------------------------------------------------------------------------------------
-module Control.Categorical.Functor 
-    ( Functor(fmap) 
-    , EndoFunctor
+module Control.Categorical.Functor
+    ( Functor(fmap)
+    , Endofunctor
     , LiftedFunctor(..)
     , LoweredFunctor(..)
     ) where
@@ -23,17 +23,16 @@
 import qualified Prelude
 #ifdef __GLASGOW_HASKELL__
 import Data.Data (Data(..), mkDataType, DataType, mkConstr, Constr, constrIndex, Fixity(..))
-import Data.Typeable (Typeable1(..), TyCon, mkTyCon, mkTyConApp, gcast1)
+import Data.Typeable (Typeable1(..), TyCon, mkTyCon3, mkTyConApp, gcast1)
 #endif
 
 -- TODO Data, Typeable
-newtype LiftedFunctor f a = LiftedFunctor (f a)
-    deriving (Show, Read)
+newtype LiftedFunctor f a = LiftedFunctor (f a) deriving (Show, Read)
 
 #ifdef __GLASGOW_HASKELL__
 
 liftedTyCon :: TyCon
-liftedTyCon = mkTyCon "Control.Categorical.Functor.LiftedFunctor"
+liftedTyCon = mkTyCon3 "categories" "Control.Categorical.Functor" "LiftedFunctor"
 {-# NOINLINE liftedTyCon #-}
 
 liftedConstr :: Constr
@@ -45,27 +44,26 @@
 {-# 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
+  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
+  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
 #endif
 
-newtype LoweredFunctor f a = LoweredFunctor (f a)
-    deriving (Show, Read)
+newtype LoweredFunctor f a = LoweredFunctor (f a) deriving (Show, Read)
 
 #ifdef __GLASGOW_HASKELL__
 
 loweredTyCon :: TyCon
-loweredTyCon = mkTyCon "Control.Categorical.Functor.LoweredFunctor"
+loweredTyCon = mkTyCon3 "categories" "Control.Categorical.Functor" "LoweredFunctor"
 {-# NOINLINE loweredTyCon #-}
 
 loweredConstr :: Constr
@@ -77,45 +75,46 @@
 {-# 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
+  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
+  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
 
 #endif
 
 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)
+  fmap :: r a b -> t (f a) (f b)
+  default fmap :: Prelude.Functor f => (a -> b) -> f a -> f b
+  fmap = Prelude.fmap
 
 instance Functor f (->) (->) => Prelude.Functor (LoweredFunctor f) where
-    fmap f (LoweredFunctor a) = LoweredFunctor (Control.Categorical.Functor.fmap f a)
+  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)
+  fmap f (LiftedFunctor a) = LiftedFunctor (Prelude.fmap f a)
 
 instance Functor ((,) a) (->) (->) where
-    fmap f ~(a, b) = (a, f b)
+  fmap f (a, b) = (a, f b)
 
 instance Functor (Either a) (->) (->) where
-    fmap _ (Left a) = Left a 
-    fmap f (Right a) = Right (f a)
+  fmap _ (Left a) = Left a
+  fmap f (Right a) = Right (f a)
 
 instance Functor Maybe (->) (->) where
-    fmap = Prelude.fmap
+  fmap = Prelude.fmap
 
 instance Functor [] (->) (->) where
-    fmap = Prelude.fmap
+  fmap = Prelude.fmap
 
 instance Functor IO (->) (->) where
-    fmap = Prelude.fmap
+  fmap = Prelude.fmap
 
-class (Functor f (~>) (~>)) => EndoFunctor f (~>)
-instance (Functor f (~>) (~>)) => EndoFunctor f (~>)
+type Endofunctor f a = Functor f a a
diff --git a/Control/Categorical/Object.hs b/Control/Categorical/Object.hs
--- a/Control/Categorical/Object.hs
+++ b/Control/Categorical/Object.hs
@@ -2,7 +2,7 @@
 -------------------------------------------------------------------------------------------
 -- |
 -- Module   : Control.Category.Object
--- Copyright: 2010 Edward Kmett
+-- Copyright: 2010-2012 Edward Kmett
 -- License  : BSD
 --
 -- Maintainer : Edward Kmett <ekmett@gmail.com>
@@ -10,26 +10,26 @@
 -- 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 
+module Control.Categorical.Object
     ( HasTerminalObject(..)
     , HasInitialObject(..)
     ) where
 
 import Control.Category
 
--- | The @Category (~>)@ has a terminal object @Terminal (~>)@ such that for all objects @a@ in @(~>)@, 
+-- | 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 (~>)
+class Category k => HasTerminalObject k where
+    type Terminal k :: *
+    terminate :: a `k` Terminal k
 
--- | The @Category (~>)@ has an initial (coterminal) object @Initial (~>)@ such that for all objects 
+-- | 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
+class Category k => HasInitialObject k where
+    type Initial k :: *
+    initiate :: Initial k `k` a
diff --git a/Control/Category/Associative.hs b/Control/Category/Associative.hs
--- a/Control/Category/Associative.hs
+++ b/Control/Category/Associative.hs
@@ -9,13 +9,12 @@
 -- Stability   : experimental
 -- Portability : portable
 --
--- NB: this contradicts another common meaning for an 'Associative' 'Category', which is one 
+-- 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 
+module Control.Category.Associative
     ( Associative(..)
-    , Disassociative(..)
     ) where
 
 import Control.Categorical.Bifunctor
@@ -23,16 +22,11 @@
 {- | A category with an associative bifunctor satisfying Mac Lane\'s pentagonal coherence identity law:
 
 > bimap id associate . associate . bimap associate id = associate . associate
+> bimap disassociate id . disassociate . bimap id disassociate = disassociate . disassociate
 -}
 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)
+    disassociate :: k (p a (p b c)) (p (p a b) c)
 
 {-- RULES
 "copentagonal coherence" first disassociate . disassociate . second disassociate = disassociate . disassociate
@@ -41,16 +35,12 @@
 
 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
--- a/Control/Category/Braided.hs
+++ b/Control/Category/Braided.hs
@@ -1,38 +1,38 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 -------------------------------------------------------------------------------------------
 -- |
--- Module	 : Control.Category.Braided
--- Copyright     : 2008-2011 Edward Kmett
--- License	 : BSD
+-- Module     : Control.Category.Braided
+-- Copyright  : 2008-2012 Edward Kmett
+-- License    : BSD
 --
--- Maintainer	: Edward Kmett <ekmett@gmail.com>
--- Stability	: experimental
--- Portability	: portable
+-- Maintainer : Edward Kmett <ekmett@gmail.com>
+-- Stability  : experimental
+-- Portability: portable
 --
 -------------------------------------------------------------------------------------------
-module Control.Category.Braided 
-	( Braided(..)
-	, Symmetric
-	, swap
-	) where
+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:
 
-> associate . braid . associate = second braid . associate . first braid 
-> disassociate . braid . disassociate = first braid . disassociate . second braid 
+> associate . braid . associate = second braid . associate . first braid
+> disassociate . braid . disassociate = first braid . disassociate . second braid
 
 If the category is Monoidal the following laws should be satisfied
 
-> idr . braid = idl 
-> idl . braid = idr 
+> idr . braid = idl
+> idl . braid = idr
 
-If the category is Comonoidal the following laws should be satisfied 
+If the category is Comonoidal the following laws should be satisfied
 
-> braid . coidr = coidl 
-> braid . coidl = coidr 
+> braid . coidr = coidl
+> braid . coidl = coidr
 
 -}
 
@@ -65,7 +65,5 @@
 "swap/swap" swap . swap = id
   --}
 
-
-instance Symmetric (->) Either 
-
+instance Symmetric (->) Either
 instance Symmetric (->) (,)
diff --git a/Control/Category/Cartesian.hs b/Control/Category/Cartesian.hs
--- a/Control/Category/Cartesian.hs
+++ b/Control/Category/Cartesian.hs
@@ -11,18 +11,14 @@
 --
 -------------------------------------------------------------------------------------------
 module Control.Category.Cartesian
-    ( 
-    -- * Pre-(Co)Cartesian categories
-      PreCartesian(..)
+    (
+    -- * (Co)Cartesian categories
+      Cartesian(..)
     , bimapProduct, braidProduct, associateProduct, disassociateProduct
-    , PreCoCartesian(..)
+    , CoCartesian(..)
     , 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)
@@ -34,23 +30,12 @@
 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: 
+Minimum definition:
 
-> fst, snd, diag 
+> fst, snd, diag
 > fst, snd, (&&&)
 -}
-class ( Associative k (Product k)
-      , Disassociative k (Product k)
-      , Symmetric k (Product k)
-      , Braided k (Product k)
-      ) => PreCartesian k where
+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
@@ -60,7 +45,6 @@
     diag = id &&& id
     f &&& g = bimap f g . diag
 
-
 {-- RULES
 "fst . diag"      fst . diag = id
 "snd . diag"    snd . diag = id
@@ -68,53 +52,38 @@
 "snd . f &&& g" forall f g. snd . (f &&& g) = g
  --}
 
-instance PreCartesian (->) where
+instance Cartesian (->) where
     type Product (->) = (,)
     fst = Prelude.fst
     snd = Prelude.snd
     diag a = (a,a)
     (f &&& g) a = (f a, g a)
 
--- alias
-class ( Monoidal k (Product k)
-      , PreCartesian k
-      ) => Cartesian k
-instance ( Monoidal k (Product k)
-         , PreCartesian k
-         ) => Cartesian k
-
 -- | free construction of 'Bifunctor' for the product 'Bifunctor' @Product k@ if @(&&&)@ is known
-bimapProduct :: (PreCartesian k, (<*>) ~ Product k) => (a `k` c) -> (b `k` d) -> (a <*> b) `k` (c <*> d)
+bimapProduct :: Cartesian k => k a c -> k b d -> Product k a b `k` Product k c d
 bimapProduct f g = (f . fst) &&& (g . snd)
-    
+
 -- | free construction of 'Braided' for the product 'Bifunctor' @Product k@
--- braidProduct :: (PreCartesian k, Product k ~ (<*>))  => a <*> b ~> b <*> a
-braidProduct :: (PreCartesian k) => Product k a b `k` Product k b a
+braidProduct :: Cartesian k => k (Product k a b) (Product k b a)
 braidProduct = snd &&& fst
 
 -- | free construction of 'Associative' for the product 'Bifunctor' @Product k@
--- associateProduct :: (PreCartesian k, (<*>) ~ Product k)  => (a <*> b) <*> c ~> (a <*> (b <*> c))
-associateProduct :: (PreCartesian k) => Product k (Product k a b) c `k` Product k a (Product k b c)
+associateProduct :: Cartesian k => Product k (Product k a b) c `k` Product k a (Product k b c)
 associateProduct = (fst . fst) &&& first snd
 
 -- | free construction of 'Disassociative' for the product 'Bifunctor' @Product k@
--- disassociateProduct:: (PreCartesian k,  (<*>) ~ Product k) => a <*> (b <*> c) ~> (a <*> b) <*> c
-disassociateProduct:: (PreCartesian k) => Product k a (Product k b c) `k` Product k (Product k a b) c
-disassociateProduct= braid . second braid . associateProduct . first braid . braid 
+disassociateProduct:: Cartesian k => Product k a (Product k b c) `k` Product k (Product k a b) c
+disassociateProduct= braid . second braid . associateProduct . first braid . braid
 
--- * Co-PreCartesian categories
+-- * Co-Cartesian categories
 
 -- a category that has finite coproducts, weakened the same way as PreCartesian above was weakened
-class ( Associative k (Sum k)
-      , Disassociative k (Sum k)
-      , Symmetric k (Product k)
-      , Braided k (Sum k)
-      ) => PreCoCartesian k where
+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
-    (|||) :: (a `k` c) -> (b `k` c) -> Sum k a b `k` c
+    (|||) :: k a c -> k b c -> Sum k a b `k` c
 
     codiag = id ||| id
     f ||| g = codiag . bimap f g
@@ -126,38 +95,27 @@
 "(f ||| g) . inr" forall f g. (f ||| g) . inr = g
  --}
 
-instance PreCoCartesian (->) where
+instance CoCartesian (->) where
     type Sum (->) = Either
     inl = Left
     inr = Right
     codiag (Left a) = a
     codiag (Right a) = a
-    (f ||| _) (Left a) = f a 
+    (f ||| _) (Left a) = f a
     (_ ||| g) (Right a) = g a
 
 -- | free construction of 'Bifunctor' for the coproduct 'Bifunctor' @Sum k@ if @(|||)@ is known
-bimapSum :: (PreCoCartesian k, Sum k ~ (+)) => (a `k` c) -> (b `k` d) -> (a + b) `k` (c + d)
+bimapSum :: CoCartesian k => k a c -> k b d -> Sum k a b `k` Sum k c d
 bimapSum f g = (inl . f) ||| (inr . g)
 
 -- | free construction of 'Braided' for the coproduct 'Bifunctor' @Sum k@
-braidSum :: (PreCoCartesian k, (+) ~ Sum k) => (a + b) `k` (b + a)
+braidSum :: CoCartesian k => Sum k a b `k` Sum k b a
 braidSum = inr ||| inl
 
 -- | free construction of 'Associative' for the coproduct 'Bifunctor' @Sum k@
--- associateSum :: (PreCoCartesian k, (+) ~ Sum k) => ((a + b) + c) ~> (a + (b + c))
-associateSum :: (PreCoCartesian k) => Sum k (Sum k a b) c `k` Sum k a (Sum k b c)
+associateSum :: CoCartesian k => Sum k (Sum k a b) c `k` Sum k a (Sum k b c)
 associateSum = braid . first braid . disassociateSum . second braid . braid
 
 -- | free construction of 'Disassociative' for the coproduct 'Bifunctor' @Sum k@
--- disassociateSum :: (PreCoCartesian k, (+) ~ Sum k) => (a + (b + c)) ~> ((a + b) + c)
-disassociateSum :: (PreCoCartesian k) => Sum k a (Sum k b c) `k` Sum k (Sum k a b) c
+disassociateSum :: CoCartesian k => Sum k a (Sum k b c) `k` Sum k (Sum k a b) c
 disassociateSum = (inl . inl) ||| first inr
-
-class 
-    ( Comonoidal k (Sum k)
-    , PreCoCartesian k
-    ) => CoCartesian k
-instance 
-    ( Comonoidal k (Sum k)
-    , PreCoCartesian k
-    ) => CoCartesian k
diff --git a/Control/Category/Cartesian/Closed.hs b/Control/Category/Cartesian/Closed.hs
--- a/Control/Category/Cartesian/Closed.hs
+++ b/Control/Category/Cartesian/Closed.hs
@@ -2,16 +2,16 @@
 -------------------------------------------------------------------------------------------
 -- |
 -- Module     : Control.Category.Cartesian.Closed
--- Copyright : 2008 Edward Kmett
--- License     : BSD
+-- Copyright  : 2008 Edward Kmett
+-- License    : BSD
 --
--- Maintainer    : Edward Kmett <ekmett@gmail.com>
--- Stability    : experimental
--- Portability    : non-portable (class-associated types)
+-- 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
@@ -26,24 +26,19 @@
 import Control.Category
 import Control.Category.Braided
 import Control.Category.Cartesian
-import Control.Category.Monoidal
 
--- * Closed Cartesian Category 
+-- * 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)
+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 (->) = (->)
@@ -58,41 +53,33 @@
  #-}
 
 -- * Free @'Adjunction' (Product (<=) a) (Exp (<=) a) (<=) (<=)@
-
--- unitCCC :: (CCC (<=), (<*>) ~ Product (<=), (<\>) ~ Exp (<=)) => a <= b <\> (b <*> a)
-unitCCC :: CCC (<=) => a <= Exp (<=) b (Product (<=) b a)
+unitCCC :: CCC k => a `k` Exp k b (Product k b a)
 unitCCC = curry braid
 
--- counitCCC :: (CCC (<=), (<*>) ~ Product (<=), (<\>) ~ Exp (<=)) => (b <*> (b <\> a)) <= a
-counitCCC :: CCC (<=) => (Product (<=) b (Exp (<=) b a)) <= a
+counitCCC :: CCC k => Product k b (Exp k b a) `k` a
 counitCCC = apply . braid
 
--- * A Co-(Closed Cartesian Category) 
+-- * 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)
+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 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 :: CoCCC k => a `k` Sum k b (Coexp k b a)
 unitCoCCC = swap . coapply
 
-counitCoCCC :: (CoCCC (<=), subtract ~ Coexp (<=), (+) ~ Sum (<=)) => subtract b (b + a) <= a
+counitCoCCC :: CoCCC k => Coexp k b (Sum k b a) `k` a
 counitCoCCC = cocurry swap
diff --git a/Control/Category/Discrete.hs b/Control/Category/Discrete.hs
--- a/Control/Category/Discrete.hs
+++ b/Control/Category/Discrete.hs
@@ -19,10 +19,9 @@
 
 import Prelude ()
 import Control.Category
--- import Unsafe.Coerce (unsafeCoerce)
 
 -- | Category of discrete objects. The only arrows are identity arrows.
-data Discrete a b where 
+data Discrete a b where
     Refl :: Discrete a a
 
 instance Category Discrete where
@@ -40,6 +39,6 @@
 cast :: Category k => Discrete a b -> k 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
--- a/Control/Category/Distributive.hs
+++ b/Control/Category/Distributive.hs
@@ -11,7 +11,7 @@
 --
 -------------------------------------------------------------------------------------------
 module Control.Category.Distributive
-    ( 
+    (
     -- * Distributive Categories
       factor
     , Distributive(..)
@@ -23,27 +23,13 @@
 import Control.Category.Cartesian
 
 -- | The canonical factoring morphism.
--- 
--- > factor :: ( PreCartesian k
--- >         , (*) ~ Product k
--- >         , PreCoCartesian k
--- >         , (+) ~ Sum k 
--- >         ) => ((a * b) + (a * c)) `k` (a * (b + c))
 
-factor :: ( PreCartesian k
-          , PreCoCartesian k
-          ) => Sum k (Product k a b) (Product k a c) `k` Product k a (Sum k b c)
+factor :: (Cartesian k, CoCartesian k) => Sum k (Product k a b) (Product k a c) `k` Product k a (Sum k b c)
 factor = second inl ||| second inr
 
 -- | A category in which 'factor' is an isomorphism
---
--- > class ( PreCartesian k 
--- >       , (*) ~ Product k
--- >       , PreCoCartesian k
--- >       , (+) ~ Sum k 
--- >       ) => Distributive k where
 
-class (PreCartesian k, PreCoCartesian k) => Distributive k where
+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
diff --git a/Control/Category/Dual.hs b/Control/Category/Dual.hs
--- a/Control/Category/Dual.hs
+++ b/Control/Category/Dual.hs
@@ -1,41 +1,41 @@
 {-# LANGUAGE TypeOperators, FlexibleContexts #-}
 -------------------------------------------------------------------------------------------
 -- |
--- Module	: Control.Category.Dual
--- Copyright    : 2008-2010 Edward Kmett
--- License      : BSD
+-- Module   : Control.Category.Dual
+-- Copyright: 2008-2010 Edward Kmett
+-- License  : BSD
 --
--- Maintainer	: Edward Kmett <ekmett@gmail.com>
--- Stability	: experimental
--- Portability	: portable
+-- Maintainer : Edward Kmett <ekmett@gmail.com>
+-- Stability  : experimental
+-- Portability: portable
 --
 -------------------------------------------------------------------------------------------
 module Control.Category.Dual
-	( Dual(..)
-	) where
+  ( Dual(..)
+  ) where
 
 import Prelude (undefined,const,error)
 import Control.Category
 
 #ifdef __GLASGOW_HASKELL__
 import Data.Data (Data(..), mkDataType, DataType, mkConstr, Constr, constrIndex, Fixity(..))
-import Data.Typeable (Typeable2(..), TyCon, mkTyCon, mkTyConApp, gcast1)
+import Data.Typeable (Typeable2(..), TyCon, mkTyCon3, mkTyConApp, gcast1)
 #endif
 
-data Dual k a b = Dual { runDual :: k b a } 
+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)
+  id = Dual id
+  Dual f . Dual g = Dual (g . f)
 
 #ifdef __GLASGOW_HASKELL__
 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
+  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"
+dataTyCon = mkTyCon3 "categories" "Control.Category.Dual" "Dual"
 {-# NOINLINE dataTyCon #-}
 
 dualConstr :: Constr
@@ -47,11 +47,11 @@
 {-# 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
+  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
 #endif
diff --git a/Control/Category/Monoidal.hs b/Control/Category/Monoidal.hs
--- a/Control/Category/Monoidal.hs
+++ b/Control/Category/Monoidal.hs
@@ -1,97 +1,81 @@
 {-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}
 -------------------------------------------------------------------------------------------
 -- |
--- Module	 : Control.Category.Monoidal
--- Copyright : 2008 Edward Kmett
--- License	 : BSD
+-- Module    : Control.Category.Monoidal
+-- Copyright : 2008,2012 Edward Kmett
+-- License   : BSD
 --
--- Maintainer	: Edward Kmett <ekmett@gmail.com>
--- Stability	: experimental
--- Portability	: non-portable (class-associated types)
+-- 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 
+-- 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 
-	( Id
-	, Monoidal(..)
-	, Comonoidal(..)
-	) where
+module Control.Category.Monoidal
+  ( Monoidal(..)
+  ) where
 
 import Control.Category.Associative
 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'
-type family Id (k :: * -> * -> *) (p :: * -> * -> *) :: *
 
 {- | A monoidal category. 'idl' and 'idr' are traditionally denoted lambda and rho
- the triangle identity holds:
+ the triangle identities hold:
 
-> first idr = second idl . associate 
+> first idr = second idl . associate
 > second idl = first idr . associate
--}
-
-class Associative 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 
+> idr . coidr = id
+> idl . coidl = id
+> coidl . idl = id
+> coidr . idr = id
 
 -}
-class Disassociative k p => Comonoidal k p where
+
+class Associative k p => Monoidal (k :: * -> * -> *) (p :: * -> * -> *) where
+  type Id (k :: * -> * -> *) (p :: * -> * -> *) :: *
+  idl   :: k (p (Id k p) a) a
+  idr   :: k (p a (Id k p)) a
   coidl :: k a (p (Id k p) a)
   coidr :: k a (p a (Id k p))
 
+instance Monoidal (->) (,) where
+  type Id (->) (,) = ()
+  idl = snd
+  idr = fst
+  coidl a = ((),a)
+  coidr a = (a,())
+
+instance Monoidal (->) Either where
+  type Id (->) Either = Void
+  idl = either absurd id
+  idr = either id absurd
+  coidl = Right
+  coidr = Left
+
 {-- RULES
--- "bimap id idl/associate" 	second idl . associate = first idr
--- "bimap idr id/associate" 	first idr . associate = second idl
+-- "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
+"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
  --}
 
-type instance Id (->) (,) = ()
-type instance Id (->) Either = Void
-
-instance Monoidal (->) (,) where
-  idl = snd
-  idr = fst
-
-instance Monoidal (->) Either where
-  idl = either absurd id
-  idr = either id absurd
-
-instance Comonoidal (->) (,) where
-  coidl a = ((),a)
-  coidr a = (a,())
-
-instance Comonoidal (->) Either where
-  coidl = Right
-  coidr = Left
diff --git a/categories.cabal b/categories.cabal
--- a/categories.cabal
+++ b/categories.cabal
@@ -1,16 +1,16 @@
 name:          categories
 category:      Control
-version:       0.59
+version:       1.0
 license:       BSD3
-cabal-version: >= 1.2.3
+cabal-version: >= 1.10
 license-file:  LICENSE
 author:        Edward A. Kmett
 maintainer:    Edward A. Kmett <ekmett@gmail.com>
 stability:     experimental
 homepage:      http://github.com/ekmett/categories
-synopsis:      categories from category-extras
+synopsis:      Categories
 copyright:     Copyright (C) 2008-2010, Edward A. Kmett
-description:   categories from category-extras
+description:   Categories
 build-type:    Simple
 
 flag Optimize
@@ -18,7 +18,8 @@
   default:     False
 
 library
-  extensions: CPP 
+  default-language: Haskell2010
+  default-extensions: CPP
   other-extensions:
     MultiParamTypeClasses
     FunctionalDependencies
@@ -29,6 +30,9 @@
     TypeFamilies
     GADTs
 
+-- these extensions aren't yet known by my version of Cabal:
+-- other-extensions: DefaultSignatures ConstraintKinds
+
   exposed-modules:
     Control.Categorical.Functor,
     Control.Categorical.Bifunctor,
@@ -42,11 +46,11 @@
     Control.Category.Distributive,
     Control.Category.Dual
 
-  build-depends: 
+  build-depends:
     base >= 4 && < 5,
     void >= 0.5.4.2 && < 0.6
 
-  ghc-options: -Wall 
+  ghc-options: -Wall
 
   if flag(Optimize)
     ghc-options: -funbox-strict-fields -O2