diff --git a/Data/Category/Adjunction.hs b/Data/Category/Adjunction.hs
--- a/Data/Category/Adjunction.hs
+++ b/Data/Category/Adjunction.hs
@@ -31,6 +31,8 @@
   , adjunctionTerminalProp
   
   -- * Examples
+  , precomposeAdj
+  , postcomposeAdj
   , contAdj
   
 ) where
@@ -90,8 +92,8 @@
 
 composeAdj :: Adjunction d e f g -> Adjunction c d f' g' -> Adjunction c e (f' :.: f) (g :.: g')
 composeAdj (Adjunction f g u c) (Adjunction f' g' u' c') = Adjunction (f' :.: f) (g :.: g') 
-  (compAssoc (g :.: g') f' f . Precompose f % (compAssocInv g g' f' . Postcompose g % u' . idPrecompInv g) . u)
-  (c' . Precompose g' % (idPrecomp f' . Postcompose f' % c . compAssoc f' f g) . compAssocInv (f' :.: f) g g')
+  (compAssoc (g :.: g') f' f . precompose f % (compAssocInv g g' f' . postcompose g % u' . idPrecompInv g) . u)
+  (c' . precompose g' % (idPrecomp f' . postcompose f' % c . compAssoc f' f g) . compAssocInv (f' :.: f) g g')
 
 
 data AdjArrow c d where
@@ -109,15 +111,15 @@
 
 precomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat c e) (Nat d e) (Precompose g e) (Precompose f e)
 precomposeAdj (Adjunction f g un coun) = mkAdjunction 
-  (Precompose g)
-  (Precompose f)
+  (precompose g)
+  (precompose f)
   (\nh@(Nat h _ _) -> compAssocInv h g f . (nh `o` un) . idPrecompInv h)
   (\nh@(Nat h _ _) -> idPrecomp h . (nh `o` coun) . compAssoc h f g)
 
 postcomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat e c) (Nat e d) (Postcompose f e) (Postcompose g e)
 postcomposeAdj (Adjunction f g un coun) = mkAdjunction 
-  (Postcompose f)
-  (Postcompose g)
+  (postcompose f)
+  (postcompose g)
   (\nh@(Nat h _ _) -> compAssoc g f h . (un `o` nh) . idPostcompInv h)
   (\nh@(Nat h _ _) -> idPostcomp h . (coun `o` nh) . compAssocInv f g h)
 
diff --git a/Data/Category/CartesianClosed.hs b/Data/Category/CartesianClosed.hs
--- a/Data/Category/CartesianClosed.hs
+++ b/Data/Category/CartesianClosed.hs
@@ -48,29 +48,21 @@
 
 
 
-data Apply (y :: * -> * -> *) (z :: * -> * -> *) = Apply
+data Apply (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Apply
 -- | 'Apply' is a bifunctor, @Apply :% (f, a)@ applies @f@ to @a@, i.e. @f :% a@.
-instance (Category y, Category z) => Functor (Apply y z) where
-  type Dom (Apply y z) = Nat y z :**: y
-  type Cod (Apply y z) = z
-  type Apply y z :% (f, a) = f :% a
+instance (Category c1, Category c2) => Functor (Apply c1 c2) where
+  type Dom (Apply c1 c2) = Nat c2 c1 :**: c2
+  type Cod (Apply c1 c2) = c1
+  type Apply c1 c2 :% (f, a) = f :% a
   Apply % (l :**: r) = l ! r
 
-data ToTuple1 (y :: * -> * -> *) (z :: * -> * -> *) = ToTuple1
--- | 'ToTuple1' converts an object @a@ to the functor 'Tuple1' @a@.
-instance (Category y, Category z) => Functor (ToTuple1 y z) where
-  type Dom (ToTuple1 y z) = z
-  type Cod (ToTuple1 y z) = Nat y (z :**: y)
-  type ToTuple1 y z :% a = Tuple1 z y a
-  ToTuple1 % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) (\z -> f :**: z)
-
-data ToTuple2 (y :: * -> * -> *) (z :: * -> * -> *) = ToTuple2
--- | 'ToTuple2' converts an object @a@ to the functor 'Tuple2' @a@.
-instance (Category y, Category z) => Functor (ToTuple2 y z) where
-  type Dom (ToTuple2 y z) = y
-  type Cod (ToTuple2 y z) = Nat z (z :**: y)
-  type ToTuple2 y z :% a = Tuple2 z y a
-  ToTuple2 % f = Nat (Tuple2 (src f)) (Tuple2 (tgt f)) (\y -> y :**: f)
+data Tuple (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Tuple
+-- | 'Tuple' converts an object @a@ to the functor 'Tuple1' @a@.
+instance (Category c1, Category c2) => Functor (Tuple c1 c2) where
+  type Dom (Tuple c1 c2) = c1
+  type Cod (Tuple c1 c2) = Nat c2 (c1 :**: c2)
+  type Tuple c1 c2 :% a = Tuple1 c1 c2 a
+  Tuple % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) (\z -> f :**: z)
 
 
 -- | Exponentials in @Cat@ are the functor categories.
@@ -78,7 +70,7 @@
   type Exponential Cat (CatW c) (CatW d) = CatW (Nat c d)
   
   apply CatA{} CatA{}   = CatA Apply
-  tuple CatA{} CatA{}   = CatA ToTuple1
+  tuple CatA{} CatA{}   = CatA Tuple
   (CatA f) ^^^ (CatA h) = CatA (Wrap f h)
 
 
@@ -88,7 +80,7 @@
          -> Adjunction k k
               (ProductFunctor k :.: Tuple2 k k y)
               (ExpFunctor k :.: Tuple1 (Op k) k y)
-curryAdj y = mkAdjunction (ProductFunctor :.: Tuple2 y) (ExpFunctor :.: Tuple1 (Op y)) (tuple y) (apply y)
+curryAdj y = mkAdjunction (ProductFunctor :.: tuple2 y) (ExpFunctor :.: Tuple1 (Op y)) (tuple y) (apply y)
 
 -- | From the adjunction between the product functor and the exponential functor we get the curry and uncurry functions,
 --   generalized to any cartesian closed category.
diff --git a/Data/Category/Fix.hs b/Data/Category/Fix.hs
--- a/Data/Category/Fix.hs
+++ b/Data/Category/Fix.hs
@@ -13,6 +13,7 @@
 import Data.Category
 import Data.Category.Functor
 import Data.Category.Limit
+import Data.Category.CartesianClosed
 
 import Data.Category.Unit
 import Data.Category.Coproduct
@@ -52,6 +53,13 @@
   inj2 (Fix a) (Fix b) = Fix (inj2 a b)
   Fix a ||| Fix b = Fix (a ||| b)
 
+-- | @Fix f@ inherits its exponentials from @f (Fix f)@.
+instance CartesianClosed (f (Fix f)) => CartesianClosed (Fix f) where
+  type Exponential (Fix f) a b = Exponential (f (Fix f)) a b
+  apply (Fix a) (Fix b) = Fix (apply a b)
+  tuple (Fix a) (Fix b) = Fix (tuple a b)
+  Fix a ^^^ Fix b = Fix (a ^^^ b)
+  
 data Wrap (f :: (* -> * -> *) -> * -> * -> *) = Wrap
 -- | The `Wrap` functor wraps `Fix` around @f (Fix f)@.
 instance Category (f (Fix f)) => Functor (Wrap f) where
diff --git a/Data/Category/Functor.hs b/Data/Category/Functor.hs
--- a/Data/Category/Functor.hs
+++ b/Data/Category/Functor.hs
@@ -31,7 +31,8 @@
   , (:***:)(..)
   , DiagProd(..)
   , Tuple1(..)
-  , Tuple2(..)
+  , Swap, swap
+  , Tuple2, tuple2
 
   -- *** Hom functors
   , Hom(..)
@@ -110,7 +111,7 @@
 
 
 data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where
-  Const :: Category c2 => Obj c2 x -> Const c1 c2 x
+  Const :: Obj c2 x -> Const c1 c2 x
 
 -- | The constant functor.
 instance (Category c1, Category c2) => Functor (Const c1 c2 x) where
@@ -212,18 +213,18 @@
   
   Tuple1 a % f = a :**: f
 
-
-data Tuple2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple2 (Obj c2 a)
+type Swap (c1 :: * -> * -> *) (c2 :: * -> * -> *) = (Proj2 c1 c2 :***: Proj1 c1 c2) :.: DiagProd (c1 :**: c2)
+-- | 'swap' swaps the 2 categories of the product of categories.
+swap :: (Category c1, Category c2) => Swap c1 c2
+swap = (Proj2 :***: Proj1) :.: DiagProd
 
+type Tuple2 c1 c2 a = Swap c2 c1 :.: Tuple1 c2 c1 a
 -- | 'Tuple2' tuples with a fixed object on the right.
-instance (Category c1, Category c2) => Functor (Tuple2 c1 c2 a2) where
-  type Dom (Tuple2 c1 c2 a2) = c1
-  type Cod (Tuple2 c1 c2 a2) = c1 :**: c2
-  type Tuple2 c1 c2 a2 :% a1 = (a1, a2)
-  
-  Tuple2 a % f = f :**: a
+tuple2 :: (Category c1, Category c2) => Obj c2 a -> Tuple2 c1 c2 a
+tuple2 a = swap :.: Tuple1 a
 
 
+
 data Hom (k :: * -> * -> *) = Hom
 
 -- | The Hom functor, Hom(--,--), a bifunctor contravariant in its first argument and covariant in its second argument.
@@ -243,4 +244,4 @@
 type k :-*: x = Hom k :.: Tuple2 (Op k) k x
 -- | The contravariant functor Hom(--,X)
 hom_X :: Category k => Obj k x -> k :-*: x
-hom_X x = Hom :.: Tuple2 x
+hom_X x = Hom :.: tuple2 x
diff --git a/Data/Category/Limit.hs b/Data/Category/Limit.hs
--- a/Data/Category/Limit.hs
+++ b/Data/Category/Limit.hs
@@ -56,9 +56,11 @@
   , HasBinaryProducts(..)
   , ProductFunctor(..)
   , (:*:)(..)
+  , prodAdj
   , HasBinaryCoproducts(..)
   , CoproductFunctor(..)
   , (:+:)(..)
+  , coprodAdj
   
 ) where
 
@@ -418,6 +420,10 @@
 
   ProductFunctor % (a1 :**: a2) = a1 *** a2
 
+-- | A specialisation of the limit adjunction to products.
+prodAdj :: HasBinaryProducts k => Adjunction (k :**: k) k (DiagProd k) (ProductFunctor k)
+prodAdj = mkAdjunction DiagProd ProductFunctor (\x -> x &&& x) (\(l :**: r) -> proj1 l r :**: proj2 l r)
+
 data p :*: q where
   (:*:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryProducts k) => p -> q -> p :*: q
 -- | The product of two functors, passing the same object to both functors and taking the product of the results.
@@ -438,8 +444,8 @@
   Nat a f af &&& Nat _ g ag = Nat a (f :*: g) (\z -> af z &&& ag z)
   Nat f1 f2 f *** Nat g1 g2 g = Nat (f1 :*: g1) (f2 :*: g2) (\z -> f z *** g z)
   
-  
 
+
 class Category k => HasBinaryCoproducts k where
   type BinaryCoproduct (k :: * -> * -> *) x y :: *
 
@@ -538,6 +544,10 @@
   type CoproductFunctor k :% (a, b) = BinaryCoproduct k a b
 
   CoproductFunctor % (a1 :**: a2) = a1 +++ a2
+
+-- | A specialisation of the colimit adjunction to coproducts.
+coprodAdj :: HasBinaryCoproducts k => Adjunction k (k :**: k) (CoproductFunctor k) (DiagProd k)
+coprodAdj = mkAdjunction CoproductFunctor DiagProd (\(l :**: r) -> inj1 l r :**: inj2 l r) (\x -> x ||| x)
 
 data p :+: q where
   (:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryCoproducts k) => p -> q -> p :+: q
diff --git a/Data/Category/Monoidal.hs b/Data/Category/Monoidal.hs
--- a/Data/Category/Monoidal.hs
+++ b/Data/Category/Monoidal.hs
@@ -1,4 +1,13 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ViewPatterns, NoImplicitPrelude #-}
+{-# LANGUAGE 
+    TypeOperators
+  , TypeFamilies
+  , GADTs
+  , Rank2Types
+  , ViewPatterns
+  , TypeSynonymInstances
+  , FlexibleInstances
+  , NoImplicitPrelude 
+  #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Monoidal
@@ -65,9 +74,9 @@
   associatorInv _ a b c = (inj1 (a +++ b) c . inj1 a b) ||| (inj2 a b +++ c)
   
 -- | Functor composition makes the category of endofunctors monoidal, with the identity functor as unit.
-instance Category k => TensorProduct (FunctorCompose k) where
+instance Category k => TensorProduct (EndoFunctorCompose k) where
   
-  type Unit (FunctorCompose k) = Id k
+  type Unit (EndoFunctorCompose k) = Id k
   unitObject _ = natId Id
   
   leftUnitor     _ (Nat g _ _) = idPostcomp g
@@ -85,12 +94,26 @@
   , multiply :: (Cod f ~ k) => k ((f :% (a, a))) a
   }
   
+trivialMonoid :: TensorProduct f => f -> MonoidObject f (Unit f)
+trivialMonoid f = MonoidObject (unitObject f) (leftUnitor f (unitObject f))
+
+coproductMonoid :: (HasInitialObject k, HasBinaryCoproducts k) => Obj k a -> MonoidObject (CoproductFunctor k) a
+coproductMonoid a = MonoidObject (initialize a) (a ||| a)
+
+
 -- | @ComonoidObject f a@ defines a comonoid @a@ in a comonoidal category with tensor product @f@.
 data ComonoidObject f a = ComonoidObject
   { counit     :: (Cod f ~ k) => k a (Unit f)
   , comultiply :: (Cod f ~ k) => k a (f :% (a, a))
   }
 
+trivialComonoid :: TensorProduct f => f -> ComonoidObject f (Unit f)
+trivialComonoid f = ComonoidObject (unitObject f) (leftUnitorInv f (unitObject f))
+  
+productComonoid :: (HasTerminalObject k, HasBinaryProducts k) => Obj k a -> ComonoidObject (ProductFunctor k) a
+productComonoid a = ComonoidObject (terminate a) (a &&& a)
+
+
 data MonoidAsCategory f m a b where
   MonoidValue :: (TensorProduct f, Dom f ~ (k :**: k), Cod f ~ k)
               => f -> MonoidObject f m -> k (Unit f) m -> MonoidAsCategory f m m m
@@ -105,7 +128,7 @@
 
 
 -- | A monad is a monoid in the category of endofunctors.
-type Monad f = MonoidObject (FunctorCompose (Dom f)) f
+type Monad f = MonoidObject (EndoFunctorCompose (Dom f)) f
 
 mkMonad :: (Functor f, Dom f ~ k, Cod f ~ k, Category k) 
   => f 
@@ -122,7 +145,7 @@
 
 
 -- | A comonad is a comonoid in the category of endofunctors.
-type Comonad f = ComonoidObject (FunctorCompose (Dom f)) f
+type Comonad f = ComonoidObject (EndoFunctorCompose (Dom f)) f
 
 mkComonad :: (Functor f, Dom f ~ k, Cod f ~ k, Category k) 
   => f 
diff --git a/Data/Category/NaturalTransformation.hs b/Data/Category/NaturalTransformation.hs
--- a/Data/Category/NaturalTransformation.hs
+++ b/Data/Category/NaturalTransformation.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, NoImplicitPrelude #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleInstances, FlexibleContexts, UndecidableInstances, RankNTypes, GADTs, LiberalTypeSynonyms, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.NaturalTransformation
@@ -38,8 +38,11 @@
     
   -- * Related functors
   , FunctorCompose(..)
-  , Precompose(..)
-  , Postcompose(..)
+  , EndoFunctorCompose
+  , Precompose
+  , precompose
+  , Postcompose
+  , postcompose
   , Wrap(..)
   
 ) where
@@ -120,59 +123,50 @@
 idPostcompInv f = Nat f (Id :.: f) (f %)
 
 
-constPrecomp :: (Category c1, Functor f) => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (f :.: Const c1 (Dom f) x) (Const c1 (Cod f) (f :% x))
+constPrecomp :: (Category c1, Functor f) 
+             => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (f :.: Const c1 (Dom f) x) (Const c1 (Cod f) (f :% x))
 constPrecomp (Const x) f = let fx = f % x in Nat (f :.: Const x) (Const fx) (\_ -> fx)
 
-constPrecompInv :: (Category c1, Functor f) => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (Const c1 (Cod f) (f :% x)) (f :.: Const c1 (Dom f) x)
+constPrecompInv :: (Category c1, Functor f) 
+                => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (Const c1 (Cod f) (f :% x)) (f :.: Const c1 (Dom f) x)
 constPrecompInv (Const x) f = let fx = f % x in Nat (Const fx) (f :.: Const x) (\_ -> fx)
 
-constPostcomp :: Functor f => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Cod f) c2 x :.: f) (Const (Dom f) c2 x)
+constPostcomp :: (Category c2, Functor f) 
+              => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Cod f) c2 x :.: f) (Const (Dom f) c2 x)
 constPostcomp (Const x) f = Nat (Const x :.: f) (Const x) (\_ -> x)
 
