diff --git a/Data/Category/Boolean.hs b/Data/Category/Boolean.hs
--- a/Data/Category/Boolean.hs
+++ b/Data/Category/Boolean.hs
@@ -8,7 +8,7 @@
 -- Stability   :  experimental
 -- Portability :  non-portable
 --
--- /2/, or the Boolean category. 
+-- /2/, or the Boolean category.
 -- It contains 2 objects, one for true and one for false.
 -- It contains 3 arrows, 2 identity arrows and one from false to true.
 -----------------------------------------------------------------------------
@@ -63,14 +63,14 @@
   terminate Tru = Tru
 
 
-type instance BinaryProduct Boolean Fls Fls = Fls
-type instance BinaryProduct Boolean Fls Tru = Fls
-type instance BinaryProduct Boolean Tru Fls = Fls
-type instance BinaryProduct Boolean Tru Tru = Tru
-
 -- | Conjunction is the binary product in the Boolean category.
-instance HasBinaryProducts Boolean where 
+instance HasBinaryProducts Boolean where
   
+  type BinaryProduct Boolean Fls Fls = Fls
+  type BinaryProduct Boolean Fls Tru = Fls
+  type BinaryProduct Boolean Tru Fls = Fls
+  type BinaryProduct Boolean Tru Tru = Tru
+  
   proj1 Fls Fls = Fls
   proj1 Fls Tru = Fls
   proj1 Tru Fls = F2T
@@ -87,14 +87,14 @@
   Tru &&& Tru = Tru
 
 
-type instance BinaryCoproduct Boolean Fls Fls = Fls
-type instance BinaryCoproduct Boolean Fls Tru = Tru
-type instance BinaryCoproduct Boolean Tru Fls = Tru
-type instance BinaryCoproduct Boolean Tru Tru = Tru
-
 -- | Disjunction is the binary coproduct in the Boolean category.
-instance HasBinaryCoproducts Boolean where 
+instance HasBinaryCoproducts Boolean where
   
+  type BinaryCoproduct Boolean Fls Fls = Fls
+  type BinaryCoproduct Boolean Fls Tru = Tru
+  type BinaryCoproduct Boolean Tru Fls = Tru
+  type BinaryCoproduct Boolean Tru Tru = Tru
+  
   inj1 Fls Fls = Fls
   inj1 Fls Tru = F2T
   inj1 Tru Fls = Tru
@@ -111,13 +111,13 @@
   Tru ||| Tru = Tru
 
 
-type instance Exponential Boolean Fls Fls = Tru
-type instance Exponential Boolean Fls Tru = Tru
-type instance Exponential Boolean Tru Fls = Fls
-type instance Exponential Boolean Tru Tru = Tru
-
 -- | Implication makes the Boolean category cartesian closed.
 instance CartesianClosed Boolean where
+  
+  type Exponential Boolean Fls Fls = Tru
+  type Exponential Boolean Fls Tru = Tru
+  type Exponential Boolean Tru Fls = Fls
+  type Exponential Boolean Tru Tru = Tru
   
   apply Fls Fls = Fls
   apply Fls Tru = F2T
diff --git a/Data/Category/CartesianClosed.hs b/Data/Category/CartesianClosed.hs
--- a/Data/Category/CartesianClosed.hs
+++ b/Data/Category/CartesianClosed.hs
@@ -19,10 +19,9 @@
 import Data.Category.Monoidal as M
 
 
-type family Exponential (k :: * -> * -> *) y z :: *
-
 -- | A category is cartesian closed if it has all products and exponentials for all objects.
 class (HasTerminalObject k, HasBinaryProducts k) => CartesianClosed k where
+  type Exponential k y z :: *
   
   apply :: Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z
   tuple :: Obj k y -> Obj k z -> k z (Exponential k y (BinaryProduct k z y))
@@ -30,19 +29,18 @@
 
 
 data ExpFunctor (k :: * -> * -> *) = ExpFunctor
-type instance Dom (ExpFunctor k) = Op k :**: k
-type instance Cod (ExpFunctor k) = k
-type instance (ExpFunctor k) :% (y, z) = Exponential k y z
 -- | The exponential as a bifunctor.
 instance CartesianClosed k => Functor (ExpFunctor k) where
-  ExpFunctor % (Op y :**: z) = z ^^^ y
+  type Dom (ExpFunctor k) = Op k :**: k
+  type Cod (ExpFunctor k) = k
+  type (ExpFunctor k) :% (y, z) = Exponential k y z
 
+  ExpFunctor % (Op y :**: z) = z ^^^ y
 
 
-type instance Exponential (->) y z = y -> z
-
 -- | Exponentials in @Hask@ are functions.
 instance CartesianClosed (->) where
+  type Exponential (->) y z = y -> z
   
   apply _ _ (f, y) = f y
   tuple _ _ z      = \y -> (z, y)
@@ -51,34 +49,33 @@
 
 
 data Apply (y :: * -> * -> *) (z :: * -> * -> *) = Apply
-type instance Dom (Apply y z) = Nat y z :**: y
-type instance Cod (Apply y z) = z
-type instance Apply y z :% (f, a) = f :% a
 -- | '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
   Apply % (l :**: r) = l ! r
 
 data ToTuple1 (y :: * -> * -> *) (z :: * -> * -> *) = ToTuple1
-type instance Dom (ToTuple1 y z) = z
-type instance Cod (ToTuple1 y z) = Nat y (z :**: y)
-type instance ToTuple1 y z :% a = Tuple1 z y a
 -- | '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
-type instance Dom (ToTuple2 y z) = y
-type instance Cod (ToTuple2 y z) = Nat z (z :**: y)
-type instance ToTuple2 y z :% a = Tuple2 z y a
 -- | '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)
 
 
-type instance Exponential Cat (CatW c) (CatW d) = CatW (Nat c d)
-
 -- | Exponentials in @Cat@ are the functor categories.
 instance CartesianClosed Cat where
+  type Exponential Cat (CatW c) (CatW d) = CatW (Nat c d)
   
   apply CatA{} CatA{}   = CatA Apply
   tuple CatA{} CatA{}   = CatA ToTuple1
@@ -86,10 +83,10 @@
 
 
 -- | The product functor is left adjoint the the exponential functor.
-curryAdj :: CartesianClosed k 
-         => Obj k y 
-         -> Adjunction k k 
-              (ProductFunctor k :.: Tuple2 k k y) 
+curryAdj :: CartesianClosed k
+         => Obj k y
+         -> 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)
 
diff --git a/Data/Category/Coproduct.hs b/Data/Category/Coproduct.hs
--- a/Data/Category/Coproduct.hs
+++ b/Data/Category/Coproduct.hs
@@ -40,58 +40,58 @@
   
     
 data Inj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Inj1
-type instance Dom (Inj1 c1 c2) = c1
-type instance Cod (Inj1 c1 c2) = c1 :++: c2
-type instance Inj1 c1 c2 :% a = I1 a
 -- | 'Inj1' is a functor which injects into the left category.
-instance (Category c1, Category c2) => Functor (Inj1 c1 c2) where 
+instance (Category c1, Category c2) => Functor (Inj1 c1 c2) where
+  type Dom (Inj1 c1 c2) = c1
+  type Cod (Inj1 c1 c2) = c1 :++: c2
+  type Inj1 c1 c2 :% a = I1 a
   Inj1 % f = I1 f
 
 data Inj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Inj2
-type instance Dom (Inj2 c1 c2) = c2
-type instance Cod (Inj2 c1 c2) = c1 :++: c2
-type instance Inj2 c1 c2 :% a = I2 a
 -- | 'Inj2' is a functor which injects into the right category.
-instance (Category c1, Category c2) => Functor (Inj2 c1 c2) where 
+instance (Category c1, Category c2) => Functor (Inj2 c1 c2) where
+  type Dom (Inj2 c1 c2) = c2
+  type Cod (Inj2 c1 c2) = c1 :++: c2
+  type Inj2 c1 c2 :% a = I2 a
   Inj2 % f = I2 f
 
 data f1 :+++: f2 = f1 :+++: f2
