diff --git a/Category.hs b/Category.hs
new file mode 100644
--- /dev/null
+++ b/Category.hs
@@ -0,0 +1,32 @@
+module Category where
+
+import qualified Prelude as P
+import GHC.Prim
+import Data.Constraint
+
+-- |The class of categories @m@ with objects of kind @k@ which satisfy the
+-- constraint @Object m@. For any objects @a@ and @b@, the type @m a b@ is the
+-- type of morphisms with domain @a@ and codomain @b@.
+class Category (m :: k -> k -> *) where
+    -- |The set of objects.
+    type Object m (a :: k) :: Constraint
+    -- |The Identity operator.
+    id :: Object m a => m a a
+    -- |The Composition operator.
+    (.) :: m b c -> m a b -> m a c
+    -- |Morphisms are arrows between objects.
+    observeObjects :: m a b -> Dict (Object m a, Object m b)
+
+-- |The category Hask of functions between types.
+instance Category (->) where
+    type Object (->) a = ()
+    id = P.id
+    observeObjects = P.const Dict
+    (.) = (P..)
+
+-- |The category of entailment from 'constraints'
+instance Category (:-) where
+    type Object (:-) a = ()
+    id = refl
+    observeObjects = P.const Dict
+    (.) = trans
diff --git a/Category/Product.hs b/Category/Product.hs
new file mode 100644
--- /dev/null
+++ b/Category/Product.hs
@@ -0,0 +1,29 @@
+module Category.Product where
+
+import Data.Constraint
+import Data.Proxy
+import Data.Tagged
+
+import Category
+import Functor
+
+data (c1 :><: c2) a b where
+    (:><:) :: (a ~ '(L a, R a), b ~ '(L b, R b))  => c1 (L a) (L b) -> c2 (R a) (R b) -> (c1 :><: c2) a b
+
+type family L t where L '(a, b) = a
+type family R t where R '(a, b) = b
+
+instance (Category c1, Category c2) => Category (c1 :><: c2) where
+    type Object (c1 :><: c2) a = (Object c1 (L a), Object c2 (R a), a ~ '(L a, R a))
+    id = id :><: id
+    observeObjects (f :><: g)
+        | Dict <- observeObjects f, Dict <- observeObjects g = Dict
+    (f1 :><: f2) . (g1 :><: g2) = (f1 . g1) :><: (f2 . g2)
+
+data Diag c where Diag :: Category c => Diag c
+
+instance Category c => Functor (Diag (c :: k -> k -> *)) ('KProxy :: KProxy (k -> (k, k))) where
+    type Domain (Diag c) = c
+    type Codomain (Diag c) = c :><: c
+    type FMap (Diag c) (a :: k) = '(a, a)
+    morphMap = Tagged (\f -> f :><: f)
diff --git a/Functor.hs b/Functor.hs
new file mode 100644
--- /dev/null
+++ b/Functor.hs
@@ -0,0 +1,62 @@
+module Functor where
+
+import qualified Prelude as P
+import Data.Constraint
+import Data.Proxy
+import Data.Tagged
+
+import Category
+
+-- |The class of functors @f@ from @Domain f@ to @Codomain f@. Rather than
+-- indexing functors on the type of their object mapping, Functor is indexed on
+-- the phantom type variable @f@. This allows the object mapping to be any type
+-- family @FMap f@, and for multiple functors to exist between categories. As a
+-- consequence, a proxy @k@ for the  kind of @FMap f@ must be given as a second
+-- parameter to Functor.
+class (Category (Domain f :: o1 -> o1 -> *), Category (Codomain f :: o2 -> o2 -> *)) => Functor (f :: *) (k :: KProxy (o1 -> o2)) | f -> k where
+    -- |The mapping of objects of @Domain f@ to objects of @Codomain f@.
+    type FMap f (a :: o1) :: o2
+    -- |The domain of @f@.
+    type Domain f :: o1 -> o1 -> *
+    -- |The codomain of @f@.
+    type Codomain f :: o2 -> o2 -> *
+    -- |The mapping of morphisms of @Domain f@ to morphisms of @Codomain f@, tagged on the type @f@.
+    morphMap :: Tagged f (Domain f (a :: o1) (b :: o1) -> Codomain f (FMap f a :: o2) (FMap f b :: o2))
+
+-- |Proof that functors map objects to objects. Defines a functor from Cat to (:-).
+objectMap :: forall f (a :: o1). Functor f ('KProxy :: KProxy (o1 -> o2)) => Tagged '(f, a) (Object (Domain f) a :- Object (Codomain f) (FMap f a :: o2))
+objectMap = Tagged (Sub (case observeObjects (proxy morphMap (Proxy :: Proxy f) (id :: Domain f a a)) of Dict -> Dict))
+
+fmap :: forall f (a :: o1) (b :: o1). Functor f ('KProxy :: KProxy (o1 -> o2)) => f -> Domain f a b -> Codomain f (FMap f a :: o2) (FMap f b :: o2)
+fmap _ = proxy morphMap (Proxy :: Proxy f)
+
+-- |The composition of functors. The type variable @k@ is a proxy for the kind of the objects of the codomain of @g@.
+data Comp (k :: KProxy o2) (f :: *) (g :: *) where
+    (:.:) :: (Functor f ('KProxy :: KProxy (o2 -> o3)), Functor g ('KProxy :: KProxy (o1 -> o2)), (Domain f :: o2 -> o2 -> *) ~ Codomain g) =>
+        f -> g -> Comp ('KProxy :: KProxy o2) f g
+
+instance (Functor f ('KProxy :: KProxy (o2 -> o3)), Functor g ('KProxy :: KProxy (o1 -> o2)), (Domain f :: o2 -> o2 -> *) ~ Codomain g)
+        => Functor (Comp ('KProxy :: KProxy o2) f g) ('KProxy :: KProxy (o1 -> o3)) where
+    type FMap (Comp ('KProxy :: KProxy o2) f g) a = FMap f (FMap g a :: o2)
+    type Domain (Comp 'KProxy f g) = Domain g
+    type Codomain (Comp 'KProxy f g) = Codomain f
+    morphMap = Tagged (proxy morphMap (Proxy :: Proxy f) . proxy morphMap (Proxy :: Proxy g))
+
+-- |The identity functor.
+data IdentityF c where IdentityF :: Category c => IdentityF c
+
+instance Category c => Functor (IdentityF (c :: k -> k -> *)) ('KProxy :: KProxy (k -> k)) where
+    type Domain (IdentityF c) = c
+    type Codomain (IdentityF c) = c
+    type FMap (IdentityF c) (a :: k) = a
+    morphMap = Tagged id
+
+-- |Functors derived from Prelude's Functor.
+data CanonicalF (f :: * -> *) where
+    CanonicalF :: P.Functor f => CanonicalF f
+
+instance P.Functor f => Functor (CanonicalF f) ('KProxy :: KProxy (* -> *)) where
+    type FMap (CanonicalF f) a = f a
+    type Domain (CanonicalF f) = (->)
+    type Codomain (CanonicalF f) = (->)
+    morphMap = Tagged P.fmap
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2014, Ian Milligan
+
+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 Ian Milligan 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/Monoidal.hs b/Monoidal.hs
new file mode 100644
--- /dev/null
+++ b/Monoidal.hs
@@ -0,0 +1,16 @@
+module Monoidal where
+
+import Data.Tagged
+import Data.Proxy
+
+import Category
+import Category.Product
+import Functor
+
+class (Category c, Functor (Mu c) ('KProxy :: KProxy ((k, k) -> k)), Domain (Mu c) ~ (c :><: c), Codomain (Mu c) ~ c, Object c (I c)) =>
+        Monoidal (c :: k -> k -> *) where
+    type Mu c
+    type I c :: k
+
+(<>) :: forall c a1 a2 b1 b2. Monoidal c => c a1 b1 -> c a2 b2 -> c (FMap (Mu c) '(a1, a2)) (FMap (Mu c) '(b1, b2))
+f <> g = proxy morphMap (Proxy :: Proxy (Mu c)) (f :><: g)
diff --git a/NaturalTransformation.hs b/NaturalTransformation.hs
new file mode 100644
--- /dev/null
+++ b/NaturalTransformation.hs
@@ -0,0 +1,47 @@
+module NaturalTransformation where
+
+import Data.Constraint
+import Data.Tagged
+import Data.Proxy
+
+import Category
+import Category.Product
+import Functor
+import Monoidal
+
+data NatTr (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) (f :: *) (g :: *) where
+    NatTr :: (Object (NatTr c1 c2) f, Object (NatTr c1 c2) g) =>
+        (forall (a :: o1). Object c1 a => Tagged a (c2 (FMap f a :: o2) (FMap g a :: o2))) -> NatTr (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) f g
+
+instance (Category c1, Category c2) => Category (NatTr (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *)) where
+    type Object (NatTr c1 c2) f = (Functor f ('KProxy :: KProxy (o1 -> o2)), Domain f ~ c1, Codomain f ~ c2)
+    observeObjects (NatTr _) = Dict
+    id :: forall f. Object (NatTr c1 c2) f => NatTr c1 c2 f f
+    id = NatTr f where
+        f :: forall a. Object c1 a => Tagged a (c2 (FMap f a) (FMap f a))
+        f = Tagged (id \\ proxy objectMap (Proxy :: Proxy '(f, a)))
+    (.) :: forall g h f. NatTr c1 c2 g h -> NatTr c1 c2 f g -> NatTr c1 c2 f h
+    NatTr f . NatTr g = NatTr h where
+        h :: forall a. Object c1 a => Tagged a (c2 (FMap f a) (FMap h a))
+        h = Tagged (proxy f (Proxy :: Proxy a) . proxy g (Proxy :: Proxy a))
+
+data CompFF c1 c2 c3  where CompFF :: (Category c1, Category c2, Category c3) => CompFF c1 c2 c3
+
+instance (Category c1, Category c2, Category c3) =>
+        Functor (CompFF (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) (c3 :: o3 -> o3 -> *)) ('KProxy :: KProxy ((*, *) -> *)) where
+    type Domain (CompFF c1 c2 c3) = NatTr c2 c3 :><: NatTr c1 c2
+    type Codomain (CompFF c1 c2 c3) = NatTr c1 c3
+    type FMap (CompFF c1 c2 c3) '(f, g) = Comp ('KProxy :: KProxy o2) f g
+    morphMap = Tagged (\(t1 :><: t2) -> compNat t1 t2)
+
+compNat :: forall (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) (c3 :: o3 -> o3 -> *) f1 f2 g1 g2.
+    NatTr c2 c3 f1 g1 -> NatTr c1 c2 f2 g2 -> NatTr c1 c3 (Comp ('KProxy :: KProxy o2) f1 f2) (Comp ('KProxy :: KProxy o2) g1 g2)
+compNat (NatTr t1) (NatTr t2) = NatTr t3 where
+    t3 :: forall (a :: o1). Object c1 a => Tagged a (c3 (FMap f1 (FMap f2 a :: o2) :: o3) (FMap g1 (FMap g2 a :: o2) :: o3))
+    t3 = Tagged (m1 . m2) where
+        m2 = proxy morphMap (Proxy :: Proxy f1) (proxy t2 (Proxy :: Proxy a))
+        m1 = proxy t1 (Proxy :: Proxy (FMap g2 a)) \\ proxy objectMap (Proxy :: Proxy '(g2, a))
+
+instance Category c => Monoidal (NatTr c c) where
+    type Mu (NatTr c c) = CompFF c c c
+    type I (NatTr c c) = IdentityF c
diff --git a/Product.hs b/Product.hs
new file mode 100644
--- /dev/null
+++ b/Product.hs
@@ -0,0 +1,72 @@
+module Product where
+
+import qualified Prelude as P
+import Data.Constraint hiding ((***), (&&&))
+import Data.Proxy
+import Data.Tagged
+
+import Category
+import Category.Product
+import Functor
+import Terminal
+import TerminalMorphism
+import Monoidal
+
+class Category c => ProductCategory (c :: k -> k -> *) where
+    type (><) (a :: k) (b :: k) :: k
+    productObjectMap :: Tagged '(c, a, b) ((Object c a, Object c b) :- Object c (a >< b))
+    univProduct :: forall (a :: k) (b :: k). Tagged '(c, a, b) ((Object c a, Object c b) :- TerminalMorphism (Diag c) (a >< b) '(a, b))
+
+proj1 :: forall a b c. (ProductCategory c, Object c a, Object c b) => Tagged b (c (a >< b) a)
+proj1 = Tagged p where
+    p :><: _ = t
+    t :: (c :><: c) '(a >< b, a >< b) '(a, b)
+    t = proxy terminalMorphism (Proxy :: Proxy '(Diag c, a >< b)) \\ proxy univProduct (Proxy :: Proxy '(c, a, b))
+
+proj2 :: forall a b c. (ProductCategory c, Object c a, Object c b) => Tagged a (c (a >< b) b)
+proj2 = Tagged p where
+    _ :><: p = t
+    t :: (c :><: c) '(a >< b, a >< b) '(a, b)
+    t = proxy terminalMorphism (Proxy :: Proxy '(Diag c, a >< b)) \\ proxy univProduct (Proxy :: Proxy '(c, a, b))
+
+(&&&) :: forall c a b1 b2. ProductCategory c => c a b1 -> c a b2 -> c a (b1 >< b2)
+f &&& g
+    | Dict <- observeObjects f, Dict <- observeObjects g
+        = proxy terminalFactorization (Proxy :: Proxy (Diag c)) (f :><: g) \\ proxy univProduct (Proxy :: Proxy '(c, b1, b2))
+
+(***) :: forall c a1 a2 b1 b2. ProductCategory c => c a1 b1 -> c a2 b2 -> c (a1 >< a2) (b1 >< b2)
+f *** g = proxy morphMap (Proxy :: Proxy (ProductF c)) (f :><: g)
+
+data ProductF c where ProductF :: ProductCategory c => ProductF c
+
+instance ProductCategory (c :: k -> k -> *) => Functor (ProductF c) ('KProxy :: KProxy ((k, k) -> k)) where
+    type Domain (ProductF c) = c :><: c
+    type Codomain (ProductF c) = c
+    type FMap (ProductF c) (a :: (k, k)) = L a >< R a
+    morphMap :: forall (a :: (k, k)) (b :: (k, k)). Tagged (ProductF c)
+        (Domain (ProductF c) a b -> Codomain (ProductF c) (FMap (ProductF c) a :: k) (FMap (ProductF c) b :: k))
+    morphMap = Tagged m where
+        m (f :><: g)
+            | Dict <- observeObjects f, Dict <- observeObjects g = (f . (proxy proj1 (Proxy :: Proxy (R a)))) &&& (g . (proxy proj2 (Proxy :: Proxy (L a))))
+
+instance (ProductCategory c, Terminal c) => Monoidal c where
+    type Mu c = ProductF c
+    type I c = T c
+
+instance TerminalMorphism (Diag (->)) (a, b) '(a, b) where
+    terminalMorphism = Tagged (P.fst :><: P.snd)
+    terminalFactorization  = Tagged (\(f :><: g) z -> (f z, g z))
+
+instance ProductCategory (->) where
+    type (><) a b = (a, b)
+    productObjectMap = Tagged (Sub Dict)
+    univProduct = Tagged (Sub Dict)
+
+instance TerminalMorphism (Diag (:-)) ((a :: Constraint), b) '(a, b) where
+    terminalMorphism = Tagged (Sub Dict :><: Sub Dict)
+    terminalFactorization = Tagged (\(f :><: g) -> Sub (Dict \\ f \\ g))
+
+instance ProductCategory (:-) where
+    type (><) a b = ((a, b) :: Constraint)
+    productObjectMap = Tagged (Sub Dict)
+    univProduct = Tagged (Sub Dict)
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/Terminal.hs b/Terminal.hs
new file mode 100644
--- /dev/null
+++ b/Terminal.hs
@@ -0,0 +1,11 @@
+module Terminal where
+
+import Category
+
+class (Category c, Object c (T c)) => Terminal c where
+    type T c
+    term :: Object c a => c a (T c)
+
+instance Terminal (->) where
+    type T (->) = ()
+    term _ = ()
diff --git a/TerminalMorphism.hs b/TerminalMorphism.hs
new file mode 100644
--- /dev/null
+++ b/TerminalMorphism.hs
@@ -0,0 +1,12 @@
+module TerminalMorphism where
+
+import Data.Tagged
+import Data.Proxy
+
+import Category
+import Functor
+
+class (Functor f ('KProxy :: KProxy (o1 -> o2)), Object (Domain f) a, Object (Codomain f) x) =>
+        TerminalMorphism f (a :: o1) (x :: o2) where
+    terminalMorphism :: Tagged '(f, a) (Codomain f (FMap f a) x)
+    terminalFactorization :: Object (Domain f) y => Tagged f (Codomain f (FMap f y) x -> Domain f y a)
diff --git a/extended-categories.cabal b/extended-categories.cabal
new file mode 100644
--- /dev/null
+++ b/extended-categories.cabal
@@ -0,0 +1,32 @@
+name:                extended-categories
+version:             0.1.0
+synopsis:       Extended Categories
+description:    An implementation of category theory which makes use of GHC's enriched kind system.
+homepage:            github.com/ian-mi/extended-categories
+license:             BSD3
+license-file:        LICENSE
+author:              Ian Milligan
+maintainer:          ianmllgn@gmail.com
+-- copyright:           
+category:            Math
+build-type:          Simple
+-- extra-source-files:  
+cabal-version:       >=1.10
+stability: experimental
+
+source-repository head
+        type: git
+        location: git@github.com:ian-mi/extended-categories.git
+
+source-repository this
+        type: git
+        location: git@github.com:ian-mi/extended-categories.git
+        tag: 0.1.0
+
+library
+  exposed-modules:     Category, Category.Product, Functor, Product, Terminal, TerminalMorphism, NaturalTransformation, Monoidal
+  -- other-modules:       
+  default-extensions:    PolyKinds, DataKinds, TypeFamilies, ConstraintKinds, InstanceSigs, ScopedTypeVariables, MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts, FlexibleInstances, UndecidableInstances, TypeOperators, GADTs, NoImplicitPrelude, RankNTypes
+  build-depends:       base >=4.7 && <4.8, constraints >=0.3 && <0.5, tagged >=0.7 && <0.8, ghc-prim >=0.3 && <0.4
+  -- hs-source-dirs:      
+  default-language:    Haskell2010