-constPostcompInv :: Functor f => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Dom f) c2 x) (Const (Cod f) c2 x :.: f)
+constPostcompInv :: (Category c2, Functor f) 
+                 => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Dom f) c2 x) (Const (Cod f) c2 x :.: f)
 constPostcompInv (Const x) f = Nat (Const x) (Const x :.: f) (\_ -> x)
 
 
-
--- | The category of endofunctors.
-type Endo k = Nat k k
-
-
-data FunctorCompose (k :: * -> * -> *) = FunctorCompose
+data FunctorCompose (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) = FunctorCompose
 
--- | Composition of endofunctors is a functor.
-instance Category k => Functor (FunctorCompose k) where
-  type Dom (FunctorCompose k) = Endo k :**: Endo k
-  type Cod (FunctorCompose k) = Endo k
-  type FunctorCompose k :% (f, g) = f :.: g
+-- | Composition of functors is a functor.
+instance (Category c, Category d, Category e) => Functor (FunctorCompose c d e) where
+  type Dom (FunctorCompose c d e) = Nat d e :**: Nat c d
+  type Cod (FunctorCompose c d e) = Nat c e
+  type FunctorCompose c d e :% (f, g) = f :.: g
   
   FunctorCompose % (n1 :**: n2) = n1 `o` n2
 
 