-type instance Dom (f1 :+++: f2) = Dom f1 :++: Dom f2
-type instance Cod (f1 :+++: f2) = Cod f1 :++: Cod f2
-type instance (f1 :+++: f2) :% (I1 a) = I1 (f1 :% a)
-type instance (f1 :+++: f2) :% (I2 a) = I2 (f2 :% a)
 -- | @f1 :+++: f2@ is the coproduct of the functors @f1@ and @f2@.
-instance (Functor f1, Functor f2) => Functor (f1 :+++: f2) where 
+instance (Functor f1, Functor f2) => Functor (f1 :+++: f2) where
+  type Dom (f1 :+++: f2) = Dom f1 :++: Dom f2
+  type Cod (f1 :+++: f2) = Cod f1 :++: Cod f2
+  type (f1 :+++: f2) :% (I1 a) = I1 (f1 :% a)
+  type (f1 :+++: f2) :% (I2 a) = I2 (f2 :% a)
   (g :+++: _) % I1 f = I1 (g % f)
   (_ :+++: g) % I2 f = I2 (g % f)
   
 data CodiagCoprod (k :: * -> * -> *) = CodiagCoprod
-type instance Dom (CodiagCoprod k) = k :++: k
-type instance Cod (CodiagCoprod k) = k
-type instance CodiagCoprod k :% I1 a = a
-type instance CodiagCoprod k :% I2 a = a
 -- | 'CodiagCoprod' is the codiagonal functor for coproducts.
-instance Category k => Functor (CodiagCoprod k) where 
+instance Category k => Functor (CodiagCoprod k) where
+  type Dom (CodiagCoprod k) = k :++: k
+  type Cod (CodiagCoprod k) = k
+  type CodiagCoprod k :% I1 a = a
+  type CodiagCoprod k :% I2 a = a
   CodiagCoprod % I1 f = f
   CodiagCoprod % I2 f = f
 
 data Cotuple1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Cotuple1 (Obj c1 a)
-type instance Dom (Cotuple1 c1 c2 a1) = c1 :++: c2
-type instance Cod (Cotuple1 c1 c2 a1) = c1
-type instance Cotuple1 c1 c2 _1 :% I1 a1 = a1
-type instance Cotuple1 c1 c2 a1 :% I2 a2 = a1
 -- | 'Cotuple1' projects out to the left category, replacing a value from the right category with a fixed object.
 instance (Category c1, Category c2) => Functor (Cotuple1 c1 c2 a1) where
+  type Dom (Cotuple1 c1 c2 a1) = c1 :++: c2
+  type Cod (Cotuple1 c1 c2 a1) = c1
+  type Cotuple1 c1 c2 a1 :% I1 a = a
+  type Cotuple1 c1 c2 a1 :% I2 a = a1
   Cotuple1 _ % I1 f = f
   Cotuple1 a % I2 _ = a
 
 data Cotuple2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Cotuple2 (Obj c2 a)
-type instance Dom (Cotuple2 c1 c2 a2) = c1 :++: c2
-type instance Cod (Cotuple2 c1 c2 a2) = c2
-type instance Cotuple2 c1 c2 a2 :% I1 a1 = a2
-type instance Cotuple2 c1 c2 _2 :% I2 a2 = a2
 -- | 'Cotuple2' projects out to the right category, replacing a value from the left category with a fixed object.
 instance (Category c1, Category c2) => Functor (Cotuple2 c1 c2 a2) where
+  type Dom (Cotuple2 c1 c2 a2) = c1 :++: c2
+  type Cod (Cotuple2 c1 c2 a2) = c2
+  type Cotuple2 c1 c2 a2 :% I1 a = a2
+  type Cotuple2 c1 c2 a2 :% I2 a = a
   Cotuple2 a % I1 _ = a
   Cotuple2 _ % I2 f = f
 
@@ -120,12 +120,15 @@
 
 
 data NatAsFunctor f g = NatAsFunctor (Nat (Dom f) (Cod f) f g)
-type instance Dom (NatAsFunctor f g) = Dom f :**: (Unit :>>: Unit)
-type instance Cod (NatAsFunctor f g) = Cod f
-type instance NatAsFunctor f g :% (a, I1 ()) = f :% a
-type instance NatAsFunctor f g :% (a, I2 ()) = g :% a
+
 -- | A natural transformation @Nat c d@ is isomorphic to a functor from @c :**: 2@ to @d@.
 instance (Functor f, Functor g, Dom f ~ Dom g, Cod f ~ Cod g) => Functor (NatAsFunctor f g) where
+  
+  type Dom (NatAsFunctor f g) = Dom f :**: (Unit :>>: Unit)
+  type Cod (NatAsFunctor f g) = Cod f
+  type NatAsFunctor f g :% (a, I1 ()) = f :% a
+  type NatAsFunctor f g :% (a, I2 ()) = g :% a
+  
   NatAsFunctor (Nat f _ _) % (a :**: I1A Unit) = f % a
   NatAsFunctor (Nat _ g _) % (a :**: I2A Unit) = g % a
   NatAsFunctor n           % (a :**: I12 Unit Unit) = n ! a
diff --git a/Data/Category/Dialg.hs b/Data/Category/Dialg.hs
--- a/Data/Category/Dialg.hs
+++ b/Data/Category/Dialg.hs
@@ -23,12 +23,12 @@
 
 -- | Objects of Dialg(F,G) are (F,G)-dialgebras.
 data Dialgebra f g a where
-  Dialgebra :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g) 
+  Dialgebra :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g)
     => Obj c a -> d (f :% a) (g :% a) -> Dialgebra f g a
 
 -- | Arrows of Dialg(F,G) are (F,G)-homomorphisms.
 data Dialg f g a b where
-  DialgA :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g) 
+  DialgA :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g)
     => Dialgebra f g a -> Dialgebra f g b -> c a b -> Dialg f g a b
 
 dialgId :: Dialgebra f g a -> Obj (Dialg f g) a
@@ -86,25 +86,25 @@
 
 
 data FreeAlg m = FreeAlg (Monad m)
-type instance Dom (FreeAlg m) = Dom m
-type instance Cod (FreeAlg m) = Alg m
-type instance FreeAlg m :% a = m :% a
 -- | @FreeAlg@ M takes @x@ to the free algebra @(M x, mu_x)@ of the monad @M@.
 instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (FreeAlg m) where
+  type Dom (FreeAlg m) = Dom m
+  type Cod (FreeAlg m) = Alg m
+  type FreeAlg m :% a = m :% a
   FreeAlg m % f = DialgA (alg (src f)) (alg (tgt f)) (monadFunctor m % f)
     where
       alg :: Obj k x -> Algebra m (m :% x)
       alg x = Dialgebra (monadFunctor m % x) (multiply m ! x)
 
 data ForgetAlg m = ForgetAlg
-type instance Dom (ForgetAlg m) = Alg m
-type instance Cod (ForgetAlg m) = Dom m
-type instance ForgetAlg m :% a = a
 -- | @ForgetAlg m@ is the forgetful functor for @Alg m@.
 instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (ForgetAlg m) where
+  type Dom (ForgetAlg m) = Alg m
+  type Cod (ForgetAlg m) = Dom m
+  type ForgetAlg m :% a = a
   ForgetAlg % DialgA _ _ f = f
 
-eilenbergMooreAdj :: (Functor m, Dom m ~ k, Cod m ~ k) 
+eilenbergMooreAdj :: (Functor m, Dom m ~ k, Cod m ~ k)
   => Monad m -> A.Adjunction (Alg m) k (FreeAlg m) (ForgetAlg m)
 eilenbergMooreAdj m = A.mkAdjunction (FreeAlg m) ForgetAlg
   (\x -> unit m ! x)
diff --git a/Data/Category/Fix.hs b/Data/Category/Fix.hs
--- a/Data/Category/Fix.hs
+++ b/Data/Category/Fix.hs
@@ -38,26 +38,26 @@
   terminalObject = Fix terminalObject
   terminate (Fix o) = Fix (terminate o)
 
-type instance BinaryProduct (Fix f) a b = BinaryProduct (f (Fix f)) a b
 -- | @Fix f@ inherits its (co)limits from @f (Fix f)@.
 instance HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f) where
