diff --git a/Adjoint.hs b/Adjoint.hs
new file mode 100644
--- /dev/null
+++ b/Adjoint.hs
@@ -0,0 +1,47 @@
+module Adjoint where
+
+import Data.Constraint
+import Data.Proxy
+import Data.Tagged
+
+import Category
+import Category.Product
+import Functor
+import Functor.Product
+import NatTr
+
+class (FunctorOf f c1 c2, FunctorOf g c2 c1) => Adjoint (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) f g | f -> c1, f -> c2, g -> c1, g -> c2 where
+    leftAdjunct :: NatTr (Op c1 :><: c2) (->)
+        (Comp ('KProxy :: KProxy (o2, o2)) (Hom c2) (Dual f :***: IdentityF c2))
+        (Comp ('KProxy :: KProxy (o1, o1)) (Hom c1) (IdentityF (Op c1) :***: g))
+    rightAdjunct :: NatTr (Op c1 :><: c2) (->)
+        (Comp ('KProxy :: KProxy (o1, o1)) (Hom c1) (IdentityF (Op c1) :***: g))
+        (Comp ('KProxy :: KProxy (o2, o2)) (Hom c2) (Dual f :***: IdentityF c2))
+
+phiL :: forall (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) f g (x :: o1) (w :: o2).
+    (Adjoint c1 c2 f g, Object c1 x) => Tagged '(f, g) (c2 (FMap f x) w -> c1 x (FMap g w))
+phiL = Tagged f where
+    f m | Dict <- observeObjects m = proxy morphMap (Proxy :: Proxy (AppNat '(x, w) (Op c1 :><: c2) (->))) adj m
+    adj :: NatTr (Op c1 :><: c2) (->)
+        (Comp ('KProxy :: KProxy (o2, o2)) (Hom c2) (Dual f :***: IdentityF c2))
+        (Comp ('KProxy :: KProxy (o1, o1)) (Hom c1) (IdentityF (Op c1) :***: g))
+    adj = leftAdjunct
+
+phiR :: forall (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) f g (x :: o1) (w :: o2).
+    (Adjoint c1 c2 f g, Object c2 w) => Tagged '(f, g) (c1 x (FMap g w) -> c2 (FMap f x) w)
+phiR = Tagged f where
+    f m | Dict <- observeObjects m = proxy morphMap (Proxy :: Proxy (AppNat '(x, w) (Op c1 :><: c2) (->))) adj m
+    adj :: NatTr (Op c1 :><: c2) (->)
+        (Comp ('KProxy :: KProxy (o1, o1)) (Hom c1) (IdentityF (Op c1) :***: g))
+        (Comp ('KProxy :: KProxy (o2, o2)) (Hom c2) (Dual f :***: IdentityF c2))
+    adj = rightAdjunct
+
+unit :: forall c1 (c2 :: o2 -> o2 -> *) f g. Adjoint c1 c2 f g => NatTr c1 c1 (IdentityF c1) (Comp ('KProxy :: KProxy o2) g f)
+unit = NatTr t where
+    t :: forall x. Object c1 x => Tagged x (c1 x (FMap g (FMap f x :: o2)))
+    t = Tagged (proxy phiL (Proxy :: Proxy '(f, g)) (id :: c2 (FMap f x) (FMap f x))) \\ proxy objectMap (Proxy :: Proxy '(f, x))
+
+counit :: forall (c1 :: o1 -> o1 -> *) c2 f g. Adjoint c1 c2 f g => NatTr c2 c2 (Comp ('KProxy :: KProxy o1) f g) (IdentityF c2)
+counit = NatTr t where
+    t :: forall y. Object c2 y => Tagged y (c2 (FMap f (FMap g y :: o1)) y)
+    t = Tagged (proxy phiR (Proxy :: Proxy '(f, g)) (id :: c1 (FMap g y) (FMap g y))) \\ proxy objectMap (Proxy :: Proxy '(g, y))
diff --git a/Category.hs b/Category.hs
--- a/Category.hs
+++ b/Category.hs
@@ -30,3 +30,12 @@
     id = refl
     observeObjects = P.const Dict
     (.) = trans
+
+-- |Dual categories
+newtype Op c a b = Op {unOp :: c b a}
+
+instance Category c => Category (Op c) where
+    id = Op id
+    (Op f) . (Op g) = Op (g . f)
+    type Object (Op c) a = Object c a
+    observeObjects (Op c) = case observeObjects c of Dict -> Dict
diff --git a/Category/Product.hs b/Category/Product.hs
--- a/Category/Product.hs
+++ b/Category/Product.hs
@@ -1,11 +1,8 @@
 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
@@ -19,11 +16,3 @@
     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/Coproduct.hs b/Coproduct.hs
new file mode 100644
--- /dev/null
+++ b/Coproduct.hs
@@ -0,0 +1,38 @@
+module Coproduct where
+
+import qualified Prelude as P
+import Data.Constraint
+import Data.Tagged
+import Data.Proxy
+
+import Adjoint
+import Category
+import Category.Product
+import Functor
+import Functor.Product
+import NatTr
+
+data CoproductF (c :: o -> o -> *) where CoproductF :: CoproductCategory c => CoproductF c
+class Adjoint (c :><: c) c (CoproductF c) (Diag c) => CoproductCategory c
+type Coproduct c a b = FMap (CoproductF c) '(a, b)
+
+inj1 :: CoproductCategory c => NatTr (c :><: c) c (Proj1 c c) (CoproductF c)
+inj1 = idL . compFR retractProj1 . assocL .  compFL unit . idRInv
+
+inj2 :: CoproductCategory c => NatTr (c :><: c) c (Proj2 c c) (CoproductF c)
+inj2 = idL . compFR retractProj2 . assocL .  compFL unit . idRInv
+
+coproduct :: forall c x y z. CoproductCategory c => c x z -> c y z -> c (Coproduct c x y) z
+coproduct f g | Dict <- observeObjects g = proxy phiR (Proxy :: Proxy '(CoproductF c, Diag c)) (f :><: g)
+
+instance Functor (CoproductF (->)) ('KProxy :: KProxy ((*, *) -> *)) where
+    type Domain (CoproductF (->)) = (->) :><: (->)
+    type Codomain (CoproductF (->)) = (->)
+    type FMap (CoproductF (->)) '(a, b) = P.Either a b
+    morphMap = (Tagged (\(f :><: g) -> coproduct (appNat inj1 . f) (appNat inj2 . g)))
+
+instance Adjoint ((->) :><: (->)) (->) (CoproductF (->)) (Diag (->)) where
+    leftAdjunct = NatTr (Tagged (\f -> (f . P.Left) :><: (f . P.Right)))
+    rightAdjunct = NatTr (Tagged (\(f :><: g) -> P.either f g))
+
+instance CoproductCategory (->)
diff --git a/Functor.hs b/Functor.hs
--- a/Functor.hs
+++ b/Functor.hs
@@ -6,6 +6,7 @@
 import Data.Tagged
 
 import Category
+import Category.Product
 
 -- |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
@@ -30,11 +31,19 @@
 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)
 
+type EndoFunctor f = (Functor f ('KProxy :: KProxy (k -> k)), (Domain f :: k -> k -> *) ~ Codomain f)
+
+type EndoFunctorOf f (c :: k -> k -> *) = (Functor f ('KProxy :: KProxy (k -> k)), Domain f ~ c, Codomain f ~ c)
+
+type FunctorOf f (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) = (Functor f ('KProxy :: KProxy (o1 -> o2)), Domain f ~ c1, Codomain f ~ c2)
+
 -- |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
 
+type f :.: g = Comp ('KProxy :: KProxy *) 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)
@@ -45,18 +54,35 @@
 -- |The identity functor.
 data IdentityF c where IdentityF :: Category c => IdentityF c
 
+type Id = IdentityF (->)
+
 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
+data Dual 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) = (->)
+instance Functor f ('KProxy :: KProxy (o1 -> o2)) => Functor (Dual f) ('KProxy :: KProxy (o1 -> o2)) where
+    type Domain (Dual f) = Op (Domain f)
+    type Codomain (Dual f) = Op (Codomain f)
+    type FMap (Dual f) a = FMap f a
+    morphMap = Tagged (\(Op f) -> Op (proxy morphMap (Proxy :: Proxy f) f))
+
+data Hom c
+
+instance Category c => Functor (Hom (c :: o -> o -> *)) ('KProxy :: KProxy ((o, o) -> *)) where
+    type Domain (Hom c) = Op c :><: c
+    type Codomain (Hom c) = (->)
+    type FMap (Hom c) '(a, b) = c a b
+    morphMap = Tagged (\(Op f :><: g) h -> g . h . f)
+
+-- |Functors from Prelude.Functor
+data Ftag f where Ftag :: P.Functor f => Ftag f
+
+instance P.Functor f => Functor (Ftag f) ('KProxy :: KProxy (* -> *)) where
+    type Domain (Ftag f) = (->)
+    type Codomain (Ftag f) = (->)
+    type FMap (Ftag f) a = f a
     morphMap = Tagged P.fmap
diff --git a/Monad.hs b/Monad.hs
new file mode 100644
--- /dev/null
+++ b/Monad.hs
@@ -0,0 +1,35 @@
+module Monad where
+
+import qualified Prelude as P
+import Data.Constraint
+import Data.Proxy
+import Data.Tagged
+
+import Category
+import Functor
+import NatTr
+
+class EndoFunctorOf t c => Monad t (c :: o -> o -> *) | t -> c where
+    nu :: NatTr c c (IdentityF c) t
+    mu :: NatTr c c (Comp ('KProxy :: KProxy o) t t) t
+
+data MonadMorph c t s where MonadMorph :: (Monad t c, Monad s c) => NatTr c c t s -> MonadMorph c t s
+
+instance Category c => Category (MonadMorph c) where
+    type Object (MonadMorph c) t = Monad t c
+    id = MonadMorph id
+    MonadMorph f . MonadMorph g = MonadMorph (f . g)
+    observeObjects (MonadMorph _) = Dict
+
+data ForgetM c where
+    ForgetM :: Category c => ForgetM c
+
+instance Category c => Functor (ForgetM c) ('KProxy :: KProxy (* -> *)) where
+    type Domain (ForgetM c) = MonadMorph c
+    type Codomain (ForgetM c) = NatTr c c
+    type FMap (ForgetM c) (t :: *) = t
+    morphMap = Tagged (\(MonadMorph t) -> t)
+
+instance (P.Functor m, P.Monad m) => Monad (Ftag m) (->) where
+    nu = NatTr (Tagged P.return)
+    mu = NatTr (Tagged (P.>>= id))
diff --git a/Monad/Free.hs b/Monad/Free.hs
new file mode 100644
--- /dev/null
+++ b/Monad/Free.hs
@@ -0,0 +1,50 @@
+module Monad.Free where
+
+import qualified Prelude as P
+import Data.Constraint
+import Data.Proxy
+import Data.Tagged
+
+import Category
+import Functor
+import Coproduct
+import Monad
+import NatTr
+import NatTr.Coproduct
+
+data Free f a where
+    Free :: FMap f (Free f a) -> Free f a
+    Pure :: EndoFunctorOf f (->) => a -> Free f a
+
+freeT :: EndoFunctorOf f (->) => NatTr (->) (->) (f :.: Ftag (Free f)) (Ftag (Free f))
+freeT = NatTr (Tagged Free)
+
+pureT :: EndoFunctorOf f (->) => NatTr (->) (->) Id (Ftag (Free f))
+pureT = NatTr (Tagged Pure)
+
+unfreeT :: forall f. EndoFunctorOf f (->) => NatTr (->) (->) (Ftag (Free f)) ((f :.: Ftag (Free f)) :+: Id)
+unfreeT = NatTr (Tagged t) where
+    t :: forall a. Free f a -> FMap ((f :.: Ftag (Free f)) :+: Id) a
+    t (Free f) = appNat inj1 f
+    t (Pure a) = appNat inj2 a
+
+instance EndoFunctorOf f (->) => P.Functor (Free f) where
+    fmap t = go where
+        go (Free f) = Free (proxy morphMap (Proxy :: Proxy f) go f)
+        go (Pure a) = Pure (t a)
+
+instance EndoFunctorOf f (->) => P.Monad (Free f) where
+    f >>= t = go f where
+        go (Free x) = Free (proxy morphMap (Proxy :: Proxy f) go x)
+        go (Pure a) = t a
+    return = Pure
+
+data FreeM = FreeM
+
+instance Functor FreeM ('KProxy :: KProxy (* -> *)) where
+    type Domain FreeM = NatTr (->) (->)
+    type Codomain FreeM = MonadMorph (->)
+    type FMap FreeM f = Ftag (Free f)
+    morphMap = Tagged (\t -> case observeObjects t of Dict -> f t) where
+        f t = MonadMorph go where
+            go = coproduct (freeT . compNat t go) pureT . unfreeT
diff --git a/Monoidal.hs b/Monoidal.hs
--- a/Monoidal.hs
+++ b/Monoidal.hs
@@ -7,10 +7,9 @@
 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
+class (Category c, FunctorOf mu (c :><: c) c) => Monoidal (c :: o -> o -> *) mu | mu -> c where
+    type I mu :: o
 
-(<>) :: 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)
+(<>) :: forall (c :: o -> o -> *) mu a1 a2 b1 b2. Monoidal c mu => c a1 b1 -> c a2 b2 -> Tagged mu (c (FMap mu '(a1, a2)) (FMap mu '(b1, b2)))
+f <> g = Tagged (proxy morphMap (Proxy :: Proxy mu) (f :><: g))
+
diff --git a/NatTr.hs b/NatTr.hs
new file mode 100644
--- /dev/null
+++ b/NatTr.hs
@@ -0,0 +1,124 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+module NatTr where
+
+import Data.Constraint hiding ((&&&))
+import Data.Tagged
+import Data.Proxy
+
+import Category
+import Category.Product
+import Functor
+
+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
+
+appNat :: forall c1 c2 f g a. Object c1 a => NatTr c1 c2 f g -> c2 (FMap f a) (FMap g a)
+appNat (NatTr t) = proxy t (Proxy :: Proxy a)
+
+instance (Category c1, Category c2) => Category (NatTr (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *)) where
+    type Object (NatTr c1 c2) f = FunctorOf f c1 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))
+
+(<.>) :: (Functor f ('KProxy :: KProxy (o3 -> o4)), Functor g ('KProxy :: KProxy (o1 -> o2))) =>
+    f -> g -> NatTr (Codomain g :: o2 -> o2 -> *) (Domain f :: o3 -> o3 -> *) h1 h2 ->
+    NatTr (Domain g :: o1 -> o1 -> *) (Codomain f :: o4 -> o4 -> *)
+        (Comp ('KProxy :: KProxy o3) f (Comp ('KProxy :: KProxy o2) h1 g))
+        (Comp ('KProxy :: KProxy o3) f (Comp ('KProxy :: KProxy o2) h2 g))
+f <.> g = compFL . compFR
+
+compFL :: forall c1 c2 f h g. (Category c1, Functor h ('KProxy :: KProxy (o2 -> o3)), Domain h ~ c2) =>
+    NatTr c1 (c2 :: o2 -> o2 -> *) f g -> NatTr c1 (Codomain h :: o3 -> o3 -> *) (Comp ('KProxy :: KProxy o2) h f) (Comp ('KProxy :: KProxy o2) h g)
+compFL t | Dict <- observeObjects t = NatTr t' where
+    t' :: forall a. Object c1 a => Tagged a (Codomain h (FMap h (FMap f a :: o2) :: o3) (FMap h (FMap g a :: o2)))
+    t' = Tagged (proxy morphMap (Proxy :: Proxy (Comp ('KProxy :: KProxy o2) h (AppNat a c1 c2))) t)
+
+compFR :: forall c2 c3 f h g. (Category c3, Functor h ('KProxy :: KProxy (o1 -> o2)), Codomain h ~ c2) =>
+    NatTr (c2 :: o2 -> o2 -> *) c3 f g -> NatTr (Domain h :: o1 -> o1 -> *) c3 (Comp ('KProxy :: KProxy o2) f h) (Comp ('KProxy :: KProxy o2) g h)
+compFR t | Dict <- observeObjects t = NatTr t' where
+    t' :: forall (a :: o1). Object (Domain h) a => Tagged a (c3 (FMap f (FMap h a :: o2)) (FMap g (FMap h a :: o2)))
+    t' = Tagged (proxy morphMap (Proxy :: Proxy (AppNat (FMap h a) c2 c3)) t \\ proxy objectMap (Proxy :: Proxy '(h, a)))
+
+data AppNat a c1 c2 where AppNat :: (Category c1, Category c2, Object c1 a) => AppNat a c1 c2
+
+instance (Category c1, Category c2, Object c1 a) => Functor (AppNat (a :: o1) (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *)) ('KProxy :: KProxy (* -> o2)) where
+    type Domain (AppNat a c1 c2) = NatTr c1 c2
+    type Codomain (AppNat a c1 c2) = c2
+    type FMap (AppNat a c1 c2) f = (FMap f a :: o2)
+    morphMap = Tagged (\(NatTr t) -> proxy t (Proxy :: Proxy a))
+
+idL :: forall f. Functor f ('KProxy :: KProxy (o1 -> o2)) =>
+    NatTr (Domain f :: o1 -> o1 -> *) (Codomain f :: o2 -> o2 -> *) (Comp ('KProxy :: KProxy o2) (IdentityF (Codomain f :: o2 -> o2 -> *)) f) f
+idL = NatTr t where
+    t :: forall (a :: o1). Object (Domain f) a => Tagged a (Codomain f (FMap f a :: o2) (FMap f a :: o2))
+    t = Tagged (id \\ proxy objectMap (Proxy :: Proxy '(f, a)))
+
+idLInv :: forall f. Functor f ('KProxy :: KProxy (o1 -> o2)) =>
+    NatTr (Domain f :: o1 -> o1 -> *) (Codomain f :: o2 -> o2 -> *) f (Comp ('KProxy :: KProxy o2) (IdentityF (Codomain f :: o2 -> o2 -> *)) f)
+idLInv = NatTr t where
+    t :: forall (a :: o1). Object (Domain f) a => Tagged a (Codomain f (FMap f a :: o2) (FMap f a :: o2))
+    t = Tagged (id \\ proxy objectMap (Proxy :: Proxy '(f, a)))
+
+idR :: forall f. Functor f ('KProxy :: KProxy (o1 -> o2)) =>
+    NatTr (Domain f :: o1 -> o1 -> *) (Codomain f :: o2 -> o2 -> *) (Comp ('KProxy :: KProxy o1) f (IdentityF (Domain f :: o1 -> o1 -> *))) f
+idR = NatTr t where
+    t :: forall (a :: o1). Object (Domain f) a => Tagged a (Codomain f (FMap f a :: o2) (FMap f a :: o2))
+    t = Tagged (id \\ proxy objectMap (Proxy :: Proxy '(f, a)))
+
+idRInv :: forall f. Functor f ('KProxy :: KProxy (o1 -> o2)) =>
+    NatTr (Domain f :: o1 -> o1 -> *) (Codomain f :: o2 -> o2 -> *) f (Comp ('KProxy :: KProxy o1) f (IdentityF (Domain f :: o1 -> o1 -> *)))
+idRInv = NatTr t where
+    t :: forall (a :: o1). Object (Domain f) a => Tagged a (Codomain f (FMap f a :: o2) (FMap f a :: o2))
+    t = Tagged (id \\ proxy objectMap (Proxy :: Proxy '(f, a)))
+
+assocL :: forall f g h.
+    (Functor f ('KProxy :: KProxy (o3 -> o4)), Functor g ('KProxy :: KProxy (o2 -> o3)), Functor h ('KProxy :: KProxy (o1 -> o2)),
+    (Domain f :: o3 -> o3 -> *) ~ Codomain g, (Domain g :: o2 -> o2 -> *) ~ Codomain h) =>
+        NatTr (Domain h :: o1 -> o1 -> *) (Codomain f :: o4 -> o4 -> *)
+            (Comp ('KProxy :: KProxy o3) f (Comp ('KProxy :: KProxy o2) g h))
+            (Comp ('KProxy :: KProxy o2) (Comp ('KProxy :: KProxy o3) f g) h)
+assocL = NatTr t where
+    t :: forall (a :: o1). Object (Domain h) a => Tagged a (Codomain f (FMap f (FMap g (FMap h a :: o2) :: o3) :: o4) (FMap f (FMap g (FMap h a :: o2) :: o3) :: o4))
+    t = Tagged (id \\
+                    proxy objectMap (Proxy :: Proxy '(f, (FMap g (FMap h a :: o2) :: o3))) .
+                    proxy objectMap (Proxy :: Proxy '(g, (FMap h a :: o2))) .
+                    proxy objectMap (Proxy :: Proxy '(h, a)))
+
+assocR :: forall f g h.
+    (Functor f ('KProxy :: KProxy (o3 -> o4)), Functor g ('KProxy :: KProxy (o2 -> o3)), Functor h ('KProxy :: KProxy (o1 -> o2)),
+    (Domain f :: o3 -> o3 -> *) ~ Codomain g, (Domain g :: o2 -> o2 -> *) ~ Codomain h) =>
+        NatTr (Domain h :: o1 -> o1 -> *) (Codomain f :: o4 -> o4 -> *)
+            (Comp ('KProxy :: KProxy o2) (Comp ('KProxy :: KProxy o3) f g) h)
+            (Comp ('KProxy :: KProxy o3) f (Comp ('KProxy :: KProxy o2) g h))
+assocR = NatTr t where
+    t :: forall (a :: o1). Object (Domain h) a => Tagged a (Codomain f (FMap f (FMap g (FMap h a :: o2) :: o3) :: o4) (FMap f (FMap g (FMap h a :: o2) :: o3) :: o4))
+    t = Tagged (id \\
+                    proxy objectMap (Proxy :: Proxy '(f, (FMap g (FMap h a :: o2) :: o3))) .
+                    proxy objectMap (Proxy :: Proxy '(g, (FMap h a :: o2))) .
+                    proxy objectMap (Proxy :: Proxy '(h, a)))
diff --git a/NatTr/Coproduct.hs b/NatTr/Coproduct.hs
new file mode 100644
--- /dev/null
+++ b/NatTr/Coproduct.hs
@@ -0,0 +1,29 @@
+module NatTr.Coproduct where
+
+import Data.Constraint hiding ((&&&))
+import Data.Tagged
+import Data.Proxy
+
+import Adjoint
+import Category
+import Category.Product
+import Functor
+import Functor.Product
+import Product
+import Coproduct
+import NatTr
+
+instance (Category c1, CoproductCategory c2) => Functor (CoproductF (NatTr c1 (c2 :: o2 -> o2 -> *))) ('KProxy :: KProxy ((*, *) -> *)) where
+    type Domain (CoproductF (NatTr c1 c2)) = NatTr c1 c2 :><: NatTr c1 c2
+    type Codomain (CoproductF (NatTr c1 c2)) = NatTr c1 c2
+    type FMap (CoproductF (NatTr c1 c2)) '((f :: *), (g :: *)) = Comp ('KProxy :: KProxy (o2, o2)) (CoproductF c2) (f :&&&: g)
+    morphMap = (Tagged (\t@(f :><: g) -> case observeObjects t of Dict -> coproduct (appNat inj1 . f) (appNat inj2 . g)))
+
+instance (Category c1, CoproductCategory c2) =>
+    Adjoint (NatTr c1 c2 :><: NatTr c1 c2) (NatTr (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *)) (CoproductF (NatTr c1 c2)) (Diag (NatTr c1 c2)) where
+    leftAdjunct = NatTr (Tagged (\t -> (t . compFR inj1 . proj1FInv) :><: (t . compFR inj2 . proj2FInv)))
+    rightAdjunct = NatTr (Tagged (\(t1 :><: t2) -> idL . compFR counit . assocL . compFL (diagInv . productNat t1 t2)))
+
+instance (Category c1, CoproductCategory c2) => CoproductCategory (NatTr c1 c2)
+
+type f :+: g = Coproduct (NatTr (->) (->)) f g
diff --git a/NatTr/Product.hs b/NatTr/Product.hs
new file mode 100644
--- /dev/null
+++ b/NatTr/Product.hs
@@ -0,0 +1,29 @@
+module NatTr.Product where
+
+import qualified Prelude as P
+import Data.Constraint hiding ((&&&))
+import Data.Tagged
+import Data.Proxy
+
+import Category
+import Category.Product
+import Functor
+import Functor.Product
+import Product
+import NatTr
+import Adjoint
+
+instance (Category c1, ProductCategory c2) => Functor (ProductF (NatTr c1 (c2 :: o2 -> o2 -> *))) ('KProxy :: KProxy ((*, *) -> *)) where
+    type Domain (ProductF (NatTr c1 c2)) = NatTr c1 c2 :><: NatTr c1 c2
+    type Codomain (ProductF (NatTr c1 c2)) = NatTr c1 c2
+    type FMap (ProductF (NatTr c1 c2)) '((f :: *), (g :: *)) = Comp ('KProxy :: KProxy (o2, o2)) (ProductF c2) (f :&&&: g)
+    morphMap = Tagged (\t@(f :><: g) -> case observeObjects t of Dict -> (f . appNat proj1) &&& (g . appNat proj2))
+
+instance (Category c1, ProductCategory c2) =>
+        Adjoint (NatTr c1 c2) (NatTr (c1 :: o1 -> o1 -> *) (c2 :: o2 -> o2 -> *) :><: NatTr c1 c2) (Diag (NatTr c1 c2)) (ProductF (NatTr c1 c2)) where
+    leftAdjunct = NatTr (Tagged (\(s :><: t) -> compFL (productNat s t . diag) . assocR . compFR unit . idLInv))
+    rightAdjunct = NatTr (Tagged (\t -> (proj1F . compFR proj1 . t) :><: (proj2F . compFR proj2 . t)))
+
+instance (Category c1, ProductCategory c2) => ProductCategory (NatTr c1 c2)
+
+type f :*: g = Product (NatTr (->) (->)) f g
diff --git a/NaturalTransformation.hs b/NaturalTransformation.hs
deleted file mode 100644
--- a/NaturalTransformation.hs
+++ /dev/null
@@ -1,47 +0,0 @@
-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
--- a/Product.hs
+++ b/Product.hs
@@ -8,65 +8,52 @@
 import Category
 import Category.Product
 import Functor
+import Functor.Product
+import NatTr
+import Adjoint
 import Terminal
-import TerminalMorphism
+import Universal
 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))
+data ProductF (c :: o -> o -> *) where ProductF :: ProductCategory c => ProductF c
+class Adjoint c (c :><: c) (Diag c) (ProductF c) => ProductCategory c
+type Product c a b = FMap (ProductF c) '(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))
+proj1 :: forall (c :: o -> o -> *). ProductCategory c => NatTr (c :><: c) c (ProductF c) (Proj1 c c)
+proj1 = idR . compFL counit . assocR . compFR retractProj1Inv . idLInv
 
-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))
+proj2 :: forall (c :: o -> o -> *). ProductCategory c => NatTr (c :><: c) c (ProductF c) (Proj2 c c)
+proj2 = idR . compFL counit . assocR . compFR retractProj2Inv . idLInv
 
-(&&&) :: 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 a b1 b2. ProductCategory c => c a b1 -> c a b2 -> c a (Product c b1 b2)
+f &&& g | Dict <- observeObjects f = proxy phiL (Proxy :: Proxy '(Diag c, ProductF c)) (f :><: g)
 
-(***) :: forall c a1 a2 b1 b2. ProductCategory c => c a1 b1 -> c a2 b2 -> c (a1 >< a2) (b1 >< b2)
+(***) :: forall c a1 a2 b1 b2. ProductCategory c => c a1 b1 -> c a2 b2 -> c (Product c a1 a2) (Product c b1 b2)
 f *** g = proxy morphMap (Proxy :: Proxy (ProductF c)) (f :><: g)
 
-data ProductF c where ProductF :: ProductCategory c => ProductF c
+instance (ProductCategory c, Terminal c) => Monoidal c (ProductF c) where
+    type I (ProductF c) = T 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 Functor (ProductF (->)) ('KProxy :: KProxy ((*,*) -> *)) where
+    type Domain (ProductF (->)) = (->) :><: (->)
+    type Codomain (ProductF (->)) = (->)
+    type FMap (ProductF (->)) '(a, b) = (a, b)
+    morphMap = Tagged (\(f :><: g) -> (f . appNat proj1) &&& (g . appNat proj2))
 
-instance (ProductCategory c, Terminal c) => Monoidal c where
-    type Mu c = ProductF c
-    type I c = T c
+instance Adjoint (->) ((->) :><: (->)) (Diag (->)) (ProductF (->)) where
+    leftAdjunct = NatTr (Tagged (\(f :><: g) z -> (f z, g z)))
+    rightAdjunct = NatTr (Tagged (\f -> (P.fst . f) :><: (P.snd . f)))
 
-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 (->)
 
-instance ProductCategory (->) where
-    type (><) a b = (a, b)
-    productObjectMap = Tagged (Sub Dict)
-    univProduct = Tagged (Sub Dict)
+instance Functor (ProductF (:-)) ('KProxy :: KProxy ((Constraint, Constraint) -> Constraint)) where
+    type Domain (ProductF (:-)) = (:-) :><: (:-)
+    type Codomain (ProductF (:-)) = (:-)
+    type FMap (ProductF (:-)) '((a :: Constraint), (b :: Constraint)) = ((a, b) :: Constraint)
+    morphMap = Tagged (\(f :><: g) -> (f . appNat proj1) &&& (g . appNat proj2))
 
-instance TerminalMorphism (Diag (:-)) ((a :: Constraint), b) '(a, b) where
-    terminalMorphism = Tagged (Sub Dict :><: Sub Dict)
-    terminalFactorization = Tagged (\(f :><: g) -> Sub (Dict \\ f \\ g))
+instance Adjoint (:-) ((:-) :><: (:-)) (Diag (:-)) (ProductF (:-)) where
+    leftAdjunct = NatTr (Tagged (\(f :><: g) -> Sub (Dict \\ f \\ g)))
+    rightAdjunct = NatTr (Tagged (\f -> (Sub (Dict \\ f) :><: Sub (Dict \\ f))))
 
-instance ProductCategory (:-) where
-    type (><) a b = ((a, b) :: Constraint)
-    productObjectMap = Tagged (Sub Dict)
-    univProduct = Tagged (Sub Dict)
+instance ProductCategory (:-)
diff --git a/TerminalMorphism.hs b/TerminalMorphism.hs
deleted file mode 100644
--- a/TerminalMorphism.hs
+++ /dev/null
@@ -1,12 +0,0 @@
-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/Universal.hs b/Universal.hs
new file mode 100644
--- /dev/null
+++ b/Universal.hs
@@ -0,0 +1,17 @@
+module Universal 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) =>
+        InitialMorphism f (a :: o1) (x :: o2) where
+    initialMorphism :: Tagged '(f, a) (Codomain f x (FMap f a))
+    initialFactorization :: Object (Domain f) b => Tagged f (Codomain f x (FMap f b) -> Domain f a b)
+
+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) b => Tagged f (Codomain f (FMap f b) x -> Domain f b a)
diff --git a/extended-categories.cabal b/extended-categories.cabal
--- a/extended-categories.cabal
+++ b/extended-categories.cabal
@@ -1,5 +1,5 @@
 name:                extended-categories
-version:             0.1.0
+version:             0.2.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
@@ -21,10 +21,10 @@
 source-repository this
         type: git
         location: git@github.com:ian-mi/extended-categories.git
-        tag: 0.1.0
+        tag: 0.2.0
 
 library
-  exposed-modules:     Category, Category.Product, Functor, Product, Terminal, TerminalMorphism, NaturalTransformation, Monoidal
+  exposed-modules:     Category, Category.Product, Functor, Universal, Product, Coproduct, Terminal, NatTr, NatTr.Product, NatTr.Coproduct, Adjoint, Monoidal, Monad, Monad.Free
   -- 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