-data Precompose :: * -> (* -> * -> *) -> * where
-  Precompose :: f -> Precompose f d
-
--- | @Precompose f d@ is the functor such that @Precompose f d :% g = g :.: f@,
---   for functors @g@ that compose with @f@ and with codomain @d@.
-instance (Functor f, Category d) => Functor (Precompose f d) where
-  type Dom (Precompose f d) = Nat (Cod f) d
-  type Cod (Precompose f d) = Nat (Dom f) d
-  type Precompose f d :% g = g :.: f
-  
-  Precompose f % n = n `o` natId f
-
+-- | The category of endofunctors.
+type Endo k = Nat k k
+-- | Composition of endofunctors is a functor.
+type EndoFunctorCompose k = FunctorCompose k k k
 
-data Postcompose :: * -> (* -> * -> *) -> * where
-  Postcompose :: f -> Postcompose f c
+-- | @Precompose f e@ is the functor such that @Precompose f e :% g = g :.: f@,
+--   for functors @g@ that compose with @f@ and with codomain @e@.
+type Precompose f e = FunctorCompose (Dom f) (Cod f) e :.: Tuple2 (Nat (Cod f) e) (Nat (Dom f) (Cod f)) f
+precompose :: (Category e, Functor f) => f -> Precompose f e
+precompose f = FunctorCompose :.: tuple2 (natId f)
 
 -- | @Postcompose f c@ is the functor such that @Postcompose f c :% g = f :.: g@,
 --   for functors @g@ that compose with @f@ and with domain @c@.
