diff --git a/src/TypeUnary/Vec.hs b/src/TypeUnary/Vec.hs
--- a/src/TypeUnary/Vec.hs
+++ b/src/TypeUnary/Vec.hs
@@ -35,8 +35,8 @@
   , Vec10,Vec11,Vec12,Vec13,Vec14,Vec15,Vec16
   , vec1, vec2, vec3, vec4
   , un1, un2, un3, un4
-  , get0, get1, get2, get3
-  , get, swizzle, split
+  , get, get0, get1, get2, get3
+  , swizzle, split
   , ToVec(..)
   ) where
 
@@ -190,16 +190,16 @@
 succI :: Index m -> Index (S m)
 succI (Index p n) = Index (SLess p) (Succ n)
 
-index0 :: Index (S m)
+index0 :: Index (N1 :+: m)
 index0 = Index ZLess Zero
 
-index1 :: Index (S (S m))
+index1 :: Index (N2 :+: m)
 index1 = succI index0
 
-index2 :: Index (S (S (S m)))
+index2 :: Index (N3 :+: m)
 index2 = succI index1
 
-index3 :: Index (S (S (S (S m))))
+index3 :: Index (N4 :+: m)
 index3 = succI index2
 
 
@@ -259,6 +259,11 @@
 instance Show a => Show (Vec n a) where
   show v = "elemsV " ++ show (toList v)
 
+-- 2011-10-26: There was an orphan Show Vec instance in shady-gen's
+-- Shady.Language.Type, which conflicted with the Show instance above. To
+-- do: check whether this change broke Shady's code generation. Maybe not,
+-- if the code generation uses Pretty instead of Show.
+
 instance Functor (Vec n) where
   fmap _ ZVec     = ZVec
   fmap f (a :< u) = f a :< fmap f u
@@ -431,15 +436,14 @@
 --------------------------------------------------------------------}
 
 -- | General indexing, taking a proof that the index is within bounds.
-get :: Index n -> Vec n a -> Vec1 a
-get (Index ZLess     Zero    ) (a :< _)  = vec1 a
+get :: Index n -> Vec n a -> a
+get (Index ZLess     Zero    ) (a :< _)  = a
 get (Index (SLess p) (Succ m)) (_ :< as) = get (Index p m) as
 
-
-get0 :: Vec (S n)             a -> Vec1 a
-get1 :: Vec (S (S n))         a -> Vec1 a
-get2 :: Vec (S (S (S n)))     a -> Vec1 a
-get3 :: Vec (S (S (S (S n)))) a -> Vec1 a
+get0 :: Vec (N1 :+: n) a -> a   -- ^ Get first  element
+get1 :: Vec (N2 :+: n) a -> a   -- ^ Get second element
+get2 :: Vec (N3 :+: n) a -> a   -- ^ Get third  element
+get3 :: Vec (N4 :+: n) a -> a   -- ^ Get fourth element
 
 get0 = get index0
 get1 = get index1
@@ -450,7 +454,7 @@
 -- | Swizzling.  Extract multiple elements simultaneously.
 swizzle :: Vec n (Index m) -> Vec m a -> Vec n a
 swizzle ZVec        _ = ZVec
-swizzle (ix :< ixs) v = un1 (get ix v) :< swizzle ixs v
+swizzle (ix :< ixs) v = get ix v :< swizzle ixs v
 
 {-
 -- 'a' :< 'b' :< 'c' :< ZVec
@@ -496,6 +500,26 @@
 --                TypeUnary.Vec.take :: IsNat n => Vec (n :+: m) a -> Vec n a
 --     at /Users/conal/Haskell/type-unary/src/TypeUnary/Vec.hs:488:1-18
 --   NB: `:+:' is a type function, and may not be injective
+
+{-
+
+-- Reversal. Thinking about this one. Currently thwarted by missing
+-- knowledge about numbers in the type-checker. Would be easy with
+-- built-in type-level naturals.
+
+-- | Reverse a vector
+reverseV :: Vec n a -> Vec n a
+reverseV = reverse' nat ZVec
+
+--  Couldn't match type `n' with `n :+: Z'
+
+-- Reverse na and append to ma
+reverse' :: Nat n -> Vec m a -> Vec n a -> Vec (n :+: m) a
+reverse' Zero     ma ZVec      = ma
+reverse' (Succ n) ma (a :< as) = reverse' n (a :< ma) as
+
+-- Could not deduce ((n1 :+: S m) ~ S (n1 :+: m))
+-}
 
 {--------------------------------------------------------------------
     Conversion to vectors
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.2
+Version:             0.1.3
 Cabal-Version:       >= 1.2
 Synopsis:            
   Type-level and typed unary natural numbers, vectors, inequality proofs