diff --git a/Data/TypeNat/Fin.hs b/Data/TypeNat/Fin.hs
--- a/Data/TypeNat/Fin.hs
+++ b/Data/TypeNat/Fin.hs
@@ -18,6 +18,7 @@
   , ix10
 
   , safeIndex
+  , safeUpdate
 
   , module Data.TypeNat.Nat
 
@@ -43,6 +44,11 @@
 ix10 = FS ix9
 
 -- | Safely index a Vect.
-safeIndex :: Vect a n -> Fin n -> a
-safeIndex (VCons a _) FZ = a
-safeIndex (VCons _ v) (FS x) = safeIndex v x
+safeIndex :: Fin n -> Vect n a -> a
+safeIndex FZ (VCons a _) = a
+safeIndex (FS x) (VCons _ v) = safeIndex x v
+
+-- | Safely update a Vect.
+safeUpdate :: Fin n -> (a -> a) -> Vect n a -> Vect n a
+safeUpdate FZ f (VCons x rest) = VCons (f x) rest
+safeUpdate (FS fs) f (VCons x rest) = VCons x (safeUpdate fs f rest)
diff --git a/Data/TypeNat/Nat.hs b/Data/TypeNat/Nat.hs
--- a/Data/TypeNat/Nat.hs
+++ b/Data/TypeNat/Nat.hs
@@ -34,6 +34,7 @@
 import Data.Proxy
 import GHC.Exts (Constraint)
 
+-- | Natural numbers
 data Nat = Z | S Nat
 
 instance Eq Nat where
diff --git a/Data/TypeNat/Vect.hs b/Data/TypeNat/Vect.hs
--- a/Data/TypeNat/Vect.hs
+++ b/Data/TypeNat/Vect.hs
@@ -20,43 +20,57 @@
 import Data.TypeNat.Nat
 
 -- | Nat-indexed list, where the nat determines the length.
-data Vect :: * -> Nat -> * where
-  VNil :: Vect a Z
-  VCons :: a -> Vect a n -> Vect a (S n)
+data Vect :: Nat -> * -> * where
+  VNil :: Vect Z a
+  VCons :: a -> Vect n a -> Vect (S n) a
 
-deriving instance Eq t => Eq (Vect t n)
-deriving instance Show t => Show (Vect t n)
+deriving instance Eq a => Eq (Vect n a)
+deriving instance Show a => Show (Vect n a)
 
+instance Functor (Vect n) where
+    fmap = vectMap
+
+instance Foldable (Vect n) where
+    foldr f b vect = case vect of
+        VNil -> b
+        VCons x rest -> f x (foldr f b rest)
+
+instance Traversable (Vect n) where
+    traverse f vect = case vect of
+        VNil -> pure VNil
+        VCons x rest -> VCons <$> f x <*> traverse f rest
+
 -- | A kind of fmap for Vect.
-vectMap :: (a -> b) -> Vect a n -> Vect b n
+vectMap :: (a -> b) -> Vect n a -> Vect n b
 vectMap f vect = case vect of
   VNil -> VNil
   VCons x v -> VCons (f x) (vectMap f v)
 
 -- | VCons to the end of a Vect.
-vectSnoc :: a -> Vect a n -> Vect a (S n)
+vectSnoc :: a -> Vect n a -> Vect (S n) a
 vectSnoc x vect = case vect of
   VNil -> VCons x VNil
   VCons y v -> VCons y (vectSnoc x v)
 
-showVect :: Show a => Vect a l -> String
+-- | Show a Vect.
+showVect :: Show a => Vect l a -> String
 showVect VNil = "VNil"
 showVect (VCons x xs) = show x ++ " , " ++ showVect xs
 
 -- | Drop the length index from a Vect, giving a typical list.
-vectToList :: Vect a n -> [a]
+vectToList :: Vect n a -> [a]
 vectToList v = case v of
   VNil -> []
   VCons x xs -> x : vectToList xs
 
 -- | Used to implement listToVect through natRecursion.
 newtype MaybeVect a n = MV {
-    unMV :: Maybe (Vect a n)
+    unMV :: Maybe (Vect n a)
   }
 
 -- | Try to produce a Vect from a list. The nat index must be fixed somehow,
 --   perhaps with the help of ScopedTypeVariables.
-listToVect:: IsNat n => [a] -> Maybe (Vect a n)
+listToVect:: IsNat n => [a] -> Maybe (Vect n a)
 listToVect = unMV . listToVect'
 
   where
diff --git a/TypeNat.cabal b/TypeNat.cabal
--- a/TypeNat.cabal
+++ b/TypeNat.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                TypeNat
-version:             0.4.0.1
+version:             0.5.0.0
 synopsis:            Some Nat-indexed types for GHC
 -- description:         
 homepage:            https://github.com/avieth/TypeNat
@@ -31,6 +31,6 @@
                      , TypeFamilies
                      , KindSignatures
 
-  build-depends:       base >=4.7 && < 4.9
+  build-depends:       base >=4.7 && < 4.11
   -- hs-source-dirs:      
   default-language:    Haskell2010