-instance (Functor f, Category c) => Functor (Postcompose f c) where
-  type Dom (Postcompose f c) = Nat c (Dom f)
-  type Cod (Postcompose f c) = Nat c (Cod f)
-  type Postcompose f c :% g = f :.: g
-  
-  Postcompose f % n = natId f `o` n
+type Postcompose f c = FunctorCompose c (Dom f) (Cod f) :.: Tuple1 (Nat (Dom f) (Cod f)) (Nat c (Dom f)) f
+postcompose :: (Category e, Functor f) => f -> Postcompose f e
+postcompose f = FunctorCompose :.: Tuple1 (natId f)
 
 
 data Wrap f h = Wrap f h
diff --git a/Data/Category/Presheaf.hs b/Data/Category/Presheaf.hs
--- a/Data/Category/Presheaf.hs
+++ b/Data/Category/Presheaf.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, TypeSynonymInstances, GADTs, FlexibleInstances, NoImplicitPrelude #-}
+{-# LANGUAGE TypeOperators, TypeFamilies, TypeSynonymInstances, GADTs, FlexibleInstances, UndecidableInstances, NoImplicitPrelude #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Category.Presheaf
@@ -26,7 +26,7 @@
   :.: YonedaEmbedding k
   )
 pshExponential :: Category k => Obj (Presheaves k) y -> Obj (Presheaves k) z -> PShExponential k y z