+  type BinaryProduct (Fix f) a b = BinaryProduct (f (Fix f)) a b
   proj1 (Fix a) (Fix b) = Fix (proj1 a b)
   proj2 (Fix a) (Fix b) = Fix (proj2 a b)
   Fix a &&& Fix b = Fix (a &&& b)
   
-type instance BinaryCoproduct (Fix f) a b = BinaryCoproduct (f (Fix f)) a b
 -- | @Fix f@ inherits its (co)limits from @f (Fix f)@.
 instance HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f) where
+  type BinaryCoproduct (Fix f) a b = BinaryCoproduct (f (Fix f)) a b
   inj1 (Fix a) (Fix b) = Fix (inj1 a b)
   inj2 (Fix a) (Fix b) = Fix (inj2 a b)
   Fix a ||| Fix b = Fix (a ||| b)
 
 data Wrap (f :: (* -> * -> *) -> * -> * -> *) = Wrap
-type instance Dom (Wrap f) = f (Fix f)
-type instance Cod (Wrap f) = Fix f
-type instance Wrap f :% a = a
 -- | The `Wrap` functor wraps `Fix` around @f (Fix f)@.
 instance Category (f (Fix f)) => Functor (Wrap f) where
+  type Dom (Wrap f) = f (Fix f)
+  type Cod (Wrap f) = Fix f
+  type Wrap f :% a = a
   Wrap % f = Fix f
 
 -- | Take the `Omega` category, add a new disctinct object, and an arrow from that object to every object in `Omega`,
diff --git a/Data/Category/Functor.hs b/Data/Category/Functor.hs
--- a/Data/Category/Functor.hs
+++ b/Data/Category/Functor.hs
@@ -15,11 +15,8 @@
   , CatW
 
   -- * Functors
-  , Dom
-  , Cod
   , Functor(..)
-  , (:%)
-  
+
   -- ** Functor instances
   , Id(..)
   , (:.:)(..)
@@ -27,7 +24,7 @@
   , Opposite(..)
   , OpOp(..)
   , OpOpInv(..)
-  
+
   -- *** Related to the product category
   , Proj1(..)
   , Proj2(..)
@@ -35,14 +32,14 @@
   , DiagProd(..)
   , Tuple1(..)
   , Tuple2(..)
-  
+
   -- *** Hom functors
   , Hom(..)
   , (:*-:)
   , homX_
   , (:-*:)
   , hom_X
-  
+
 ) where
   
 import Data.Category
@@ -51,20 +48,25 @@
 infixr 9 %
 infixr 9 :%
 
--- | The domain, or source category, of the functor.
-type family Dom ftag :: * -> * -> *
--- | The codomain, or target category, of the functor.
-type family Cod ftag :: * -> * -> *
 
+
 -- | Functors map objects and arrows.
 class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where
+  
+  -- | The domain, or source category, of the functor.
+  type Dom ftag :: * -> * -> *
+  -- | The codomain, or target category, of the functor.
+  type Cod ftag :: * -> * -> *
+
+  -- | @:%@ maps objects.
+  type ftag :% a :: *
+  
   -- | @%@ maps arrows.
   (%)  :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
 
--- | @:%@ maps objects.
-type family ftag :% a :: *
 
 
+
 -- | Functors are arrows in the category Cat.
 data Cat :: * -> * -> * where
   CatA :: (Functor ftag, Category (Dom ftag), Category (Cod ftag)) => ftag -> Cat (CatW (Dom ftag)) (CatW (Cod ftag))
@@ -85,36 +87,37 @@
 
 data Id (k :: * -> * -> *) = Id
 
-type instance Dom (Id k) = k
-type instance Cod (Id k) = k
-type instance Id k :% a = a
-
 -- | The identity functor on k
-instance Category k => Functor (Id k) where 
+instance Category k => Functor (Id k) where
+  type Dom (Id k) = k
+  type Cod (Id k) = k
+  type Id k :% a = a
+
   _ % f = f
 
 
 data (g :.: h) where
   (:.:) :: (Functor g, Functor h, Cod h ~ Dom g) => g -> h -> g :.: h
-  
-type instance Dom (g :.: h) = Dom h
-type instance Cod (g :.: h) = Cod g
-type instance (g :.: h) :% a = g :% (h :% a)
 
 -- | The composition of two functors.
-instance (Category (Cod g), Category (Dom h)) => Functor (g :.: h) where 
+instance (Category (Cod g), Category (Dom h)) => Functor (g :.: h) where
+  type Dom (g :.: h) = Dom h
+  type Cod (g :.: h) = Cod g
+  type (g :.: h) :% a = g :% (h :% a)
+
   (g :.: h) % f = g % (h % f)
+  
 
 
 data Const (c1 :: * -> * -> *) (c2 :: * -> * -> *) x where
   Const :: Category c2 => Obj c2 x -> Const c1 c2 x
-  
-type instance Dom (Const c1 c2 x) = c1
-type instance Cod (Const c1 c2 x) = c2
-type instance Const c1 c2 x :% a = x
 
 -- | The constant functor.
-instance (Category c1, Category c2) => Functor (Const c1 c2 x) where 
+instance (Category c1, Category c2) => Functor (Const c1 c2 x) where
+  type Dom (Const c1 c2 x) = c1
+  type Cod (Const c1 c2 x) = c2
+  type Const c1 c2 x :% a = x
+  
   Const x % _ = x
 
 -- | The constant functor with the same domain and codomain as f.
@@ -123,112 +126,112 @@
 
 data Opposite f where
   Opposite :: Functor f => f -> Opposite f
-  
-type instance Dom (Opposite f) = Op (Dom f)
-type instance Cod (Opposite f) = Op (Cod f)
-type instance Opposite f :% a = f :% a
 
 -- | The dual of a functor
 instance (Category (Dom f), Category (Cod f)) => Functor (Opposite f) where
+  type Dom (Opposite f) = Op (Dom f)
+  type Cod (Opposite f) = Op (Cod f)
+  type Opposite f :% a = f :% a
+  
   Opposite f % Op a = Op (f % a)
 
 
 data OpOp (k :: * -> * -> *) = OpOp
 
-type instance Dom (OpOp k) = Op (Op k)
-type instance Cod (OpOp k) = k
-type instance OpOp k :% a = a
-
 -- | The @Op (Op x) = x@ functor.
 instance Category k => Functor (OpOp k) where
+  type Dom (OpOp k) = Op (Op k)
+  type Cod (OpOp k) = k
+  type OpOp k :% a = a
+  
   OpOp % Op (Op f) = f
 
 
 data OpOpInv (k :: * -> * -> *) = OpOpInv
 
-type instance Dom (OpOpInv k) = k
-type instance Cod (OpOpInv k) = Op (Op k)
-type instance OpOpInv k :% a = a
-
 -- | The @x = Op (Op x)@ functor.
 instance Category k => Functor (OpOpInv k) where
+  type Dom (OpOpInv k) = k
+  type Cod (OpOpInv k) = Op (Op k)
+  type OpOpInv k :% a = a
+  
   OpOpInv % f = Op (Op f)
 
 
 data Proj1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj1
 
-type instance Dom (Proj1 c1 c2) = c1 :**: c2
-type instance Cod (Proj1 c1 c2) = c1
-type instance Proj1 c1 c2 :% (a1, a2) = a1
-
 -- | 'Proj1' is a bifunctor that projects out the first component of a product.
-instance (Category c1, Category c2) => Functor (Proj1 c1 c2) where 
+instance (Category c1, Category c2) => Functor (Proj1 c1 c2) where
+  type Dom (Proj1 c1 c2) = c1 :**: c2
+  type Cod (Proj1 c1 c2) = c1
+  type Proj1 c1 c2 :% (a1, a2) = a1
+  
   Proj1 % (f1 :**: _) = f1
 
 
 data Proj2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Proj2
 
-type instance Dom (Proj2 c1 c2) = c1 :**: c2
-type instance Cod (Proj2 c1 c2) = c2
-type instance Proj2 c1 c2 :% (a1, a2) = a2
-
 -- | 'Proj2' is a bifunctor that projects out the second component of a product.
