diff --git a/src/Control/Category/Tensor.hs b/src/Control/Category/Tensor.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Category/Tensor.hs
@@ -0,0 +1,23 @@
+module Control.Category.Tensor where
+{
+    import Data.Semigroupoid.Dual;
+
+    -- could use data-lens:Control.Category.Product(Tensor)
+    class Tensor cc where
+    {
+        tensorUnit :: cc () ();
+        tensorPair :: cc a1 b1 -> cc a2 b2 -> cc (a1,a2) (b1,b2);
+    };
+
+    instance Tensor (->) where
+    {
+        tensorUnit = id;
+        tensorPair ab1 ab2 (a1,a2) = (ab1 a1,ab2 a2);
+    };
+
+    instance (Tensor cc) => Tensor (Dual cc) where
+    {
+        tensorUnit = Dual tensorUnit;
+        tensorPair (Dual ab1) (Dual ab2) = Dual (tensorPair ab1 ab2);
+    };
+}
diff --git a/src/Data/Nat.hs b/src/Data/Nat.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Nat.hs
@@ -0,0 +1,19 @@
+module Data.Nat where
+{
+    data Nat = Zero | Succ Nat;
+
+    addNat :: Nat -> Nat -> Nat;
+    addNat Zero b = b;
+    addNat (Succ a) b = Succ $ addNat a b;
+
+    -- | subtractFromNat a b = b - a
+    ;
+    subtractFromNat :: Nat -> Nat -> Maybe Nat;
+    subtractFromNat Zero b = Just b;
+    subtractFromNat (Succ a) (Succ b) = subtractFromNat a b;
+    subtractFromNat (Succ _) Zero = Nothing;
+
+    multiplyNat :: Nat -> Nat -> Nat;
+    multiplyNat Zero _ = Zero;
+    multiplyNat (Succ a) b = addNat (multiplyNat a b) b;
+}
diff --git a/src/Data/Witness/List.hs b/src/Data/Witness/List.hs
--- a/src/Data/Witness/List.hs
+++ b/src/Data/Witness/List.hs
@@ -1,13 +1,14 @@
+{-# OPTIONS -fno-warn-overlapping-patterns #-}
 module Data.Witness.List where
 {
     import Prelude hiding (id,(.));
     import Data.Witness.Representative;
     import Data.Type.Equality;
-    import Control.Category.Dual;
     import Data.Constraint(Dict(..));
     import Control.Applicative;
     import Control.Category;
     import Data.Functor.Identity as Import;
+    import Control.Category.Tensor;
 
     -- | a witness type for HList-style lists.
     -- The @w@ parameter is the witness type of the elements.
@@ -199,25 +200,6 @@
                 }
             };
         };
-    };
-
-    -- could use data-lens:Control.Category.Product(Tensor)
-    class Tensor cc where
-    {
-        tensorUnit :: cc () ();
-        tensorPair :: cc a1 b1 -> cc a2 b2 -> cc (a1,a2) (b1,b2);
-    };
-
-    instance Tensor (->) where
-    {
-        tensorUnit = id;
-        tensorPair ab1 ab2 (a1,a2) = (ab1 a1,ab2 a2);
-    };
-
-    instance (Tensor cc) => Tensor (Dual cc) where
-    {
-        tensorUnit = Dual tensorUnit;
-        tensorPair (Dual ab1) (Dual ab2) = Dual (tensorPair ab1 ab2);
     };
 
     type MapWitness cc w1 w2 = forall r v1. w1 v1 -> (forall v2. w2 v2 -> (cc v1 v2) -> r) -> r;