-pshExponential y z = hom_X z :.: Opposite (ProductFunctor :.: Tuple2 y :.: yonedaEmbedding)
+pshExponential y z = hom_X z :.: Opposite (ProductFunctor :.: tuple2 y :.: yonedaEmbedding)
 
 -- | The category of presheaves on a category @C@ is cartesian closed for any @C@.
 instance Category k => CartesianClosed (Presheaves k) where
diff --git a/Data/Category/Simplex.hs b/Data/Category/Simplex.hs
--- a/Data/Category/Simplex.hs
+++ b/Data/Category/Simplex.hs
@@ -68,11 +68,11 @@
   tgt (Y f) = suc (tgt f)
   tgt (X f) = tgt f
   
-  Z     .    f  = f
-  f     .    Z  = f
-  (Y f) .    g  = Y (f . g)
-  (X f) . (Y g) = f . g
-  (X f) . (X g) = X ((X f) . g)
+  Z   .   f = f
+  f   .   Z = f
+  Y f .   g = Y (f . g)
+  X f . Y g = f . g
+  X f . X g = X (X f . g)
 
 
 -- | The ordinal @0@ is the initial object of the simplex category.
@@ -94,45 +94,6 @@
   terminate (X (Y f)) = X (terminate f)
 
 
-
-type Merge m n = BinaryCoproduct Simplex m n
-
-mergeLS :: Obj Simplex m -> Obj Simplex n -> Simplex (Merge (S m) n) (S (Merge m n))
-mergeLS Z Z = X (Y Z)
-mergeLS Z (X (Y n)) = X (Y (X (Y (Z +++ n))))
-mergeLS (X (Y m)) Z = X (Y (X (Y (m +++ Z))))
-mergeLS (X (Y m)) (X (Y n)) = X (Y (X (Y (mergeLS m n))))
-
-mergeRS :: Obj Simplex m -> Obj Simplex n -> Simplex (Merge m (S n)) (S (Merge m n))
-mergeRS Z Z = X (Y Z)
-mergeRS Z (X (Y n)) = X (Y (X (Y (Z +++ n))))
-mergeRS (X (Y m)) Z = X (Y (X (Y (m +++ Z))))
-mergeRS (X (Y m)) (X (Y n)) = X (Y (X (Y (mergeRS m n))))
-
--- | The coproduct in the simplex category is a merge operation.
-instance HasBinaryCoproducts Simplex where
-  type BinaryCoproduct Simplex  Z       Z  = Z
-  type BinaryCoproduct Simplex  Z    (S n) = S (Merge Z n)
-  type BinaryCoproduct Simplex (S m)    Z  = S (Merge m Z)
-  type BinaryCoproduct Simplex (S m) (S n) = S (S (Merge m n))
-
-  inj1       Z         Z   = Z
-  inj1       Z   (X (Y n)) = Y (inj1 Z n)
-  inj1 (X (Y m))       Z   = X (Y (inj1 m Z))
-  inj1 (X (Y m)) (X (Y n)) = X (Y (Y (inj1 m n)))
-
-  inj2       Z         Z   = Z
-  inj2       Z   (X (Y n)) = X (Y (inj2 Z n))
-  inj2 (X (Y m))       Z   = Y (inj2 m Z)
-  inj2 (X (Y m)) (X (Y n)) = Y (X (Y (inj2 m n)))
-
-  Z   ||| Z   = Z
-  X f ||| X g = X (X (f ||| g))
-  X f ||| Y g = X (f ||| Y g) . mergeLS (src f) (src g)
-  Y f ||| X g = X (Y f ||| g) . mergeRS (src f) (src g)
-  Y f ||| Y g = Y (f ||| g)
-
-
 data Fin :: * -> * where
   Fz ::          Fin (S n)
   Fs :: Fin n -> Fin (S n)