-instance (Category c1, Category c2) => Functor (Proj2 c1 c2) where 
+instance (Category c1, Category c2) => Functor (Proj2 c1 c2) where
+  type Dom (Proj2 c1 c2) = c1 :**: c2
+  type Cod (Proj2 c1 c2) = c2
+  type Proj2 c1 c2 :% (a1, a2) = a2
+  
   Proj2 % (_ :**: f2) = f2
 
 
 data f1 :***: f2 = f1 :***: f2
 
-type instance Dom (f1 :***: f2) = Dom f1 :**: Dom f2
-type instance Cod (f1 :***: f2) = Cod f1 :**: Cod f2
-type instance (f1 :***: f2) :% (a1, a2) = (f1 :% a1, f2 :% a2)
-
 -- | @f1 :***: f2@ is the product of the functors @f1@ and @f2@.
-instance (Functor f1, Functor f2) => Functor (f1 :***: f2) where 
-  (g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2)
-  
+instance (Functor f1, Functor f2) => Functor (f1 :***: f2) where
+  type Dom (f1 :***: f2) = Dom f1 :**: Dom f2
+  type Cod (f1 :***: f2) = Cod f1 :**: Cod f2
+  type (f1 :***: f2) :% (a1, a2) = (f1 :% a1, f2 :% a2)
   
-data DiagProd (k :: * -> * -> *) = DiagProd
+  (g1 :***: g2) % (f1 :**: f2) = (g1 % f1) :**: (g2 % f2)
 
-type instance Dom (DiagProd k) = k
-type instance Cod (DiagProd k) = k :**: k
-type instance DiagProd k :% a = (a, a)
 
+data DiagProd (k :: * -> * -> *) = DiagProd
+
 -- | 'DiagProd' is the diagonal functor for products.
-instance Category k => Functor (DiagProd k) where 
+instance Category k => Functor (DiagProd k) where
+  type Dom (DiagProd k) = k
+  type Cod (DiagProd k) = k :**: k
+  type DiagProd k :% a = (a, a)
+  
   DiagProd % f = f :**: f
 
 
 data Tuple1 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple1 (Obj c1 a)
 
-type instance Dom (Tuple1 c1 c2 a1) = c2
-type instance Cod (Tuple1 c1 c2 a1) = c1 :**: c2
-type instance Tuple1 c1 c2 a1 :% a2 = (a1, a2)
-
 -- | 'Tuple1' tuples with a fixed object on the left.
 instance (Category c1, Category c2) => Functor (Tuple1 c1 c2 a1) where
+  type Dom (Tuple1 c1 c2 a1) = c2
+  type Cod (Tuple1 c1 c2 a1) = c1 :**: c2
+  type Tuple1 c1 c2 a1 :% a2 = (a1, a2)
+  
   Tuple1 a % f = a :**: f
 
 
 data Tuple2 (c1 :: * -> * -> *) (c2 :: * -> * -> *) a = Tuple2 (Obj c2 a)
 
-type instance Dom (Tuple2 c1 c2 a2) = c1
-type instance Cod (Tuple2 c1 c2 a2) = c1 :**: c2
-type instance Tuple2 c1 c2 a2 :% a1 = (a1, a2)
-
 -- | '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
 
 
-data Hom (k :: * -> * -> *) = Hom  
-
-type instance Dom (Hom k) = Op k :**: k
-type instance Cod (Hom k) = (->)
-type instance (Hom k) :% (a1, a2) = k a1 a2
+data Hom (k :: * -> * -> *) = Hom
 
 -- | The Hom functor, Hom(--,--), a bifunctor contravariant in its first argument and covariant in its second argument.
-instance Category k => Functor (Hom k) where 
+instance Category k => Functor (Hom k) where
+  type Dom (Hom k) = Op k :**: k
+  type Cod (Hom k) = (->)
+  type (Hom k) :% (a1, a2) = k a1 a2
+  
   Hom % (Op f1 :**: f2) = \g -> f2 . g . f1
 
 
diff --git a/Data/Category/Kleisli.hs b/Data/Category/Kleisli.hs
--- a/Data/Category/Kleisli.hs
+++ b/Data/Category/Kleisli.hs
@@ -8,7 +8,7 @@
 -- Stability   :  experimental
 -- Portability :  non-portable
 --
--- This is an attempt at the Kleisli category, and the construction 
+-- This is an attempt at the Kleisli category, and the construction
 -- of an adjunction for each monad.
 -----------------------------------------------------------------------------
 module Data.Category.Kleisli where
@@ -37,20 +37,20 @@
 
 
 data KleisliAdjF m = KleisliAdjF (Monad m)
-type instance Dom (KleisliAdjF m) = Dom m
-type instance Cod (KleisliAdjF m) = Kleisli m
-type instance KleisliAdjF m :% a = a
 instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjF m) where
+  type Dom (KleisliAdjF m) = Dom m
+  type Cod (KleisliAdjF m) = Kleisli m
+  type KleisliAdjF m :% a = a
   KleisliAdjF m % f = Kleisli m (tgt f) ((unit m ! tgt f) . f)
    
 data KleisliAdjG m = KleisliAdjG (Monad m)
-type instance Dom (KleisliAdjG m) = Kleisli m
-type instance Cod (KleisliAdjG m) = Dom m
-type instance KleisliAdjG m :% a = m :% a
 instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjG m) where
+  type Dom (KleisliAdjG m) = Kleisli m
+  type Cod (KleisliAdjG m) = Dom m
+  type KleisliAdjG m :% a = m :% a
   KleisliAdjG m % Kleisli _ b f = (multiply m ! b) . (monadFunctor m % f)
 
-kleisliAdj :: (Functor m, Dom m ~ k, Cod m ~ k) 
+kleisliAdj :: (Functor m, Dom m ~ k, Cod m ~ k)
   => Monad m -> A.Adjunction (Kleisli m) k (KleisliAdjF m) (KleisliAdjG m)
 kleisliAdj m = A.mkAdjunction (KleisliAdjF m) (KleisliAdjG m)
   (\x -> unit m ! x)