diff --git a/src/Data/Witness/ListElement.hs b/src/Data/Witness/ListElement.hs
--- a/src/Data/Witness/ListElement.hs
+++ b/src/Data/Witness/ListElement.hs
@@ -1,15 +1,16 @@
 module Data.Witness.ListElement where
 {
+    import Data.Nat;
     import Data.Witness.Nat;
 
-    class HasListElement (n :: NatKind) (list :: *) where
+    class HasListElement (n :: Nat) (list :: *) where
     {
         type ListElement n list :: *;
-        getListElement :: Nat n -> list -> ListElement n list;
-        putListElement :: Nat n -> ListElement n list -> list -> list;
+        getListElement :: NatType n -> list -> ListElement n list;
+        putListElement :: NatType n -> ListElement n list -> list -> list;
     };
 
-    modifyListElement :: (HasListElement n t) => Nat n -> (ListElement n t -> ListElement n t) -> t -> t;
+    modifyListElement :: (HasListElement n t) => NatType n -> (ListElement n t -> ListElement n t) -> t -> t;
     modifyListElement n aa t = putListElement n (aa (getListElement n t)) t;
 
     instance HasListElement 'Zero (a,r) where
@@ -22,7 +23,7 @@
     instance (HasListElement n r) => HasListElement ('Succ n) (a,r) where
     {
         type ListElement ('Succ n) (a,r) = ListElement n r;
-        getListElement (SuccNat n) (_,r) = getListElement n r;
-        putListElement (SuccNat n) a (f,r) = (f,putListElement n a r);
+        getListElement (SuccType n) (_,r) = getListElement n r;
+        putListElement (SuccType n) a (f,r) = (f,putListElement n a r);
     };
 }
diff --git a/src/Data/Witness/Nat.hs b/src/Data/Witness/Nat.hs
--- a/src/Data/Witness/Nat.hs
+++ b/src/Data/Witness/Nat.hs
@@ -4,20 +4,19 @@
     import Data.Maybe;
     import Data.Type.Equality;
     import Data.Constraint(Dict(..));
+    import Data.Nat;
     import Data.Witness.Representative;
 
-    data NatKind = Zero | Succ NatKind;
-
-    data Nat (t :: NatKind) where
+    data NatType (t :: Nat) where
     {
-        ZeroNat :: Nat 'Zero;
-        SuccNat :: Nat t -> Nat ('Succ t);
+        ZeroType :: NatType 'Zero;
+        SuccType :: NatType t -> NatType ('Succ t);
     };
 
-    instance TestEquality Nat where
+    instance TestEquality NatType where
     {
-        testEquality ZeroNat ZeroNat = return Refl;
-        testEquality (SuccNat a) (SuccNat b) = do
+        testEquality ZeroType ZeroType = return Refl;
+        testEquality (SuccType a) (SuccType b) = do
         {
             Refl <- testEquality a b;
             return Refl;
@@ -25,27 +24,27 @@
         testEquality _ _ = Nothing;
     };
 
-    instance Eq1 Nat where
+    instance Eq1 NatType where
     {
         equals1 a b = isJust (testEquality a b);
     };
 
-    instance Representative Nat where
+    instance Representative NatType where
     {
-        getRepWitness ZeroNat = Dict;
-        getRepWitness (SuccNat n) = case getRepWitness n of
+        getRepWitness ZeroType = Dict;
+        getRepWitness (SuccType n) = case getRepWitness n of
         {
             Dict -> Dict;
         };
     };
 
-    instance Is Nat 'Zero where
+    instance Is NatType 'Zero where
     {
-        representative = ZeroNat;
+        representative = ZeroType;
     };
 
-    instance (Is Nat n) => Is Nat ('Succ n) where
+    instance (Is NatType n) => Is NatType ('Succ n) where
     {
-        representative = SuccNat representative;
+        representative = SuccType representative;
     };
 }
diff --git a/src/Data/Witness/WitnessDict.hs b/src/Data/Witness/WitnessDict.hs
--- a/src/Data/Witness/WitnessDict.hs
+++ b/src/Data/Witness/WitnessDict.hs
@@ -58,6 +58,6 @@
 
     -- | Create a dictionary from a list of witness\/value pairs
     ;
-    witnessDictFromList :: (TestEquality w) => [Any w] -> WitnessDict w;
+    witnessDictFromList :: [Any w] -> WitnessDict w;
     witnessDictFromList = MkWitnessDict;
 }
diff --git a/src/Data/Witness/WitnessFDict.hs b/src/Data/Witness/WitnessFDict.hs
--- a/src/Data/Witness/WitnessFDict.hs
+++ b/src/Data/Witness/WitnessFDict.hs
@@ -58,6 +58,6 @@
 
     -- | Create a dictionary from a list of witness\/value pairs
     ;
-    witnessFDictFromList :: (TestEquality w) => [AnyF w f] -> WitnessFDict w f;
+    witnessFDictFromList :: [AnyF w f] -> WitnessFDict w f;
     witnessFDictFromList = MkWitnessFDict;
 }
diff --git a/witness.cabal b/witness.cabal
--- a/witness.cabal
+++ b/witness.cabal
@@ -1,6 +1,6 @@
 cabal-version:  >=1.14
 name:           witness
-version:        0.3.0.1
+version:        0.4
 x-follows-version-policy:
 license:        BSD3
 license-file:   LICENSE
@@ -35,12 +35,15 @@
         DataKinds
         ScopedTypeVariables
         PatternGuards
+        PatternSynonyms
     build-depends:
         base >= 4.7 && < 5,
         transformers,
-        categories,
+        semigroupoids,
         constraints
     exposed-modules:
+        Data.Nat
+        Control.Category.Tensor
         Data.Witness.Any
         Data.Witness.WitnessDict
         Data.Witness.WitnessFDict