@@ -143,9 +104,9 @@
   type Dom Forget = Simplex
   type Cod Forget = (->)
   type Forget :% n = Fin n
-  Forget %  Z    = \x -> x
-  Forget % (Y f) = \x -> Fs ((Forget % f) x)
-  Forget % (X f) = \x -> case x of
+  Forget % Z   = \x -> x
+  Forget % Y f = \x -> Fs ((Forget % f) x)
+  Forget % X f = \x -> case x of
     Fz -> Fz
     Fs n -> (Forget % f) n
 
@@ -181,7 +142,7 @@
 
 
 -- | The maps @0 -> 1@ and @2 -> 1@ form a monoid, which is universal, c.f. `Replicate`.
-universalMonoid :: MonoidObject (CoproductFunctor Simplex) (S Z)
+universalMonoid :: MonoidObject Add (S Z)
 universalMonoid = MonoidObject { unit = Y Z, multiply = X (X (Y Z)) }
 
 data Replicate f a = Replicate f (MonoidObject f a)
diff --git a/Data/Category/Yoneda.hs b/Data/Category/Yoneda.hs
--- a/Data/Category/Yoneda.hs
+++ b/Data/Category/Yoneda.hs
@@ -15,11 +15,13 @@
 import Data.Category.NaturalTransformation
 import Data.Category.CartesianClosed
 
-type YonedaEmbedding k = Postcompose (Hom k) (Op k) :.: ToTuple2 k (Op k)
+type YonedaEmbedding k = 
+  Postcompose (Hom k) (Op k) :.: 
+  (Postcompose (Swap k (Op k)) (Op k) :.: Tuple k (Op k))
 
 -- | The Yoneda embedding functor, @C -> Set^(C^op)@.
 yonedaEmbedding :: Category k => YonedaEmbedding k
-yonedaEmbedding = Postcompose Hom :.: ToTuple2
+yonedaEmbedding = postcompose Hom :.: (postcompose swap :.: Tuple)
 
 
 data Yoneda (k :: * -> * -> *) f = Yoneda
diff --git a/data-category.cabal b/data-category.cabal
--- a/data-category.cabal
+++ b/data-category.cabal
@@ -1,5 +1,5 @@
 name:                data-category
-version:             0.5.1.1
+version:             0.6.0
 synopsis:            Category theory
 
 description:         Data-category is a collection of categories, and some categorical constructions on them.