diff --git a/Data/Category/Limit.hs b/Data/Category/Limit.hs
--- a/Data/Category/Limit.hs
+++ b/Data/Category/Limit.hs
@@ -1,14 +1,14 @@
-{-# LANGUAGE 
-  FlexibleContexts, 
-  FlexibleInstances, 
-  GADTs, 
+{-# LANGUAGE
+  FlexibleContexts,
+  FlexibleInstances,
+  GADTs,
   MultiParamTypeClasses,
-  RankNTypes, 
+  RankNTypes,
   ScopedTypeVariables,
-  TypeOperators, 
+  TypeOperators,
   TypeFamilies,
   TypeSynonymInstances,
-  UndecidableInstances, 
+  UndecidableInstances,
   LambdaCase,
   NoImplicitPrelude  #-}
 -----------------------------------------------------------------------------
@@ -54,19 +54,13 @@
   , Zero
   
   -- ** Limits of type Pair
-  , BinaryProduct
   , HasBinaryProducts(..)
   , ProductFunctor(..)
   , (:*:)(..)
-  , BinaryCoproduct
   , HasBinaryCoproducts(..)
   , CoproductFunctor(..)
   , (:+:)(..)
   
-  -- -- ** Limits of type Hask
-  -- , ForAll(..)
-  -- , Exists(..)
-  
 ) where
 
 import Data.Category
@@ -88,12 +82,12 @@
 data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where
   Diag :: Diag j k
   
-type instance Dom (Diag j k) = k
-type instance Cod (Diag j k) = Nat j k
-type instance Diag j k :% a = Const j k a
-
 -- | The diagonal functor from (index-) category J to k.
-instance (Category j, Category k) => Functor (Diag j k) where 
+instance (Category j, Category k) => Functor (Diag j k) where
+  type Dom (Diag j k) = k
+  type Cod (Diag j k) = Nat j k
+  type Diag j k :% a = Const j k a
+  
   Diag % f = Nat (Const (src f)) (Const (tgt f)) (\_ -> f)
 
 -- | The diagonal functor with the same domain and codomain as @f@.
@@ -127,17 +121,18 @@
 class (Category j, Category k) => HasLimits j k where
   -- | 'limit' returns the limiting cone for a functor @f@.
   limit           :: Obj (Nat j k) f -> Cone f (Limit f)
-  -- | 'limitFactorizer' shows that the limiting cone is universal – i.e. any other cone of @f@ factors through it –
+  -- | 'limitFactorizer' shows that the limiting cone is universal – i.e. any other cone of @f@ factors through it
   --   by returning the morphism between the vertices of the cones.
   limitFactorizer :: Obj (Nat j k) f -> (forall n. Cone f n -> k n (Limit f))
 
 data LimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = LimitFunctor
-type instance Dom (LimitFunctor j k) = Nat j k
-type instance Cod (LimitFunctor j k) = k
-type instance LimitFunctor j k :% f = LimitFam j k f
 -- | If every diagram of type @j@ has a limit in @k@ there exists a limit functor.
 --   It can be seen as a generalisation of @(***)@.
 instance HasLimits j k => Functor (LimitFunctor j k) where
+  type Dom (LimitFunctor j k) = Nat j k
+  type Cod (LimitFunctor j k) = k
+  type LimitFunctor j k :% f = LimitFam j k f
+
   LimitFunctor % n @ Nat{}  = limitFactorizer (tgt n) (n . limit (src n))
 
 -- | The limit functor is right adjoint to the diagonal functor.
@@ -156,22 +151,23 @@
 class (Category j, Category k) => HasColimits j k where
   -- | 'colimit' returns the limiting co-cone for a functor @f@.
   colimit           :: Obj (Nat j k) f -> Cocone f (Colimit f)
-  -- | 'colimitFactorizer' shows that the limiting co-cone is universal – i.e. any other co-cone of @f@ factors through it –
+  -- | 'colimitFactorizer' shows that the limiting co-cone is universal – i.e. any other co-cone of @f@ factors through it
   --   by returning the morphism between the vertices of the cones.
   colimitFactorizer :: Obj (Nat j k) f -> (forall n. Cocone f n -> k (Colimit f) n)
 
 data ColimitFunctor (j :: * -> * -> *) (k  :: * -> * -> *) = ColimitFunctor
-type instance Dom (ColimitFunctor j k) = Nat j k
-type instance Cod (ColimitFunctor j k) = k
-type instance ColimitFunctor j k :% f = ColimitFam j k f
 -- | If every diagram of type @j@ has a colimit in @k@ there exists a colimit functor.
 --   It can be seen as a generalisation of @(+++)@.
 instance HasColimits j k => Functor (ColimitFunctor j k) where
+  type Dom (ColimitFunctor j k) = Nat j k
+  type Cod (ColimitFunctor j k) = k
+  type ColimitFunctor j k :% f = ColimitFam j k f
+
   ColimitFunctor % n @ Nat{}  = colimitFactorizer (src n) (colimit (tgt n) . n)
 
 -- | The colimit functor is left adjoint to the diagonal functor.
 colimitAdj :: forall j k. HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)
-colimitAdj = mkAdjunction ColimitFunctor diag (\f @ Nat{} -> colimit f) (\a -> colimitFactorizer (diag % a) (diag % a)) 
+colimitAdj = mkAdjunction ColimitFunctor diag (\f @ Nat{} -> colimit f) (\a -> colimitFactorizer (diag % a) (diag % a))
   where diag = Diag :: Diag j k -- Forces the type of all Diags to be the same.
   
 
@@ -196,7 +192,6 @@
 
 -- | @()@ is the terminal object in @Hask@.
 instance HasTerminalObject (->) where
-  
   type TerminalObject (->) = ()
   
   terminalObject = \x -> x
@@ -205,7 +200,6 @@
 
 -- | @Unit@ is the terminal category.
 instance HasTerminalObject Cat where
-  
   type TerminalObject Cat = CatW Unit
   
   terminalObject = CatA Id
@@ -214,7 +208,6 @@
 
 -- | The constant functor to the terminal object is itself the terminal object in its functor category.
 instance (Category c, HasTerminalObject d) => HasTerminalObject (Nat c d) where
-  
   type TerminalObject (Nat c d) = Const c d (TerminalObject d)
   
   terminalObject = natId (Const terminalObject)
@@ -223,7 +216,6 @@
 
 -- | The category of one object has that object as terminal object.
 instance HasTerminalObject Unit where
-  
   type TerminalObject Unit = ()
   
   terminalObject = Unit
@@ -232,7 +224,6 @@
   
 -- | The terminal object of the product of 2 categories is the product of their terminal objects.
 instance (HasTerminalObject c1, HasTerminalObject c2) => HasTerminalObject (c1 :**: c2) where
-  
   type TerminalObject (c1 :**: c2) = (TerminalObject c1, TerminalObject c2)
   
   terminalObject = terminalObject :**: terminalObject
@@ -241,7 +232,6 @@
   
 -- | The terminal object of the direct coproduct of categories is the terminal object of the terminal category.
 instance (Category c1, HasTerminalObject c2) => HasTerminalObject (c1 :>>: c2) where
-  
   type TerminalObject (c1 :>>: c2) = I2 (TerminalObject c2)
   
   terminalObject = I2A terminalObject
@@ -252,7 +242,6 @@
 
 
 class Category k => HasInitialObject k where
-  
   type InitialObject k :: *
   
   initialObject :: Obj k (InitialObject k)
@@ -273,7 +262,6 @@
 
 -- | Any empty data type is an initial object in @Hask@.
 instance HasInitialObject (->) where
-  
   type InitialObject (->) = Zero
   
   initialObject = \x -> x
@@ -282,7 +270,6 @@
 
 -- | The empty category is the initial object in @Cat@.
 instance HasInitialObject Cat where
-  
   type InitialObject Cat = CatW Void
   
   initialObject = CatA Id
@@ -291,7 +278,6 @@
 
 -- | The constant functor to the initial object is itself the initial object in its functor category.
 instance (Category c, HasInitialObject d) => HasInitialObject (Nat c d) where
-  
   type InitialObject (Nat c d) = Const c d (InitialObject d)
   
   initialObject = natId (Const initialObject)
@@ -300,16 +286,14 @@
 
 -- | The initial object of the product of 2 categories is the product of their initial objects.
 instance (HasInitialObject c1, HasInitialObject c2) => HasInitialObject (c1 :**: c2) where
-  
   type InitialObject (c1 :**: c2) = (InitialObject c1, InitialObject c2)
   
   initialObject = initialObject :**: initialObject
   
   initialize (a1 :**: a2) = initialize a1 :**: initialize a2
 
--- | The category of one object has that object as initial object. 
+-- | The category of one object has that object as initial object.
 instance HasInitialObject Unit where
-  
   type InitialObject Unit = ()
   
   initialObject = Unit
@@ -318,7 +302,6 @@
 
 -- | The initial object of the direct coproduct of categories is the initial object of the initial category.
 instance (HasInitialObject c1, Category c2) => HasInitialObject (c1 :>>: c2) where
-  
   type InitialObject (c1 :>>: c2) = I1 (InitialObject c1)
   
   initialObject = I1A initialObject
@@ -327,9 +310,8 @@
   initialize (I2A a) = I12 initialObject a
 
 
-type family BinaryProduct (k :: * -> * -> *) x y :: *
-
 class Category k => HasBinaryProducts k where
+  type BinaryProduct (k :: * -> * -> *) x y :: *
   
   proj1 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) x
   proj2 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) y
@@ -340,7 +322,7 @@
   l *** r = (l . proj1 (src l) (src r)) &&& (r . proj2 (src l) (src r))
 
 
-type instance LimitFam (i :++: j) k f = BinaryProduct k 
+type instance LimitFam (i :++: j) k f = BinaryProduct k
   (LimitFam i k (f :.: Inj1 i j))
   (LimitFam j k (f :.: Inj2 i j))
 
@@ -360,16 +342,15 @@
           h (I1 n) = Com (lim1 ! n . proj1 x y)
           h (I2 n) = Com (lim2 ! n . proj2 x y)
 
-  limitFactorizer l@Nat{} c = 
+  limitFactorizer l@Nat{} c =
     limitFactorizer (l `o` natId Inj1) ((c `o` natId Inj1) . constPostcompInv (srcF c) Inj1)
