diff --git a/.ghci b/.ghci
new file mode 100644
--- /dev/null
+++ b/.ghci
@@ -0,0 +1,1 @@
+:set -isrc -idist/build/autogen -optP-include -optPdist/build/autogen/cabal_macros.h
diff --git a/.gitignore b/.gitignore
new file mode 100644
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,13 @@
+dist
+docs
+wiki
+TAGS
+tags
+wip
+.DS_Store
+.*.swp
+.*.swo
+*.o
+*.hi
+*~
+*#
diff --git a/.travis.yml b/.travis.yml
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,1 +1,8 @@
 language: haskell
+notifications:
+  irc:
+    channels:
+      - "irc.freenode.org#haskell-lens"
+    skip_join: true
+    template:
+      - "\x0313categories\x03/\x0306%{branch}\x03 \x0314%{commit}\x03 %{build_url} %{message}"
diff --git a/.vim.custom b/.vim.custom
new file mode 100644
--- /dev/null
+++ b/.vim.custom
@@ -0,0 +1,31 @@
+" Add the following to your .vimrc to automatically load this on startup
+
+" if filereadable(".vim.custom")
+"     so .vim.custom
+" endif
+
+function StripTrailingWhitespace()
+  let myline=line(".")
+  let mycolumn = col(".")
+  silent %s/  *$//
+  call cursor(myline, mycolumn)
+endfunction
+
+" enable syntax highlighting
+syntax on
+
+" search for the tags file anywhere between here and /
+set tags=TAGS;/
+
+" highlight tabs and trailing spaces
+set listchars=tab:‗‗,trail:‗
+set list
+
+" f2 runs hasktags
+map <F2> :exec ":!hasktags -x -c --ignore src"<CR><CR>
+
+" strip trailing whitespace before saving
+" au BufWritePre *.hs,*.markdown silent! cal StripTrailingWhitespace()
+
+" rebuild hasktags after saving
+au BufWritePost *.hs silent! :exec ":!hasktags -x -c --ignore src"
diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.markdown
@@ -0,0 +1,4 @@
+1.0.5
+---
+* Removed the upper bound on void.
+* Added `README` and `CHANGELOG`
diff --git a/Control/Categorical/Bifunctor.hs b/Control/Categorical/Bifunctor.hs
deleted file mode 100644
--- a/Control/Categorical/Bifunctor.hs
+++ /dev/null
@@ -1,61 +0,0 @@
-{-# 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)
-    , QFunctor (second)
-    , 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)
---    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
-
--- | Minimal definition: @bimap@ 
-
--- 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 (,) (->) (->) where first f = bimap f id
-instance QFunctor (,) (->) (->) where second = bimap id
-instance Bifunctor (,) (->) (->) (->) where
-    bimap f g (a,b)= (f a, g b)
-
-instance PFunctor Either (->) (->) where first f = bimap f id
-instance QFunctor Either (->) (->) where second = bimap id
-instance Bifunctor Either (->) (->) (->) where
-    bimap f _ (Left a) = Left (f a)
-    bimap _ g (Right a) = Right (g a)
-
-instance QFunctor (->) (->) (->) where
-    second = (.)
-
-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
deleted file mode 100644
--- a/Control/Categorical/Functor.hs
+++ /dev/null
@@ -1,137 +0,0 @@
-{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, 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
-
-#ifndef MIN_VERSION_base
-#define MIN_VERSION_base(x,y,z) 1
-#endif
-
-import Control.Category
-import Prelude hiding (id, (.), Functor(..))
-import qualified Prelude
-#ifdef __GLASGOW_HASKELL__
-import Data.Data (Data(..), mkDataType, DataType, mkConstr, Constr, constrIndex, Fixity(..))
-#if MIN_VERSION_base(4,4,0)
-import Data.Typeable (Typeable1(..), TyCon, mkTyCon3, mkTyConApp, gcast1)
-#else
-import Data.Typeable (Typeable1(..), TyCon, mkTyCon, mkTyConApp, gcast1)
-#endif
-#endif
-
--- TODO Data, Typeable
-newtype LiftedFunctor f a = LiftedFunctor (f a) deriving (Show, Read)
-
-#ifdef __GLASGOW_HASKELL__
-
-liftedTyCon :: TyCon
-#if MIN_VERSION_base(4,4,0)
-liftedTyCon = mkTyCon3 "categories" "Control.Categorical.Functor" "LiftedFunctor"
-#else
-liftedTyCon = mkTyCon "Control.Categorical.Functor.LiftedFunctor"
-#endif
-{-# 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
-#endif
-
-newtype LoweredFunctor f a = LoweredFunctor (f a) deriving (Show, Read)
-
-#ifdef __GLASGOW_HASKELL__
-
-loweredTyCon :: TyCon
-#if MIN_VERSION_base(4,4,0)
-loweredTyCon = mkTyCon3 "categories" "Control.Categorical.Functor" "LoweredFunctor"
-#else
-loweredTyCon = mkTyCon "Control.Categorical.Functor.LoweredFunctor"
-#endif
-{-# 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
-
-#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)
---  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)
-
-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 a a => Endofunctor f a
-instance Functor f a a => Endofunctor f a
diff --git a/Control/Categorical/Object.hs b/Control/Categorical/Object.hs
deleted file mode 100644
--- a/Control/Categorical/Object.hs
+++ /dev/null
@@ -1,35 +0,0 @@
-{-# LANGUAGE TypeFamilies, TypeOperators #-}
--------------------------------------------------------------------------------------------
--- |
--- Module   : Control.Category.Object
--- Copyright: 2010-2012 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 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
--- @a@ in @(~>)@, there exists a unique morphism from @Initial (~>) @ to @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
deleted file mode 100644
--- a/Control/Category/Associative.hs
+++ /dev/null
@@ -1,46 +0,0 @@
-{-# 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(..)
-    ) 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
-> 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))
-    disassociate :: k (p a (p b c)) (p (p 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))
-        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)
-        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
deleted file mode 100644
--- a/Control/Category/Braided.hs
+++ /dev/null
@@ -1,69 +0,0 @@
-{-# LANGUAGE MultiParamTypeClasses #-}
--------------------------------------------------------------------------------------------
--- |
--- Module     : Control.Category.Braided
--- Copyright  : 2008-2012 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:
-
-> 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
-
-If the category is Comonoidal the following laws should be satisfied
-
-> braid . coidr = coidl
-> braid . coidl = coidr
-
--}
-
-class Associative k p => 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
deleted file mode 100644
--- a/Control/Category/Cartesian.hs
+++ /dev/null
@@ -1,121 +0,0 @@
-{-# 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 = 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 Cartesian (->) where
-    type Product (->) = (,)
-    fst = Prelude.fst
-    snd = Prelude.snd
-    diag a = (a,a)
-    (f &&& g) a = (f a, g 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 f g = (f . fst) &&& (g . snd)
-
--- | free construction of 'Braided' for the product 'Bifunctor' @Product k@
-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 :: 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:: 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-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 = 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 CoCartesian (->) 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 k@ if @(|||)@ is known
-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 :: 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 :: 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 :: CoCartesian k => Sum k a (Sum k b c) `k` Sum k (Sum k a b) c
-disassociateSum = (inl . inl) ||| first inr
diff --git a/Control/Category/Cartesian/Closed.hs b/Control/Category/Cartesian/Closed.hs
deleted file mode 100644
--- a/Control/Category/Cartesian/Closed.hs
+++ /dev/null
@@ -1,85 +0,0 @@
-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, TypeOperators, FlexibleContexts #-}
--------------------------------------------------------------------------------------------
--- |
--- Module     : Control.Category.Cartesian.Closed
--- Copyright  : 2008 Edward Kmett
--- License    : BSD
---
--- Maintainer : Edward Kmett <ekmett@gmail.com>
--- Stability  : experimental
--- Portability: non-portable (class-associated types)
---
--------------------------------------------------------------------------------------------
-module Control.Category.Cartesian.Closed
-    (
-    -- * Cartesian Closed Category
-      CCC(..)
-    , unitCCC, counitCCC
-    -- * Co-(Cartesian Closed Category)
-    , CoCCC(..)
-    , unitCoCCC, counitCoCCC
-    ) where
-
-import Prelude ()
-import qualified Prelude
-
-import Control.Category
-import Control.Category.Braided
-import Control.Category.Cartesian
-
--- * Closed Cartesian Category
-
--- | A 'CCC' has full-fledged monoidal finite products and exponentials
-
--- Ideally you also want an instance for @'Bifunctor' ('Exp' hom) ('Dual' hom) hom hom@.
--- or at least @'Functor' ('Exp' hom a) hom hom@, which cannot be expressed in the constraints here.
-
-class Cartesian k => CCC k where
-    type Exp k :: * -> * -> *
-    apply :: Product k (Exp k a b) a `k` b
-    curry :: Product k a b `k` c -> a `k` Exp k b c
-    uncurry :: a `k` Exp k b c -> Product k a b `k` c
-
-instance CCC (->) where
-  type Exp (->) = (->)
-  apply (f,a) = f a
-  curry = Prelude.curry
-  uncurry = Prelude.uncurry
-
-{-# RULES
-"curry apply"         curry apply = id
--- "curry . uncurry"     curry . uncurry = id
--- "uncurry . curry"     uncurry . curry = id
- #-}
-
--- * Free @'Adjunction' (Product (<=) a) (Exp (<=) a) (<=) (<=)@
-unitCCC :: CCC k => a `k` Exp k b (Product k b a)
-unitCCC = curry braid
-
-counitCCC :: CCC k => Product k b (Exp k b a) `k` 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 k => CoCCC k where
-    type Coexp k :: * -> * -> *
-    coapply :: b `k` Sum k (Coexp k a b) a
-    cocurry :: c `k` Sum k a b -> Coexp k b c `k` a
-    uncocurry :: Coexp k b c `k` a -> c `k` Sum k a b
-
-{-# RULES
-"cocurry coapply" cocurry coapply = id
--- "cocurry . uncocurry"   cocurry . uncocurry = id
--- "uncocurry . cocurry"   uncocurry . cocurry = id
- #-}
-
--- * Free @'Adjunction' ('Coexp' (<=) a) ('Sum' (<=) a) (<=) (<=)@
-unitCoCCC :: CoCCC k => a `k` Sum k b (Coexp k b a)
-unitCoCCC = swap . coapply
-
-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
deleted file mode 100644
--- a/Control/Category/Discrete.hs
+++ /dev/null
@@ -1,44 +0,0 @@
-{-# 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
-
--- | 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
-
--- instance Groupoid Discrete where
---  inv 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 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
deleted file mode 100644
--- a/Control/Category/Distributive.hs
+++ /dev/null
@@ -1,42 +0,0 @@
-{-# 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 :: (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 (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 (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
deleted file mode 100644
--- a/Control/Category/Dual.hs
+++ /dev/null
@@ -1,69 +0,0 @@
-{-# LANGUAGE 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
-
-#ifndef MIN_VERSION_base
-#define MIN_VERSION_base(x,y,z) 1
-#endif
-
-import Prelude (undefined,const,error)
-import Control.Category
-
-#ifdef __GLASGOW_HASKELL__
-import Data.Data (Data(..), mkDataType, DataType, mkConstr, Constr, constrIndex, Fixity(..))
-#if MIN_VERSION_base(4,4,0)
-import Data.Typeable (Typeable2(..), TyCon, mkTyCon3, mkTyConApp, gcast1)
-#else
-import Data.Typeable (Typeable2(..), TyCon, mkTyCon, mkTyConApp, gcast1)
-#endif
-#endif
-
-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)
-
-#ifdef __GLASGOW_HASKELL__
-instance Typeable2 k => Typeable2 (Dual k) 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
-#if MIN_VERSION_base(4,4,0)
-dataTyCon = mkTyCon3 "categories" "Control.Category.Dual" "Dual"
-#else
-dataTyCon = mkTyCon "Control.Category.Dual.Dual"
-#endif
-{-# NOINLINE dataTyCon #-}
-
-dualConstr :: Constr
-dualConstr = mkConstr dataDataType "Dual" [] Prefix
-{-# NOINLINE dualConstr #-}
-
-dataDataType :: DataType
-dataDataType = mkDataType "Control.Category.Dual.Dual" [dualConstr]
-{-# NOINLINE dataDataType #-}
-
-instance (Typeable2 k, Data a, Data b, Data (k b a)) => Data (Dual k 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
-#endif
diff --git a/Control/Category/Monoidal.hs b/Control/Category/Monoidal.hs
deleted file mode 100644
--- a/Control/Category/Monoidal.hs
+++ /dev/null
@@ -1,81 +0,0 @@
-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}
--------------------------------------------------------------------------------------------
--- |
--- 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)
---
--- 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.
-
--------------------------------------------------------------------------------------------
-
-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'
-
-{- | A monoidal category. 'idl' and 'idr' are traditionally denoted lambda and rho
- the triangle identities hold:
-
-> first idr = second idl . associate
-> second idl = first idr . associate
-> first idr = disassociate . second idl
-> second idl = disassociate . first idr
-> idr . coidr = id
-> idl . coidl = id
-> coidl . idl = id
-> coidr . idr = id
-
--}
-
-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
--- "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
- --}
-
diff --git a/README.markdown b/README.markdown
new file mode 100644
--- /dev/null
+++ b/README.markdown
@@ -0,0 +1,15 @@
+categories
+==========
+
+[![Build Status](https://secure.travis-ci.org/ekmett/categories.png?branch=master)](http://travis-ci.org/ekmett/categories)
+
+This package provides a number of classes for working with `Category` instances with more structure in Haskell.
+
+Contact Information
+-------------------
+
+Contributions and bug reports are welcome!
+
+Please feel free to contact me through github or on the #haskell IRC channel on irc.freenode.net.
+
+-Edward Kmett
diff --git a/categories.cabal b/categories.cabal
--- a/categories.cabal
+++ b/categories.cabal
@@ -1,6 +1,6 @@
 name:          categories
 category:      Control
-version:       1.0.4
+version:       1.0.5
 license:       BSD3
 cabal-version: >= 1.10
 license-file:  LICENSE
@@ -13,8 +13,14 @@
 copyright:     Copyright (C) 2008-2010, Edward A. Kmett
 description:   Categories
 build-type:    Simple
-extra-source-files: .travis.yml
 tested-with:   GHC == 7.4.1, GHC == 7.6.1
+extra-source-files:
+  .ghci
+  .gitignore
+  .travis.yml
+  .vim.custom
+  README.markdown
+  CHANGELOG.markdown
 
 flag Optimize
   description: Enable optimizations
@@ -51,8 +57,9 @@
 
   build-depends:
     base >= 4 && < 5,
-    void >= 0.5.4.2 && < 0.6
+    void >= 0.5.4.2
 
+  hs-source-dirs: src
   ghc-options: -Wall
 
   if flag(Optimize)
diff --git a/src/Control/Categorical/Bifunctor.hs b/src/Control/Categorical/Bifunctor.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Categorical/Bifunctor.hs
@@ -0,0 +1,61 @@
+{-# 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)
+    , QFunctor (second)
+    , 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)
+--    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
+
+-- | Minimal definition: @bimap@ 
+
+-- 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 (,) (->) (->) where first f = bimap f id
+instance QFunctor (,) (->) (->) where second = bimap id
+instance Bifunctor (,) (->) (->) (->) where
+    bimap f g (a,b)= (f a, g b)
+
+instance PFunctor Either (->) (->) where first f = bimap f id
+instance QFunctor Either (->) (->) where second = bimap id
+instance Bifunctor Either (->) (->) (->) where
+    bimap f _ (Left a) = Left (f a)
+    bimap _ g (Right a) = Right (g a)
+
+instance QFunctor (->) (->) (->) where
+    second = (.)
+
+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/src/Control/Categorical/Functor.hs b/src/Control/Categorical/Functor.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Categorical/Functor.hs
@@ -0,0 +1,137 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, 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
+
+#ifndef MIN_VERSION_base
+#define MIN_VERSION_base(x,y,z) 1
+#endif
+
+import Control.Category
+import Prelude hiding (id, (.), Functor(..))
+import qualified Prelude
+#ifdef __GLASGOW_HASKELL__
+import Data.Data (Data(..), mkDataType, DataType, mkConstr, Constr, constrIndex, Fixity(..))
+#if MIN_VERSION_base(4,4,0)
+import Data.Typeable (Typeable1(..), TyCon, mkTyCon3, mkTyConApp, gcast1)
+#else
+import Data.Typeable (Typeable1(..), TyCon, mkTyCon, mkTyConApp, gcast1)
+#endif
+#endif
+
+-- TODO Data, Typeable
+newtype LiftedFunctor f a = LiftedFunctor (f a) deriving (Show, Read)
+
+#ifdef __GLASGOW_HASKELL__
+
+liftedTyCon :: TyCon
+#if MIN_VERSION_base(4,4,0)
+liftedTyCon = mkTyCon3 "categories" "Control.Categorical.Functor" "LiftedFunctor"
+#else
+liftedTyCon = mkTyCon "Control.Categorical.Functor.LiftedFunctor"
+#endif
+{-# 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
+#endif
+
+newtype LoweredFunctor f a = LoweredFunctor (f a) deriving (Show, Read)
+
+#ifdef __GLASGOW_HASKELL__
+
+loweredTyCon :: TyCon
+#if MIN_VERSION_base(4,4,0)
+loweredTyCon = mkTyCon3 "categories" "Control.Categorical.Functor" "LoweredFunctor"
+#else
+loweredTyCon = mkTyCon "Control.Categorical.Functor.LoweredFunctor"
+#endif
+{-# 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
+
+#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)
+--  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)
+
+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 a a => Endofunctor f a
+instance Functor f a a => Endofunctor f a
diff --git a/src/Control/Categorical/Object.hs b/src/Control/Categorical/Object.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Categorical/Object.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE TypeFamilies, TypeOperators #-}
+-------------------------------------------------------------------------------------------
+-- |
+-- Module   : Control.Category.Object
+-- Copyright: 2010-2012 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 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
+-- @a@ in @(~>)@, there exists a unique morphism from @Initial (~>) @ to @a@.
+
+class Category k => HasInitialObject k where
+    type Initial k :: *
+    initiate :: Initial k `k` a
diff --git a/src/Control/Category/Associative.hs b/src/Control/Category/Associative.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Category/Associative.hs
@@ -0,0 +1,46 @@
+{-# 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(..)
+    ) 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
+> 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))
+    disassociate :: k (p a (p b c)) (p (p 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))
+        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)
+        disassociate (Left a) = Left (Left a)
+        disassociate (Right (Left b)) = Left (Right b)
+        disassociate (Right (Right c)) = Right c
diff --git a/src/Control/Category/Braided.hs b/src/Control/Category/Braided.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Category/Braided.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+-------------------------------------------------------------------------------------------
+-- |
+-- Module     : Control.Category.Braided
+-- Copyright  : 2008-2012 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:
+
+> 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
+
+If the category is Comonoidal the following laws should be satisfied
+
+> braid . coidr = coidl
+> braid . coidl = coidr
+
+-}
+
+class Associative k p => 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/src/Control/Category/Cartesian.hs b/src/Control/Category/Cartesian.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Category/Cartesian.hs
@@ -0,0 +1,121 @@
+{-# 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 = 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 Cartesian (->) where
+    type Product (->) = (,)
+    fst = Prelude.fst
+    snd = Prelude.snd
+    diag a = (a,a)
+    (f &&& g) a = (f a, g 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 f g = (f . fst) &&& (g . snd)
+
+-- | free construction of 'Braided' for the product 'Bifunctor' @Product k@
+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 :: 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:: 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-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 = 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 CoCartesian (->) 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 k@ if @(|||)@ is known
+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 :: 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 :: 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 :: CoCartesian k => Sum k a (Sum k b c) `k` Sum k (Sum k a b) c
+disassociateSum = (inl . inl) ||| first inr
diff --git a/src/Control/Category/Cartesian/Closed.hs b/src/Control/Category/Cartesian/Closed.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Category/Cartesian/Closed.hs
@@ -0,0 +1,85 @@
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, TypeOperators, FlexibleContexts #-}
+-------------------------------------------------------------------------------------------
+-- |
+-- Module     : Control.Category.Cartesian.Closed
+-- Copyright  : 2008 Edward Kmett
+-- License    : BSD
+--
+-- Maintainer : Edward Kmett <ekmett@gmail.com>
+-- Stability  : experimental
+-- Portability: non-portable (class-associated types)
+--
+-------------------------------------------------------------------------------------------
+module Control.Category.Cartesian.Closed
+    (
+    -- * Cartesian Closed Category
+      CCC(..)
+    , unitCCC, counitCCC
+    -- * Co-(Cartesian Closed Category)
+    , CoCCC(..)
+    , unitCoCCC, counitCoCCC
+    ) where
+
+import Prelude ()
+import qualified Prelude
+
+import Control.Category
+import Control.Category.Braided
+import Control.Category.Cartesian
+
+-- * Closed Cartesian Category
+
+-- | A 'CCC' has full-fledged monoidal finite products and exponentials
+
+-- Ideally you also want an instance for @'Bifunctor' ('Exp' hom) ('Dual' hom) hom hom@.
+-- or at least @'Functor' ('Exp' hom a) hom hom@, which cannot be expressed in the constraints here.
+
+class Cartesian k => CCC k where
+    type Exp k :: * -> * -> *
+    apply :: Product k (Exp k a b) a `k` b
+    curry :: Product k a b `k` c -> a `k` Exp k b c
+    uncurry :: a `k` Exp k b c -> Product k a b `k` c
+
+instance CCC (->) where
+  type Exp (->) = (->)
+  apply (f,a) = f a
+  curry = Prelude.curry
+  uncurry = Prelude.uncurry
+
+{-# RULES
+"curry apply"         curry apply = id
+-- "curry . uncurry"     curry . uncurry = id
+-- "uncurry . curry"     uncurry . curry = id
+ #-}
+
+-- * Free @'Adjunction' (Product (<=) a) (Exp (<=) a) (<=) (<=)@
+unitCCC :: CCC k => a `k` Exp k b (Product k b a)
+unitCCC = curry braid
+
+counitCCC :: CCC k => Product k b (Exp k b a) `k` 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 k => CoCCC k where
+    type Coexp k :: * -> * -> *
+    coapply :: b `k` Sum k (Coexp k a b) a
+    cocurry :: c `k` Sum k a b -> Coexp k b c `k` a
+    uncocurry :: Coexp k b c `k` a -> c `k` Sum k a b
+
+{-# RULES
+"cocurry coapply" cocurry coapply = id
+-- "cocurry . uncocurry"   cocurry . uncocurry = id
+-- "uncocurry . cocurry"   uncocurry . cocurry = id
+ #-}
+
+-- * Free @'Adjunction' ('Coexp' (<=) a) ('Sum' (<=) a) (<=) (<=)@
+unitCoCCC :: CoCCC k => a `k` Sum k b (Coexp k b a)
+unitCoCCC = swap . coapply
+
+counitCoCCC :: CoCCC k => Coexp k b (Sum k b a) `k` a
+counitCoCCC = cocurry swap
diff --git a/src/Control/Category/Discrete.hs b/src/Control/Category/Discrete.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Category/Discrete.hs
@@ -0,0 +1,44 @@
+{-# 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
+
+-- | 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
+
+-- instance Groupoid Discrete where
+--  inv 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 k => Discrete a b -> k a b
+cast Refl = id
+
+-- |
+inverse :: Discrete a b -> Discrete b a
+inverse Refl = Refl
diff --git a/src/Control/Category/Distributive.hs b/src/Control/Category/Distributive.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Category/Distributive.hs
@@ -0,0 +1,42 @@
+{-# 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 :: (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 (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 (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/src/Control/Category/Dual.hs b/src/Control/Category/Dual.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Category/Dual.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE 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
+
+#ifndef MIN_VERSION_base
+#define MIN_VERSION_base(x,y,z) 1
+#endif
+
+import Prelude (undefined,const,error)
+import Control.Category
+
+#ifdef __GLASGOW_HASKELL__
+import Data.Data (Data(..), mkDataType, DataType, mkConstr, Constr, constrIndex, Fixity(..))
+#if MIN_VERSION_base(4,4,0)
+import Data.Typeable (Typeable2(..), TyCon, mkTyCon3, mkTyConApp, gcast1)
+#else
+import Data.Typeable (Typeable2(..), TyCon, mkTyCon, mkTyConApp, gcast1)
+#endif
+#endif
+
+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)
+
+#ifdef __GLASGOW_HASKELL__
+instance Typeable2 k => Typeable2 (Dual k) 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
+#if MIN_VERSION_base(4,4,0)
+dataTyCon = mkTyCon3 "categories" "Control.Category.Dual" "Dual"
+#else
+dataTyCon = mkTyCon "Control.Category.Dual.Dual"
+#endif
+{-# NOINLINE dataTyCon #-}
+
+dualConstr :: Constr
+dualConstr = mkConstr dataDataType "Dual" [] Prefix
+{-# NOINLINE dualConstr #-}
+
+dataDataType :: DataType
+dataDataType = mkDataType "Control.Category.Dual.Dual" [dualConstr]
+{-# NOINLINE dataDataType #-}
+
+instance (Typeable2 k, Data a, Data b, Data (k b a)) => Data (Dual k 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
+#endif
diff --git a/src/Control/Category/Monoidal.hs b/src/Control/Category/Monoidal.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Category/Monoidal.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}
+-------------------------------------------------------------------------------------------
+-- |
+-- 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)
+--
+-- 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.
+
+-------------------------------------------------------------------------------------------
+
+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'
+
+{- | A monoidal category. 'idl' and 'idr' are traditionally denoted lambda and rho
+ the triangle identities hold:
+
+> first idr = second idl . associate
+> second idl = first idr . associate
+> first idr = disassociate . second idl
+> second idl = disassociate . first idr
+> idr . coidr = id
+> idl . coidl = id
+> coidl . idl = id
+> coidr . idr = id
+
+-}
+
+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
+-- "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
+ --}
+