diff --git a/src/TypeUnary/Nat.hs b/src/TypeUnary/Nat.hs
--- a/src/TypeUnary/Nat.hs
+++ b/src/TypeUnary/Nat.hs
@@ -36,7 +36,7 @@
 
 import TypeUnary.TyNat
 
--- Natural numbers
+-- Natural numbers in unary form, built from zero & successor
 data Nat :: * -> * where
   Zero :: Nat Z
   Succ :: IsNat n => Nat n -> Nat (S n)
@@ -117,6 +117,9 @@
 
 -- | A number under the given limit, with proof
 data Index lim = forall n. IsNat n => Index (n :<: lim) (Nat n)
+
+-- TODO: Consider removing the Nat n field, since it's computable from
+-- IsNat n or n :<: lim.
 
 instance Eq (Index lim) where
   Index _ n == Index _ n' = isJust (n `natEq` n')
diff --git a/src/TypeUnary/Vec.hs b/src/TypeUnary/Vec.hs
--- a/src/TypeUnary/Vec.hs
+++ b/src/TypeUnary/Vec.hs
@@ -38,6 +38,7 @@
 
 -- #include "Typeable.h"
 
+import Data.Monoid (Monoid(..))
 import Control.Applicative (Applicative(..),liftA2,(<$>))
 import Data.Foldable (Foldable(..),toList,sum)
 import Data.Traversable (Traversable(..))
@@ -59,8 +60,8 @@
 -- | Vectors with type-determined length, having empty vector ('ZVec') and
 -- vector cons ('(:<)').
 data Vec :: * -> * -> * where
-  ZVec :: Vec Z a                       -- -- ^ zero vector
-  (:<) :: a -> Vec n a -> Vec (S n) a   -- -- ^ vector cons
+  ZVec :: Vec Z a 
+  (:<) :: a -> Vec n a -> Vec (S n) a
 
 -- | Type-safe head for vectors
 headV :: Vec (S n) a -> a
@@ -121,6 +122,11 @@
 -- do: check whether this change broke Shady's code generation. Maybe not,
 -- if the code generation uses Pretty instead of Show.
 
+-- The Monoid instance uses a standard recipe for applicative functors.
+instance (IsNat n, Monoid a) => Monoid (Vec n a) where
+  mempty  = pure mempty
+  mappend = liftA2 mappend
+
 instance Functor (Vec n) where
   fmap _ ZVec     = ZVec
   fmap f (a :< u) = f a :< fmap f u
@@ -167,6 +173,7 @@
   traverse _ ZVec      = pure ZVec
   traverse f (a :< as) = liftA2 (:<) (f a) (traverse f as)
 
+
 instance (IsNat n, Num a) => AdditiveGroup (Vec n a) where
   { zeroV = pure 0; (^+^) = liftA2 (+) ; negateV = fmap negate }
 
@@ -178,6 +185,10 @@
    -- u <.> v = vec1 (sum (liftA2 (*) u v))
    (<.>) = (result.result) (vec1 . sum) (liftA2 (*))
 
+-- TODO: Rethink the previous three instances. Maybe replace the Num
+-- constraints with AdditiveGroup, VectorSpace, and InnerSpace.
+-- And why Vec1 for Scalar?
+
 instance (IsNat n, Storable a) => Storable (Vec n a) where
    sizeOf    = const (fromIntegral (natToZ (nat :: Nat n))
                       * sizeOf (undefined :: a))
@@ -294,6 +305,16 @@
 -- | Extract elements
 un4 :: Vec4 a -> (a,a,a,a)
 un4 (a :< b :< c :< d :< ZVec) = (a,b,c,d)
+
+-- TODO: consider this notation:
+--
+--   infixr 5 :<
+--   (<|) :: a -> a -> Vec2 a
+--   (<|) = vec2
+-- 
+-- So we can say things like
+-- 
+--   a :< b <| c
 
 {--------------------------------------------------------------------
     Extract and set elements
diff --git a/type-unary.cabal b/type-unary.cabal
--- a/type-unary.cabal
+++ b/type-unary.cabal
@@ -1,5 +1,5 @@
 Name:                type-unary
-Version:             0.1.12
+Version:             0.1.13
 Cabal-Version:       >= 1.2
 Synopsis:            
   Type-level and typed unary natural numbers, inequality proofs, vectors