-    &&& 
+    &&&
     limitFactorizer (l `o` natId Inj2) ((c `o` natId Inj2) . constPostcompInv (srcF c) Inj2)
 
 
-type instance BinaryProduct (->) x y = (x, y)
-
 -- | The tuple is the binary product in @Hask@.
 instance HasBinaryProducts (->) where
+  type BinaryProduct (->) x y = (x, y)
   
   proj1 _ _ = \(x, _) -> x
   proj2 _ _ = \(_, y) -> y
@@ -377,10 +358,9 @@
   f &&& g = \x -> (f x, g x)
   f *** g = \(x, y) -> (f x, g y)
 
-type instance BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :**: c2)
-
 -- | The product of categories ':**:' is the binary product in 'Cat'.
 instance HasBinaryProducts Cat where
+  type BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :**: c2)
   
   proj1 (CatA _) (CatA _) = CatA Proj1
   proj2 (CatA _) (CatA _) = CatA Proj2
@@ -388,10 +368,9 @@
   CatA f1 &&& CatA f2 = CatA ((f1 :***: f2) :.: DiagProd)
   CatA f1 *** CatA f2 = CatA (f1 :***: f2)
 
-type instance BinaryProduct Unit () () = ()
-
 -- | In the category of one object that object is its own product.
 instance HasBinaryProducts Unit where
+  type BinaryProduct Unit () () = ()
 
   proj1 Unit Unit = Unit
   proj2 Unit Unit = Unit
@@ -399,10 +378,9 @@
   Unit &&& Unit = Unit
   Unit *** Unit = Unit
 
-type instance BinaryProduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryProduct c1 x1 y1, BinaryProduct c2 x2 y2)
-
 -- | The binary product of the product of 2 categories is the product of their binary products.
 instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :**: c2) where
+  type BinaryProduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryProduct c1 x1 y1, BinaryProduct c2 x2 y2)
   
   proj1 (x1 :**: x2) (y1 :**: y2) = proj1 x1 y1 :**: proj1 x2 y2
   proj2 (x1 :**: x2) (y1 :**: y2) = proj2 x1 y1 :**: proj2 x2 y2
@@ -410,13 +388,12 @@
   (f1 :**: f2) &&& (g1 :**: g2) = (f1 &&& g1) :**: (f2 &&& g2)
   (f1 :**: f2) *** (g1 :**: g2) = (f1 *** g1) :**: (f2 *** g2)
 
-type instance BinaryProduct (c1 :>>: c2) (I1 a) (I1 b) = I1 (BinaryProduct c1 a b)
-type instance BinaryProduct (c1 :>>: c2) (I1 a) (I2 b) = I1 a
-type instance BinaryProduct (c1 :>>: c2) (I2 a) (I1 b) = I1 b
-type instance BinaryProduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryProduct c2 a b)
-
 instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :>>: c2) where
-
+  type BinaryProduct (c1 :>>: c2) (I1 a) (I1 b) = I1 (BinaryProduct c1 a b)
+  type BinaryProduct (c1 :>>: c2) (I1 a) (I2 b) = I1 a
+  type BinaryProduct (c1 :>>: c2) (I2 a) (I1 b) = I1 b
+  type BinaryProduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryProduct c2 a b)
+  
   proj1 (I1A a) (I1A b) = I1A (proj1 a b)
   proj1 (I1A a) (I2A _) = I1A a
   proj1 (I2A a) (I1A b) = I12 b a
@@ -434,27 +411,28 @@
 
 
 data ProductFunctor (k :: * -> * -> *) = ProductFunctor
-type instance Dom (ProductFunctor k) = k :**: k
-type instance Cod (ProductFunctor k) = k
-type instance ProductFunctor k :% (a, b) = BinaryProduct k a b
 -- | Binary product as a bifunctor.
 instance HasBinaryProducts k => Functor (ProductFunctor k) where
+  type Dom (ProductFunctor k) = k :**: k
+  type Cod (ProductFunctor k) = k
+  type ProductFunctor k :% (a, b) = BinaryProduct k a b
+
   ProductFunctor % (a1 :**: a2) = a1 *** a2
 
-data p :*: q where 
+data p :*: q where
   (:*:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryProducts k) => p -> q -> p :*: q
-type instance Dom (p :*: q) = Dom p
-type instance Cod (p :*: q) = Cod p
-type instance (p :*: q) :% a = BinaryProduct (Cod p) (p :% a) (q :% a)
 -- | The product of two functors, passing the same object to both functors and taking the product of the results.
 instance (Category (Dom p), Category (Cod p)) => Functor (p :*: q) where
-  (p :*: q) % f = (p % f) *** (q % f)
+  type Dom (p :*: q) = Dom p
+  type Cod (p :*: q) = Cod p
+  type (p :*: q) :% a = BinaryProduct (Cod p) (p :% a) (q :% a)
 
-type instance BinaryProduct (Nat c d) x y = x :*: y
+  (p :*: q) % f = (p % f) *** (q % f)
 
 -- | The functor product ':*:' is the binary product in functor categories.
 instance (Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d) where
-  
+  type BinaryProduct (Nat c d) x y = x :*: y
+    
   proj1 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) f (\z -> proj1 (f % z) (g % z))
   proj2 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) g (\z -> proj2 (f % z) (g % z))
   
@@ -463,9 +441,8 @@
   
   
 
-type family BinaryCoproduct (k :: * -> * -> *) x y :: *
-
 class Category k => HasBinaryCoproducts k where
+  type BinaryCoproduct (k :: * -> * -> *) x y :: *
 
   inj1 :: Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
   inj2 :: Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
@@ -476,7 +453,7 @@
   l +++ r = (inj1 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r)
     
 
-type instance ColimitFam (i :++: j) k f = BinaryCoproduct k 
+type instance ColimitFam (i :++: j) k f = BinaryCoproduct k
   (ColimitFam i k (f :.: Inj1 i j))
   (ColimitFam j k (f :.: Inj2 i j))
 
@@ -496,27 +473,25 @@
           h (I1 n) = Com (inj1 x y . col1 ! n)
           h (I2 n) = Com (inj2 x y . col2 ! n)
   
-  colimitFactorizer l@Nat{} c = 
+  colimitFactorizer l@Nat{} c =
     colimitFactorizer (l `o` natId Inj1) (constPostcomp (tgtF c) Inj1 . (c `o` natId Inj1))
-    ||| 
+    |||
     colimitFactorizer (l `o` natId Inj2) (constPostcomp (tgtF c) Inj2 . (c `o` natId Inj2))
 
 
-type instance BinaryCoproduct Cat (CatW c1) (CatW c2) = CatW (c1 :++: c2)
-
 -- | The coproduct of categories ':++:' is the binary coproduct in 'Cat'.
 instance HasBinaryCoproducts Cat where
-  
+  type BinaryCoproduct Cat (CatW c1) (CatW c2) = CatW (c1 :++: c2)
+    
   inj1 (CatA _) (CatA _) = CatA Inj1
   inj2 (CatA _) (CatA _) = CatA Inj2
   
   CatA f1 ||| CatA f2 = CatA (CodiagCoprod :.: (f1 :+++: f2))
   CatA f1 +++ CatA f2 = CatA (f1 :+++: f2)
 
-type instance BinaryCoproduct Unit () () = ()
-
 -- | In the category of one object that object is its own coproduct.
 instance HasBinaryCoproducts Unit where
+  type BinaryCoproduct Unit () () = ()
   
   inj1 Unit Unit = Unit
   inj2 Unit Unit = Unit
@@ -524,10 +499,9 @@
   Unit ||| Unit = Unit
   Unit +++ Unit = Unit
   
-type instance BinaryCoproduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryCoproduct c1 x1 y1, BinaryCoproduct c2 x2 y2)
-
 -- | The binary coproduct of the product of 2 categories is the product of their binary coproducts.
 instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :**: c2) where
+  type BinaryCoproduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryCoproduct c1 x1 y1, BinaryCoproduct c2 x2 y2)
   
   inj1 (x1 :**: x2) (y1 :**: y2) = inj1 x1 y1 :**: inj1 x2 y2
   inj2 (x1 :**: x2) (y1 :**: y2) = inj2 x1 y1 :**: inj2 x2 y2
