diff --git a/Data/Category.hs b/Data/Category.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category.hs
@@ -0,0 +1,71 @@
+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes #-}
+module Data.Category where
+
+import Prelude hiding ((.), id, ($))
+
+
+
+class CategoryO (~>) a where
+  id :: a ~> a
+  
+class (CategoryO (~>) a, CategoryO (~>) b, CategoryO (~>) c) => CategoryA (~>) a b c where
+  (.) :: b ~> c -> a ~> b -> a ~> c
+
+class (CategoryO (~>) a, CategoryO (~>) b) => Apply (~>) a b where
+  -- Would have liked to use ($) here, but that causes GHC to crash.
+  -- http://hackage.haskell.org/trac/ghc/ticket/3297
+  ($$) :: a ~> b -> a -> b
+  
+
+type family F ftag a :: *
+type family Dom ftag :: * -> * -> *
+type family Cod ftag :: * -> * -> *
+
+class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b) 
+  => FunctorA ftag a b where
+  (%) :: ftag -> Dom ftag a b -> Cod ftag (F ftag a) (F ftag b)
+
+class (CategoryO (Dom ftag) a, CategoryO (Dom ftag) b) 
+  => ContraFunctorA ftag a b where
+  (-%) :: ftag -> Dom ftag a b -> Cod ftag (F ftag b) (F ftag a)
+
+
+-- |The identity functor on (~>)
+data Id ((~>) :: * -> * -> *) = Id
+type instance F (Id (~>)) a = a
+type instance Dom (Id (~>)) = (~>)
+type instance Cod (Id (~>)) = (~>)
+instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Id (~>)) a b where
+  Id % f = f
+
+-- |The composition of two functors.
+data (g :.: h) = g :.: h
+type instance F (g :.: h) a = F g (F h a)
+type instance Dom (g :.: h) = Dom h
+type instance Cod (g :.: h) = Cod g
+instance (FunctorA g (F h a) (F h b), FunctorA h a b, Cod h ~ Dom g) => FunctorA (g :.: h) a b where
+   (g :.: h) % f = g % (h % f)
+
+-- |The constant functor.
+data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x = Const
+type instance F (Const c1 c2 x) a = x
+type instance Dom (Const c1 c2 x) = c1
+type instance Cod (Const c1 c2 x) = c2
+instance (CategoryO c1 a, CategoryO c1 b, CategoryO c2 x) => FunctorA (Const c1 c2 x) a b where
+  Const % f = id
+  
+-- |The covariant functor Hom(X,--)
+data (x :*-: ((~>) :: * -> * -> *)) = HomX_
+type instance F (x :*-: (~>)) a = x ~> a
+type instance Dom (x :*-: (~>)) = (~>)
+type instance Cod (x :*-: (~>)) = (->)
+instance (CategoryO (~>) a, CategoryO (~>) b, CategoryA (~>) x a b) => FunctorA (x :*-: (~>)) a b where
+  HomX_ % f = (f .)
+
+-- |The contravariant functor Hom(--,X)
+data (((~>) :: * -> * -> *) :-*: x) = Hom_X
+type instance F ((~>) :-*: x) a = a ~> x
+type instance Dom ((~>) :-*: x) = (~>)
+type instance Cod ((~>) :-*: x) = (->)
+instance (CategoryO (~>) a, CategoryO (~>) b, CategoryA (~>) a b x) => ContraFunctorA ((~>) :-*: x) a b where
+  Hom_X -% f = (. f)
diff --git a/Data/Category/Boolean.hs b/Data/Category/Boolean.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Boolean.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}
+module Data.Category.Boolean where
+
+import Prelude hiding ((.), id)
+
+import Data.Category
+import Data.Category.Functor
+import Data.Category.Void
+import Data.Category.Pair
+
+
+-- "2", Boolean Category
+data family Boolean a b :: *
+
+data Fls = Fls deriving Show
+data Tru = Tru deriving Show
+
+data instance Boolean Fls Fls = IdFls
+data instance Boolean Tru Tru = IdTru
+data instance Boolean Fls Tru = FlsTru
+
+instance Apply Boolean Fls Fls where
+  IdFls $$ Fls = Fls
+instance Apply Boolean Fls Tru where
+  FlsTru $$ Fls = Tru
+instance Apply Boolean Tru Tru where
+  IdTru $$ Tru = Tru
+  
+instance CategoryO Boolean Fls where
+  id = IdFls
+instance CategoryO Boolean Tru where
+  id = IdTru
+
+instance CategoryA Boolean Fls Fls Fls where
+  IdFls . IdFls = IdFls
+instance CategoryA Boolean Fls Fls Tru where
+  FlsTru . IdFls = FlsTru  
+instance CategoryA Boolean Fls Tru Tru where
+  IdTru . FlsTru = FlsTru  
+instance CategoryA Boolean Tru Tru Tru where
+  IdTru . IdTru = IdTru
+  
+
+  
+data instance Funct Boolean d (FunctO Boolean d f) (FunctO Boolean d g) = 
+  BooleanNat { flsComp :: Component f g Fls, truComp :: Component f g Tru }
+instance (CategoryO (Cod f) (F f Fls), CategoryO (Cod f) (F f Tru)) => CategoryO (Funct Boolean d) (FunctO Boolean d f) where
+  id = BooleanNat id id
+
+instance VoidColimit Boolean where
+  type InitialObject Boolean = Fls
+  voidColimit = InitialUniversal VoidNat (BooleanNat (\VoidNat -> IdFls) (\VoidNat -> FlsTru))
+instance VoidLimit Boolean where
+  type TerminalObject Boolean = Tru
+  voidLimit = TerminalUniversal VoidNat (BooleanNat (\VoidNat -> FlsTru) (\VoidNat -> IdTru))
+
+instance PairLimit Boolean Fls Fls where 
+  type Product Fls Fls = Fls
+  pairLimit = TerminalUniversal (IdFls :***: IdFls) (BooleanNat fstComp sndComp)
+instance PairLimit Boolean Fls Tru where 
+  type Product Fls Tru = Fls
+  pairLimit = TerminalUniversal (IdFls :***: FlsTru) (BooleanNat fstComp fstComp)
+instance PairLimit Boolean Tru Fls where 
+  type Product Tru Fls = Fls
+  pairLimit = TerminalUniversal (FlsTru :***: IdFls) (BooleanNat sndComp sndComp)
+instance PairLimit Boolean Tru Tru where 
+  type Product Tru Tru = Tru
+  pairLimit = TerminalUniversal (IdTru :***: IdTru) (BooleanNat fstComp sndComp)
+
+instance PairColimit Boolean Fls Fls where 
+  type Coproduct Fls Fls = Fls
+  pairColimit = InitialUniversal (IdFls :***: IdFls) (BooleanNat fstComp sndComp)
+instance PairColimit Boolean Fls Tru where 
+  type Coproduct Fls Tru = Tru
+  pairColimit = InitialUniversal (FlsTru :***: IdTru) (BooleanNat sndComp sndComp)
+instance PairColimit Boolean Tru Fls where 
+  type Coproduct Tru Fls = Tru
+  pairColimit = InitialUniversal (IdTru :***: FlsTru) (BooleanNat fstComp fstComp)
+instance PairColimit Boolean Tru Tru where 
+  type Coproduct Tru Tru = Tru
+  pairColimit = InitialUniversal (IdTru :***: IdTru) (BooleanNat fstComp sndComp)
diff --git a/Data/Category/Functor.hs b/Data/Category/Functor.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Functor.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs #-}
+module Data.Category.Functor where
+  
+import Prelude hiding ((.), id)
+
+import Data.Category
+
+
+-- |Functor category Funct(C, D), or D^C.
+-- Arrows of Funct(C, D) are natural transformations.
+-- Each category C needs its own data instance.
+data family Funct (c :: * -> * -> *) (d :: * -> * -> *) (a :: *) (b :: *) :: *
+
+-- |Objects of Funct(C, D) are functors from C to D.
+data FunctO (c :: * -> * -> *) (d :: * -> * -> *) (f :: *) = (Dom f ~ c, Cod f ~ d) => FunctO f
+
+-- |Arrows of the category Funct(Funct(C, D), E)
+-- I.e. natural transformations between functors of type D^C -> E
+data instance Funct (Funct c d) e (FunctO (Funct c d) e f) (FunctO (Funct c d) e g) =
+  FunctNat (forall h. (Dom h ~ c, Cod h ~ d) => Component f g (FunctO c d h))
+
+
+type Component f g z = Cod f (F f z) (F g z)
+type f :~> g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Funct c d (FunctO c d f) (FunctO c d g)
+
+
+-- | The diagonal functor from (index-) category J to (~>).
+data Diag (j :: * -> * -> *) ((~>) :: * -> * -> *) = Diag
+type instance Dom (Diag j (~>)) = (~>)
+type instance Cod (Diag j (~>)) = Funct j (~>)
+type instance F (Diag j (~>)) a = FunctO j (~>) (Const j (~>) a)
+
+
+type InitMorF x u = (x :*-: Cod u) :.: u
+type TermMorF x u = (Cod u :-*: x) :.: u
+data InitialUniversal  x u a = InitialUniversal  (F (InitMorF x u) a) (InitMorF x u :~> (a :*-: Dom u))
+data TerminalUniversal x u a = TerminalUniversal (F (TermMorF x u) a) (TermMorF x u :~> (Dom u :-*: a))
+
+-- |A cone from N to F is a natural transformation from the constant functor to N to F.
+type Cone   f n = Const (Dom f) (Cod f) n :~> f
+-- |A co-cone from F to N is a natural transformation from F to the constant functor to N.
+type Cocone f n = f :~> Const (Dom f) (Cod f) n
+
+type Limit   f l = TerminalUniversal (FunctO (Dom f) (Cod f) f) (Diag (Dom f) (Cod f)) l
+type Colimit f l = InitialUniversal  (FunctO (Dom f) (Cod f) f) (Diag (Dom f) (Cod f)) l
+
+data Adjunction f g = Adjunction 
+  { unit :: Id (Dom f) :~> (g :.: f)
+  , counit :: (f :.: g) :~> Id (Dom g)
+  }
diff --git a/Data/Category/Hask.hs b/Data/Category/Hask.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Hask.hs
@@ -0,0 +1,77 @@
+{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, EmptyDataDecls #-}
+module Data.Category.Hask where
+
+import Prelude hiding ((.), id)
+import qualified Prelude
+import Control.Arrow ((&&&), (***), (+++))
+
+import Data.Category
+import Data.Category.Functor
+import Data.Category.Void
+import Data.Category.Pair
+
+type Hask = (->)
+
+instance Apply (->) a b where
+  ($$) = ($)
+
+instance CategoryO (->) a where
+  id = Prelude.id
+  
+instance CategoryA (->) a b c where
+  (.) = (Prelude..)
+
+
+
+newtype instance Funct (->) d (FunctO (->) d f) (FunctO (->) d g) = 
+  HaskNat { unHaskNat :: (forall a. CategoryO d (F f a) => Component f g a) }
+instance (Dom f ~ (->), Cod f ~ d) => CategoryO (Funct (->) d) (FunctO (->) d f) where
+  id = HaskNat id
+instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag (->) (~>)) a b where
+  Diag % f = HaskNat f
+
+
+data Zero
+-- With thanks to Conor McBride
+magic :: Zero -> a
+magic x = x `seq` error "we never get this far"
+
+instance VoidColimit (->) where
+  type InitialObject (->) = Zero
+  voidColimit = InitialUniversal VoidNat (HaskNat $ \VoidNat -> magic)
+instance VoidLimit (->) where
+  type TerminalObject (->) = ()
+  voidLimit = TerminalUniversal VoidNat (HaskNat $ \VoidNat -> const ())
+
+initObjInHask :: Limit (Id (->)) Zero
+initObjInHask = TerminalUniversal (HaskNat $ magic) (HaskNat unHaskNat)
+termObjInHask :: Colimit (Id (->)) ()
+termObjInHask = InitialUniversal (HaskNat $ const ()) (HaskNat unHaskNat)
+
+instance PairColimit (->) x y where
+  type Coproduct x y = Either x y
+  pairColimit = InitialUniversal (Left :***: Right) (HaskNat $ \(l :***: r) -> either l r)
+instance PairLimit (->) x y where
+  type Product x y = (x, y)
+  pairLimit = TerminalUniversal (fst :***: snd) (HaskNat $ \(f :***: s) -> f &&& s)
+
+
+data ProdInHask = ProdInHask
+type instance Dom ProdInHask = Funct Pair (->)
+type instance Cod ProdInHask = (->)
+type instance F ProdInHask (FunctO Pair (->) f) = (F f Fst, F f Snd)
+instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA ProdInHask (FunctO Pair (->) f) (FunctO Pair (->) g) where
+  ProdInHask % (f :***: g) = f *** g
+
+prodInHaskAdj :: Adjunction (Diag Pair (->)) ProdInHask
+prodInHaskAdj = Adjunction { unit = HaskNat $ id &&& id, counit = FunctNat $ fst :***: snd }
+
+data SumInHask = SumInHask
+type instance Dom SumInHask = Funct Pair (->)
+type instance Cod SumInHask = (->)
+type instance F SumInHask (FunctO Pair (->) f) = Either (F f Fst) (F f Snd)
+instance (Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA SumInHask (FunctO Pair (->) f) (FunctO Pair (->) g) where
+  SumInHask % (f :***: g) = f +++ g
+
+sumInHaskAdj :: Adjunction SumInHask (Diag Pair (->))
+sumInHaskAdj = Adjunction { unit = FunctNat $ Left :***: Right, counit = HaskNat $ either id id }
diff --git a/Data/Category/Kleisli.hs b/Data/Category/Kleisli.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Kleisli.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE TypeFamilies, TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}
+module Data.Category.Kleisli where
+  
+import Prelude hiding ((.), id, Monad(..))
+
+import Data.Category
+import Data.Category.Functor
+import Data.Category.Hask
+import Unsafe.Coerce
+
+class Pointed m where
+  point :: m -> Id (Cod m) :~> m
+  
+class Pointed m => Monad m where
+  join :: m -> (m :.: m) :~> m
+  
+data Kleisli ((~>) :: * -> * -> *) m a b = Kleisli (m -> a ~> F m b)
+
+instance (Monad m, Dom m ~ (->), Cod m ~ (->)) => CategoryO (Kleisli (->) m) o where
+  id = Kleisli $ \m -> unHaskNat (point m)
+instance (Monad m, Dom m ~ (->), Cod m ~ (->), FunctorA m b (F m c)) => CategoryA (Kleisli (->) m) a b c where
+  (Kleisli f) . (Kleisli g) = Kleisli $ \m -> unsafeCoerce (unHaskNat (join m)) . (m % f m) . g m
+newtype instance Funct (Kleisli (->) m) d (FunctO (Kleisli (->) m) d f) (FunctO (Kleisli (->) m) d g) = 
+  KleisliNat { unKleisliNat :: (forall a. CategoryO d (F f a) => Component f g a) }
+
+data KleisliAdjF ((~>) :: * -> * -> *) m = KleisliAdjF m
+type instance Dom (KleisliAdjF (~>) m) = (~>)
+type instance Cod (KleisliAdjF (~>) m) = Kleisli (~>) m
+type instance F (KleisliAdjF (~>) m) a = a
+instance (Monad m, Dom m ~ (->), Cod m ~ (->)) => FunctorA (KleisliAdjF (->) m) a b where
+  KleisliAdjF _ % f = Kleisli $ \m -> unHaskNat (point m) . f
+  
+data KleisliAdjG ((~>) :: * -> * -> *) m = KleisliAdjG m
+type instance Dom (KleisliAdjG (~>) m) = Kleisli (~>) m
+type instance Cod (KleisliAdjG (~>) m) = (~>)
+type instance F (KleisliAdjG (~>) m) a = F m a
+instance (Monad m, Dom m ~ (->), Cod m ~ (->), FunctorA m a (F m b)) => FunctorA (KleisliAdjG (->) m) a b where
+  KleisliAdjG m % Kleisli f = unsafeCoerce (unHaskNat (join m)) . (m % f m)
+
+instance (Pointed m, Dom m ~ (->), Cod m ~ (->)) => Pointed (KleisliAdjG (->) m :.: KleisliAdjF (->) m) where
+  point (KleisliAdjG m :.: _) = HaskNat (unHaskNat (point m))
+   
+kleisliAdj :: (Monad m, Dom m ~ (->), Cod m ~ (->)) => m -> Adjunction (KleisliAdjF (->) m) (KleisliAdjG (->) m)
+kleisliAdj m = Adjunction { unit = point (KleisliAdjG m :.: KleisliAdjF m), counit = KleisliNat (Kleisli $ \m -> undefined) }
diff --git a/Data/Category/Omega.hs b/Data/Category/Omega.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Omega.hs
@@ -0,0 +1,85 @@
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}
+module Data.Category.Omega where
+
+import Prelude hiding ((.), id)
+
+import Data.Category
+import Data.Category.Functor
+import Data.Category.Void
+import Data.Category.Pair
+
+
+-- Natural numbers, the omega Category 0 -> 1 -> 2 -> 3 ...
+data family Omega a b :: * 
+
+-- Objects
+data Z = Z deriving Show
+newtype S n = S { unS :: n } deriving Show
+
+-- Arrows, there's an arrow from a to b when a is less than or equal to b
+data instance Omega Z Z = IdZ
+newtype instance Omega Z (S n) = GTZ { unGTZ :: Omega Z n }
+newtype instance Omega (S a) (S b) = StepS { unStepS :: Omega a b }
+
+instance Apply Omega Z Z where
+  IdZ $$ Z = Z
+instance Apply Omega Z n => Apply Omega Z (S n) where
+  GTZ d $$ Z = S (d $$ Z)
+instance Apply Omega a b => Apply Omega (S a) (S b) where
+  StepS d $$ S a = S (d $$ a)
+
+instance CategoryO Omega Z where
+  id = IdZ
+instance (CategoryO Omega n) => CategoryO Omega (S n) where
+  id = StepS id
+
+instance (CategoryO Omega n) => CategoryA Omega Z Z n where
+  a . IdZ = a
+instance (CategoryA Omega Z n p) => CategoryA Omega Z (S n) (S p) where
+  (StepS a) . (GTZ n) = GTZ (a . n)
+instance (CategoryA Omega n p q) => CategoryA Omega (S n) (S p) (S q) where
+  (StepS a) . (StepS b) = StepS (a . b)
+
+
+data instance Funct Omega d (FunctO Omega d f) (FunctO Omega d g) = 
+  OmegaNat (Component f g Z) (forall n. CategoryO d (F f (S n)) => Component f g n -> Component f g (S n))
+instance (Dom f ~ Omega, Cod f ~ d, CategoryO (Cod f) (F f Z)) => CategoryO (Funct Omega d) (FunctO Omega d f) where
+  id = OmegaNat id (const id)
+
+instance VoidColimit Omega where
+  type InitialObject Omega = Z
+  voidColimit = InitialUniversal VoidNat (OmegaNat (\VoidNat -> IdZ) (\cpt VoidNat -> GTZ (cpt VoidNat)))
+
+-- The product in omega is the minimum.
+instance PairLimit Omega Z Z where 
+  type Product Z Z = Z
+  pairLimit = TerminalUniversal (IdZ :***: IdZ) (OmegaNat fstComp (\cpt -> sndComp))
+instance (PairLimit Omega Z n, Product Z n ~ Z) => PairLimit Omega Z (S n) where 
+  type Product Z (S n) = Z
+  pairLimit = TerminalUniversal (IdZ :***: GTZ p) (OmegaNat fstComp (\cpt -> fstComp)) where
+    TerminalUniversal (_ :***: p) _ = pairLimit :: Limit (PairF Omega Z n) (Product Z n)
+instance (PairLimit Omega n Z, Product n Z ~ Z) => PairLimit Omega (S n) Z where 
+  type Product (S n) Z = Z
+  pairLimit = TerminalUniversal (GTZ p :***: IdZ) (OmegaNat sndComp (\cpt -> sndComp)) where
+    TerminalUniversal (p :***: _) _ = pairLimit :: Limit (PairF Omega n Z) (Product n Z)
+instance (PairLimit Omega a b) => PairLimit Omega (S a) (S b) where 
+  type Product (S a) (S b) = S (Product a b)
+  pairLimit = TerminalUniversal (StepS p1 :***: StepS p2) undefined where
+    TerminalUniversal (p1 :***: p2) _ = pairLimit :: Limit (PairF Omega a b) (Product a b)
+
+-- The coproduct in omega is the maximum.
+instance PairColimit Omega Z Z where 
+  type Coproduct Z Z = Z
+  pairColimit = InitialUniversal (IdZ :***: IdZ) (OmegaNat fstComp (\cpt -> sndComp))
+instance (PairColimit Omega Z n, Coproduct Z n ~ n) => PairColimit Omega Z (S n) where 
+  type Coproduct Z (S n) = S n
+  pairColimit = InitialUniversal (GTZ p1 :***: StepS p2) (OmegaNat sndComp (\cpt -> sndComp)) where
+    InitialUniversal (p1 :***: p2) _ = pairColimit :: Colimit (PairF Omega Z n) (Coproduct Z n)
+instance (PairColimit Omega n Z, Coproduct n Z ~ n) => PairColimit Omega (S n) Z where 
+  type Coproduct (S n) Z = S n
+  pairColimit = InitialUniversal (StepS p1 :***: GTZ p2) (OmegaNat fstComp (\cpt -> fstComp)) where
+    InitialUniversal (p1 :***: p2) _ = pairColimit :: Colimit (PairF Omega n Z) (Coproduct n Z)
+instance (PairColimit Omega a b) => PairColimit Omega (S a) (S b) where 
+  type Coproduct (S a) (S b) = S (Coproduct a b)
+  pairColimit = InitialUniversal (StepS p1 :***: StepS p2) undefined where
+    InitialUniversal (p1 :***: p2) _ = pairColimit :: Colimit (PairF Omega a b) (Coproduct a b)
diff --git a/Data/Category/Pair.hs b/Data/Category/Pair.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Pair.hs
@@ -0,0 +1,64 @@
+{-# LANGUAGE TypeFamilies, TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, ScopedTypeVariables #-}
+module Data.Category.Pair where
+
+import Prelude hiding ((.), id)
+
+import Data.Category
+import Data.Category.Functor
+
+data family Pair a b :: *
+
+data Fst = Fst deriving Show
+data Snd = Snd deriving Show
+
+data instance Pair Fst Fst = IdFst
+data instance Pair Snd Snd = IdSnd
+
+instance Apply Pair Fst Fst where
+  IdFst $$ Fst = Fst
+instance Apply Pair Snd Snd where
+  IdSnd $$ Snd = Snd
+  
+instance CategoryO Pair Fst where
+  id = IdFst
+instance CategoryO Pair Snd where
+  id = IdSnd
+
+instance CategoryA Pair Fst Fst Fst where
+  IdFst . IdFst = IdFst
+instance CategoryA Pair Snd Snd Snd where
+  IdSnd . IdSnd = IdSnd
+
+data instance Funct Pair d (FunctO Pair d f) (FunctO Pair d g) = 
+  (:***:) { fstComp :: Component f g Fst, sndComp :: Component f g Snd }
+instance (CategoryO (Cod f) (F f Fst), CategoryO (Cod f) (F f Snd)) => CategoryO (Funct Pair d) (FunctO Pair d f) where
+  id = id :***: id
+instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag Pair (~>)) a b where
+  Diag % f = f :***: f
+
+
+data PairF ((~>) :: * -> * -> *) x y = PairF
+type instance Dom (PairF (~>) x y) = Pair
+type instance Cod (PairF (~>) x y) = (~>)
+type instance F (PairF (~>) x y) Fst = x
+type instance F (PairF (~>) x y) Snd = y
+instance (CategoryO (~>) x) => FunctorA (PairF (~>) x y) Fst Fst where
+  PairF % IdFst = id
+instance (CategoryO (~>) y) => FunctorA (PairF (~>) x y) Snd Snd where
+  PairF % IdSnd = id
+
+class (CategoryO (~>) x, CategoryO (~>) y) => PairLimit (~>) x y where
+  type Product x y :: *
+  pairLimit :: Limit (PairF (~>) x y) (Product x y)
+  proj1 :: Product x y ~> x
+  proj2 :: Product x y ~> y
+  proj1 = p where TerminalUniversal (p :***: _) _ = pairLimit :: Limit (PairF (~>) x y) (Product x y)
+  proj2 = p where TerminalUniversal (_ :***: p) _ = pairLimit :: Limit (PairF (~>) x y) (Product x y)
+class (CategoryO (~>) x, CategoryO (~>) y) => PairColimit (~>) x y where
+  type Coproduct x y :: *
+  pairColimit :: Colimit (PairF (~>) x y) (Coproduct x y)
+  inj1 :: x ~> Coproduct x y
+  inj2 :: y ~> Coproduct x y
+  inj1 = i where InitialUniversal (i :***: _) _ = pairColimit :: Colimit (PairF (~>) x y) (Coproduct x y)
+  inj2 = i where InitialUniversal (_ :***: i) _ = pairColimit :: Colimit (PairF (~>) x y) (Coproduct x y)
+  
diff --git a/Data/Category/Unit.hs b/Data/Category/Unit.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Unit.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}
+module Data.Category.Unit where
+
+import Data.Category
+
+-- "1", Singleton category
+data family Unit a b :: *
+
+data instance Unit () () = UnitId
+
+instance Apply Unit () () where
+  UnitId $$ () = ()
+  
+instance CategoryO Unit () where
+  id = UnitId
+instance CategoryA Unit () () () where
+  UnitId . UnitId = UnitId
diff --git a/Data/Category/Void.hs b/Data/Category/Void.hs
new file mode 100644
--- /dev/null
+++ b/Data/Category/Void.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE TypeFamilies, FlexibleInstances, MultiParamTypeClasses #-}
+module Data.Category.Void where
+
+import Data.Category
+import Data.Category.Functor
+
+-- Void, the empty category
+data family Void a b :: *
+
+data instance Funct Void d (FunctO Void d f) (FunctO Void d g) = 
+  VoidNat
+instance CategoryO (Funct Void d) (FunctO Void d f) where
+  id = VoidNat
+instance (CategoryO (~>) a, CategoryO (~>) b) => FunctorA (Diag Void (~>)) a b where
+  Diag % f = VoidNat
+
+data VoidF ((~>) :: * -> * -> *) = VoidF
+type instance Dom (VoidF (~>)) = Void
+type instance Cod (VoidF (~>)) = (~>)
+
+class VoidColimit (~>) where
+  type InitialObject (~>) :: *
+  voidColimit :: Colimit (VoidF (~>)) (InitialObject (~>))
+class VoidLimit (~>) where
+  type TerminalObject (~>) :: *
+  voidLimit :: Limit (VoidF (~>)) (TerminalObject (~>))
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,31 @@
+Copyright Sjoerd Visscher 2010
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Sjoerd Visscher nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,3 @@
+#!/usr/bin/env runhaskell
+> import Distribution.Simple
+> main = defaultMain
diff --git a/data-category.cabal b/data-category.cabal
new file mode 100644
--- /dev/null
+++ b/data-category.cabal
@@ -0,0 +1,26 @@
+name:                data-category
+version:             0.0.1
+synopsis:            Restricted categories
+description:         
+  Data-category is a collection of categories, and some categorical constructions on them.
+category:            Data
+license:             BSD3
+license-file:        LICENSE
+author:              Sjoerd Visscher
+maintainer:          sjoerd@w3future.com
+build-type:          Simple
+cabal-version:       >= 1.2
+
+Library
+  exposed-modules:     
+    Data.Category,
+    Data.Category.Functor,
+    Data.Category.Void,
+    Data.Category.Unit,
+    Data.Category.Pair,
+    Data.Category.Boolean,
+    Data.Category.Omega,
+    Data.Category.Hask,
+    Data.Category.Kleisli
+    
+  build-depends:       base >= 3 && < 5