@@ -535,12 +509,11 @@
   (f1 :**: f2) ||| (g1 :**: g2) = (f1 ||| g1) :**: (f2 ||| g2)
   (f1 :**: f2) +++ (g1 :**: g2) = (f1 +++ g1) :**: (f2 +++ g2)
 
-type instance BinaryCoproduct (c1 :>>: c2) (I1 a) (I1 b) = I1 (BinaryCoproduct c1 a b)
-type instance BinaryCoproduct (c1 :>>: c2) (I1 a) (I2 b) = I2 b
-type instance BinaryCoproduct (c1 :>>: c2) (I2 a) (I1 b) = I2 a
-type instance BinaryCoproduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryCoproduct c2 a b)
-
 instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :>>: c2) where
+  type BinaryCoproduct (c1 :>>: c2) (I1 a) (I1 b) = I1 (BinaryCoproduct c1 a b)
+  type BinaryCoproduct (c1 :>>: c2) (I1 a) (I2 b) = I2 b
+  type BinaryCoproduct (c1 :>>: c2) (I2 a) (I1 b) = I2 a
+  type BinaryCoproduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryCoproduct c2 a b)
 
   inj1 (I1A a) (I1A b) = I1A (inj1 a b)
   inj1 (I1A a) (I2A b) = I12 a b
@@ -559,26 +532,27 @@
 
 
 data CoproductFunctor (k :: * -> * -> *) = CoproductFunctor
-type instance Dom (CoproductFunctor k) = k :**: k
-type instance Cod (CoproductFunctor k) = k
-type instance CoproductFunctor k :% (a, b) = BinaryCoproduct k a b
 -- | Binary coproduct as a bifunctor.
 instance HasBinaryCoproducts k => Functor (CoproductFunctor k) where
+  type Dom (CoproductFunctor k) = k :**: k
+  type Cod (CoproductFunctor k) = k
+  type CoproductFunctor k :% (a, b) = BinaryCoproduct k a b
+
   CoproductFunctor % (a1 :**: a2) = a1 +++ a2
 
-data p :+: q where 
+data p :+: q where
   (:+:) :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryCoproducts k) => p -> q -> p :+: q
-type instance Dom (p :+: q) = Dom p
-type instance Cod (p :+: q) = Cod p
-type instance (p :+: q) :% a = BinaryCoproduct (Cod p) (p :% a) (q :% a)
 -- | The coproduct of two functors, passing the same object to both functors and taking the coproduct of the results.
 instance (Category (Dom p), Category (Cod p)) => Functor (p :+: q) where
-  (p :+: q) % f = (p % f) +++ (q % f)
+  type Dom (p :+: q) = Dom p
+  type Cod (p :+: q) = Cod p
+  type (p :+: q) :% a = BinaryCoproduct (Cod p) (p :% a) (q :% a)
 
-type instance BinaryCoproduct (Nat c d) x y = x :+: y
+  (p :+: q) % f = (p % f) +++ (q % f)
 
 -- | The functor coproduct ':+:' is the binary coproduct in functor categories.
 instance (Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d) where
+  type BinaryCoproduct (Nat c d) x y = x :+: y
   
   inj1 (Nat f _ _) (Nat g _ _) = Nat f (f :+: g) (\z -> inj1 (f % z) (g % z))
   inj2 (Nat f _ _) (Nat g _ _) = Nat g (f :+: g) (\z -> inj2 (f % z) (g % z))
@@ -598,17 +572,19 @@
   initialObject = Op terminalObject
   initialize (Op f) = Op (terminate f)
 
-type instance BinaryProduct (Op k) x y = BinaryCoproduct k x y
 -- | Binary products are the dual of binary coproducts.
 instance HasBinaryCoproducts k => HasBinaryProducts (Op k) where
+  type BinaryProduct (Op k) x y = BinaryCoproduct k x y
+
   proj1 (Op x) (Op y) = Op (inj1 x y)
   proj2 (Op x) (Op y) = Op (inj2 x y)
   Op f &&& Op g = Op (f ||| g)
   Op f *** Op g = Op (f +++ g)
 
-type instance BinaryCoproduct (Op k) x y = BinaryProduct k x y
 -- | Binary products are the dual of binary coproducts.
 instance HasBinaryProducts k => HasBinaryCoproducts (Op k) where
+  type BinaryCoproduct (Op k) x y = BinaryProduct k x y
+
   inj1 (Op x) (Op y) = Op (proj1 x y)
   inj2 (Op x) (Op y) = Op (proj2 x y)
   Op f ||| Op g = Op (f &&& g)
diff --git a/Data/Category/NNO.hs b/Data/Category/NNO.hs
--- a/Data/Category/NNO.hs
+++ b/Data/Category/NNO.hs
@@ -53,10 +53,10 @@
   primRec (CatA z) (CatA s) = CatA (PrimRec z s)
   
 data PrimRec z s = PrimRec z s
-type instance Dom (PrimRec z s) = Nat
-type instance Cod (PrimRec z s) = Cod z
-type instance PrimRec z s :% I1 () = z :% ()
-type instance PrimRec z s :% I2 n  = s :% PrimRec z s :% n
 instance (Functor z, Functor s, Dom z ~ Unit, Cod z ~ Dom s, Dom s ~ Cod s) => Functor (PrimRec z s) where
+  type Dom (PrimRec z s) = Nat
+  type Cod (PrimRec z s) = Cod z
+  type PrimRec z s :% I1 () = z :% ()
+  type PrimRec z s :% I2 n  = s :% PrimRec z s :% n
   PrimRec z s % Fix (I1 Unit) = z % Unit
   PrimRec z s % Fix (I2 n) = s % PrimRec z s % n
diff --git a/Data/Category/NaturalTransformation.hs b/Data/Category/NaturalTransformation.hs
--- a/Data/Category/NaturalTransformation.hs
+++ b/Data/Category/NaturalTransformation.hs
@@ -53,10 +53,10 @@
 -- | @f :~> g@ is a natural transformation from functor f to functor g.
 type f :~> g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g
 
--- | Natural transformations are built up of components, 
+-- | Natural transformations are built up of components,
 -- one for each object @z@ in the domain category of @f@ and @g@.
 data Nat :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where
-  Nat :: (Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) 
+  Nat :: (Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g)
     => f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
 
 
@@ -99,11 +99,11 @@
   Nat _ h ngh . Nat f _ nfg = Nat f h (\i -> ngh i . nfg i)
 
 
-compAssoc :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) 
+compAssoc :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h)
           => f -> g -> h -> Nat (Dom h) (Cod f) ((f :.: g) :.: h) (f :.: (g :.: h))
 compAssoc f g h = Nat ((f :.: g) :.: h) (f :.: (g :.: h)) (\i -> f % g % h % i)
 
-compAssocInv :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) 
+compAssocInv :: (Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h)
              => f -> g -> h -> Nat (Dom h) (Cod f) (f :.: (g :.: h)) ((f :.: g) :.: h)
 compAssocInv f g h = Nat (f :.: (g :.: h)) ((f :.: g) :.: h) (\i -> f % g % h % i)
 
@@ -140,48 +140,48 @@
 
 data FunctorCompose (k :: * -> * -> *) = FunctorCompose
 
-type instance Dom (FunctorCompose k) = Endo k :**: Endo k
-type instance Cod (FunctorCompose k) = Endo k
-type instance FunctorCompose k :% (f, g) = f :.: g
-
 -- | 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
+  
   FunctorCompose % (n1 :**: n2) = n1 `o` n2
 
 
 data Precompose :: * -> (* -> * -> *) -> * where
   Precompose :: f -> Precompose f d
 
-type instance Dom (Precompose f d) = Nat (Cod f) d
-type instance Cod (Precompose f d) = Nat (Dom f) d
-type instance Precompose f d :% g = g :.: f
-
--- | @Precompose f d@ is the functor such that @Precompose f d :% g = g :.: f@, 
+-- | @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
 
 
 data Postcompose :: * -> (* -> * -> *) -> * where
   Postcompose :: f -> Postcompose f c
 
-type instance Dom (Postcompose f c) = Nat c (Dom f)
-type instance Cod (Postcompose f c) = Nat c (Cod f)
-type instance Postcompose f c :% g = f :.: g
-
--- | @Postcompose f c@ is the functor such that @Postcompose f c :% g = f :.: g@, 
+-- | @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
 
 
 data Wrap f h = Wrap f h
 
-type instance Dom (Wrap f h) = Nat (Cod h) (Dom f)
-type instance Cod (Wrap f h) = Nat (Dom h) (Cod f)
-type instance Wrap f h :% g = f :.: g :.: h
-
--- | @Wrap f h@ is the functor such that @Wrap f h :% g = f :.: g :.: h@, 
+-- | @Wrap f h@ is the functor such that @Wrap f h :% g = f :.: g :.: h@,
 --   for functors @g@ that compose with @f@ and @h@.
 instance (Functor f, Functor h) => Functor (Wrap f h) where
+  type Dom (Wrap f h) = Nat (Cod h) (Dom f)
+  type Cod (Wrap f h) = Nat (Dom h) (Cod f)
+  type Wrap f h :% g = f :.: g :.: h
+  
   Wrap f h % n = natId f `o` n `o` natId h
diff --git a/Data/Category/Presheaf.hs b/Data/Category/Presheaf.hs
--- a/Data/Category/Presheaf.hs
+++ b/Data/Category/Presheaf.hs
@@ -20,7 +20,7 @@
 
 type Presheaves k = Nat (Op k) (->)
 
-type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite 
+type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite
   (   ProductFunctor (Presheaves k)
   :.: Tuple2 (Presheaves k) (Presheaves k) y
   :.: YonedaEmbedding k
@@ -28,10 +28,9 @@
 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)
 
-type instance Exponential (Presheaves k) y z = PShExponential k y z
-
 -- | The category of presheaves on a category @C@ is cartesian closed for any @C@.
 instance Category k => CartesianClosed (Presheaves k) where
+  type Exponential (Presheaves k) y z = PShExponential k y z
   
   apply yn@(Nat y _ _) zn@(Nat z _ _) = Nat (pshExponential yn zn :*: y) z (\(Op i) (n, yi) -> (n ! Op i) (i, yi))
   tuple yn zn@(Nat z _ _) = Nat z (pshExponential yn (zn *** yn)) (\(Op i) zi -> (Nat (hom_X i) z (\_ j2i -> (z % Op j2i) zi) *** yn))
diff --git a/Data/Category/Simplex.hs b/Data/Category/Simplex.hs
--- a/Data/Category/Simplex.hs
+++ b/Data/Category/Simplex.hs
@@ -55,7 +55,7 @@
 
 suc :: Obj Simplex n -> Obj Simplex (S n)
 suc = X . Y
--- Note: Objects are represented by their identity arrows, 
+-- Note: Objects are represented by their identity arrows,
 -- which are in the shape of the elements of `iterate suc Z`.
 
 -- | The (augmented) simplex category is the category of finite ordinals and order preserving maps.
@@ -96,10 +96,6 @@
 
 
 type Merge m n = BinaryCoproduct Simplex m n
-type instance BinaryCoproduct Simplex  Z       Z  = Z
-type instance BinaryCoproduct Simplex  Z    (S n) = S (Merge Z n)
-type instance BinaryCoproduct Simplex (S m)    Z  = S (Merge m Z)
-type instance BinaryCoproduct Simplex (S m) (S n) = S (S (Merge m n))
 
 mergeLS :: Obj Simplex m -> Obj Simplex n -> Simplex (Merge (S m) n) (S (Merge m n))
 mergeLS Z Z = X (Y Z)
@@ -115,6 +111,11 @@
 
 -- | 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))
@@ -137,11 +138,11 @@
   Fs :: Fin n -> Fin (S n)
 
 data Forget = Forget
-type instance Dom Forget = Simplex
-type instance Cod Forget = (->)
-type instance Forget :% n = Fin n
 -- | Turn @Simplex x y@ arrows into @Fin x -> Fin y@ functions.
-instance Functor Forget where 
+instance Functor Forget where
+  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
@@ -150,12 +151,12 @@
 
 
 data Add = Add
-type instance Dom Add = Simplex :**: Simplex
-type instance Cod Add = Simplex
-type instance Add :% (Z  , n) = n
-type instance Add :% (S m, n) = S (Add :% (m, n))
 -- | Ordinal addition is a bifuntor, it concattenates the maps as it were.
 instance Functor Add where
+  type Dom Add = Simplex :**: Simplex
+  type Cod Add = Simplex
+  type Add :% (Z  , n) = n
+  type Add :% (S m, n) = S (Add :% (m, n))
   Add % (Z   :**: g) = g
   Add % (Y f :**: g) = Y (Add % (f :**: g))
   Add % (X f :**: g) = X (Add % (f :**: g))
@@ -184,16 +185,16 @@
 universalMonoid = MonoidObject { unit = Y Z, multiply = X (X (Y Z)) }
 
 data Replicate f a = Replicate f (MonoidObject f a)
-type instance Dom (Replicate f a) = Simplex
-type instance Cod (Replicate f a) = Cod f
-type instance Replicate f a :% Z = Unit f
-type instance Replicate f a :% S n = f :% (a, Replicate f a :% n)
 -- | Replicate a monoid a number of times.
 instance TensorProduct f => Functor (Replicate f a) where
+  type Dom (Replicate f a) = Simplex
+  type Cod (Replicate f a) = Cod f
+  type Replicate f a :% Z = Unit f
+  type Replicate f a :% S n = f :% (a, Replicate f a :% n)
   Replicate f _ % Z = unitObject f
   Replicate f m % Y n = f % (unit m :**: tgt n') . leftUnitorInv f (tgt n') . n' where n' = Replicate f m % n
   Replicate f m % X (Y n) = f % (tgt (unit m) :**: (Replicate f m % n))
-  Replicate f m % X (X n) = n' . (f % (multiply m :**: b)) . associatorInv f a a b 
+  Replicate f m % X (X n) = n' . (f % (multiply m :**: b)) . associatorInv f a a b
     where
       n' = Replicate f m % X n
       a = tgt (unit m)
diff --git a/Data/Category/Void.hs b/Data/Category/Void.hs
--- a/Data/Category/Void.hs
+++ b/Data/Category/Void.hs
@@ -35,8 +35,9 @@
 
 
 data Magic (k :: * -> * -> *) = Magic
-type instance Dom (Magic k) = Void
-type instance Cod (Magic k) = k
 -- | Since there is nothing to map in `Void`, there's a functor from it to any other category.
 instance Category k => Functor (Magic k) where
+  type Dom (Magic k) = Void
+  type Cod (Magic k) = k
+
   Magic % f = magic f
diff --git a/Data/Category/Yoneda.hs b/Data/Category/Yoneda.hs
--- a/Data/Category/Yoneda.hs
+++ b/Data/Category/Yoneda.hs
@@ -15,7 +15,7 @@
 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) :.: ToTuple2 k (Op k)
 
 -- | The Yoneda embedding functor, @C -> Set^(C^op)@.
 yonedaEmbedding :: Category k => YonedaEmbedding k
@@ -23,11 +23,11 @@
 
 
 data Yoneda (k :: * -> * -> *) f = Yoneda
-type instance Dom (Yoneda k f) = Op k
-type instance Cod (Yoneda k f) = (->)
-type instance Yoneda k f :% a = Nat (Op k) (->) (k :-*: a) f
 -- | 'Yoneda' converts a functor @f@ into a natural transformation from the hom functor to f.
 instance (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => Functor (Yoneda k f) where
+  type Dom (Yoneda k f) = Op k
+  type Cod (Yoneda k f) = (->)
+  type Yoneda k f :% a = Nat (Op k) (->) (k :-*: a) f
   Yoneda % Op ab = \n -> n . yonedaEmbedding % ab
       
   
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.0
+version:             0.5.1
 synopsis:            Category theory
 
 description:         Data-category is a collection of categories, and some categorical constructions on them.
@@ -27,7 +27,7 @@
 cabal-version:       >= 1.10
 
 Library
-  exposed-modules:     
+  exposed-modules:
     Data.Category,
     Data.Category.Functor,
     Data.Category.NaturalTransformation,