diff --git a/src/TypeUnary/Nat.hs b/src/TypeUnary/Nat.hs
--- a/src/TypeUnary/Nat.hs
+++ b/src/TypeUnary/Nat.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE TypeOperators, GADTs, KindSignatures, RankNTypes #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# OPTIONS_GHC -Wall #-}
 ----------------------------------------------------------------------
 -- |
@@ -21,8 +22,10 @@
   , withIsNat, natSucc, natIsNat
   , natToZ, natEq, natAdd, natMul
   , IsNat(..)
+  , induction
   -- * Inequality proofs and indices
-  , (:<:)(..), Index(..), unIndex, succI, index0, index1, index2, index3
+  , (:<:)(..), succLim
+  , Index(..), unIndex, succI, index0, index1, index2, index3
   , coerceToIndex
   ) where
 
@@ -113,6 +116,23 @@
 -- and zero, ..., four, considering that all of them can be synthesized
 -- from IsNat.
 
+-- | Peano's induction principle
+induction :: forall p. 
+             p Z -> (forall n. IsNat n => p n -> p (S n))
+          -> (forall n. IsNat n => p n)
+induction z s = go nat
+ where
+   -- morphism over z & s.
+   go :: forall n. Nat n -> p n
+   go Zero     = z
+   go (Succ m) = s (go m)
+
+-- TODO: Use induction for n + Z == n. Then associativity and commutativity.
+
+{--------------------------------------------------------------------
+    Inequality proofs
+--------------------------------------------------------------------}
+
 infix 4 :<:
 
 -- | Proof that @m < n@
@@ -120,6 +140,77 @@
   ZLess :: Z :<: S n
   SLess :: m :<: n -> S m :<: S n
 
+-- | Increase the upper limit in an inequality proof
+succLim :: m :<: n -> m :<: S n
+succLim ZLess     = ZLess
+succLim (SLess p) = SLess (succLim p)
+
+-- Note: succLim is a morphism
+
+-- addLim :: forall p m n. IsNat p => 
+--           m :<: n -> m :<: (p :+: n)
+-- addLim = addLim' nat
+
+-- addLim' :: Nat p -> m :<: n -> m :<: (p :+: n)
+-- addLim' Zero mn = mn
+-- addLim' (Succ p') mn = bump p' (addLim' p' mn)
+
+
+-- addLim mn = case (nat :: Nat p) of
+--               Zero    -> mn
+--           --  Succ p' -> bump p' (addLim mn)
+--               -- Succ (p' :: Nat p') -> bump p' (addLim mn :: (m :<: p' :+: n))
+--               Succ (p' :: Nat p') -> undefined p' (addLim mn :: (m :<: p' :+: n))
+
+-- p :: S p'
+
+-- S p' + n = S (p' + n)
+
+--               Succ (p' :: Nat p') -> succLim (addLim mn :: (m :<: p' :+: n))
+
+-- bump :: Nat p
+--      -> (m :<:   (p :+: n))
+--      -> (m :<: S (p :+: n))
+-- bump = undefined
+
+-- addLim = case (nat :: Nat p) of
+--               Zero -> id
+--               Succ p' -> succLim . addLim
+
+-- p :: S p'
+-- p = Succ p'
+
+-- p + n == S (p' + n)
+
+-- mn :: m < n
+-- addLim mn :: m < p' + n
+-- succLim (addLim mn) :: m < S (p' + n)
+
+
+-- mn :: S m :<: S n
+-- mn = SLess mn'
+-- mn' :: m :<: n
+
+
+
+
+-- Z + n == n
+
+-- S p' + n == S (p' + n)
+
+-- mn :: S m < S n
+-- mn' :: m < n
+
+-- p :: S p'
+-- p' :: p'
+
+-- ... :: S m :<: (S p' :+: n)
+-- ... :: S m :<: S (p' :+: S n)
+
+-- addLim' :: forall p m n. IsNat p => 
+--            Nat p -> m :<: n -> m :<: (p :+: n)
+-- addLim' Zero = id
+
 -- | A number under the given limit, with proof
 data Index lim = forall n. IsNat n => Index (n :<: lim) (Nat n)
 
@@ -154,18 +245,36 @@
 
 -- | Index generation from integer. Can fail dynamically if the integer is
 -- too large.
-coerceToIndex :: (Show i, Integral i, IsNat m) => i -> Index m
+coerceToIndex :: (Show i, Num i, IsNat m) => i -> Index m
 coerceToIndex = coerceToIndex' nat
 
-coerceToIndex' :: (Show i, Integral i) => Nat m -> i -> Index m
+coerceToIndex' :: (Show i, Num i) => Nat m -> i -> Index m
 coerceToIndex' mOrig niOrig = loop mOrig niOrig
  where
-   loop :: (Show i, Integral i) => Nat m -> i -> Index m
+   loop :: (Show i, Num i) => Nat m -> i -> Index m
    loop Zero _        = error $ "coerceToIndex: out of bounds: "
                                 ++ show niOrig ++ " should be less than "
                                 ++ show mOrig
    loop (Succ _)   0  = Index ZLess Zero
    loop (Succ m') ni' = succI (loop m' (ni'-1))
+
+-- Experimental instances:
+
+instance Show (Index n) where
+  show (Index _ n) = show n
+
+instance IsNat n => Num (Index n) where
+  fromInteger = coerceToIndex
+  (+)    = noIndex "(+)"
+  (*)    = noIndex "(*)"
+  abs    = noIndex "abs"
+  signum = noIndex "signum"
+
+noIndex :: String -> a
+noIndex meth = error (meth ++ ": no method for Index n. Sorry.")
+
+-- TODO: Perhaps replace these noIndex uses with real definitions. However, it
+-- doesn't seem likely that we'd want to stay in Index n for the same n.
 
 {--------------------------------------------------------------------
     IsNat
diff --git a/src/TypeUnary/TyNat.hs b/src/TypeUnary/TyNat.hs
--- a/src/TypeUnary/TyNat.hs
+++ b/src/TypeUnary/TyNat.hs
@@ -16,7 +16,7 @@
 module TypeUnary.TyNat
   (
     -- * Type-level natural numbers
-    Z, S, (:+:), (:*:)
+    Z, S, (:+:), (:*:), (:-:)
   , N0,N1,N2,N3,N4,N5,N6,N7,N8,N9,N10,N11,N12,N13,N14,N15,N16
   ) where
 
@@ -45,6 +45,13 @@
 type instance Z   :*: b = Z
 type instance S a :*: b = b :+: (a :*: b)
 
+infixl 6 :-:
+
+-- Experiment:
+type family a :-: b
+
+type instance   n :-:   Z = n
+type instance S n :-: S m = n :-: m
 
 -- Generated code
 -- 
diff --git a/src/TypeUnary/Vec.hs b/src/TypeUnary/Vec.hs
--- a/src/TypeUnary/Vec.hs
+++ b/src/TypeUnary/Vec.hs
@@ -32,19 +32,21 @@
   , update
   , set, set0, set1, set2, set3
   , getI, setI
-  , flattenV, swizzle, split, deleteV, elemsV, unzipV
+  , flattenV, swizzle, split, deleteV, elemsV
+  , zipV , zipWithV , unzipV
+  , zipV3, zipWithV3, unzipV3
   , ToVec(..)
   ) where
 
   -- TODO: Consider dropping "V" suffix from several of the names.
 
-import Prelude hiding (foldr,sum)
+import Prelude hiding (foldr,sum,and)
 
 -- #include "Typeable.h"
 
 import Data.Monoid (Monoid(..))
 import Control.Applicative (Applicative(..),liftA2,(<$>))
-import Data.Foldable (Foldable(..),toList,sum)
+import Data.Foldable (Foldable(..),toList,sum) -- ,and
 import Data.Traversable (Traversable(..))
 -- import Data.Typeable
 
@@ -113,11 +115,27 @@
 instance Ord a => Ord (Vec n a) where
   ZVec      `compare` ZVec      = EQ
   (a :< as) `compare` (b :< bs) =
-    case a `compare` b of
-      LT -> LT
-      GT -> GT
-      EQ -> as `compare` bs
+    (a `compare` b) `mappend` (as `compare` bs)
 
+-- Equivalently,
+-- 
+--   (a :< as) `compare` (b :< bs) =
+--     case a `compare` b of
+--       LT -> LT
+--       GT -> GT
+--       EQ -> as `compare` bs
+
+-- Some alternatives:
+-- 
+--   (==*) :: (IsNat n, Eq a) => Vec n a -> Vec n a -> Bool
+--   (==*) = (fmap.fmap) and (liftA2 (==))
+--   
+--   -- as ==* bs = and (liftA2 (==) as bs)
+--   
+--   compare' :: (IsNat n, Ord a) => Vec n a -> Vec n a -> Ordering
+--   compare' = (fmap.fmap) fold (liftA2 compare)
+
+
 instance Show a => Show (Vec n a) where
   show v = "elemsV " ++ show (toList v)
 
@@ -320,7 +338,7 @@
 
 -- TODO: consider this notation:
 --
---   infixr 5 :<
+--   infixr 5 <|
 --   (<|) :: a -> a -> Vec2 a
 --   (<|) = vec2
 -- 
@@ -391,9 +409,13 @@
 
 -- | Swizzling.  Extract multiple elements simultaneously.
 swizzle :: Vec n (Index m) -> Vec m a -> Vec n a
-swizzle ZVec        _ = ZVec
-swizzle (ix :< ixs) v = get ix v :< swizzle ixs v
+swizzle is v = flip get v <$> is
 
+-- swizzle ZVec        _ = ZVec
+-- swizzle (ix :< ixs) v = get ix v :< swizzle ixs v
+
+-- swizzle = flip (fmap . flip get)
+
 -- | Split a vector
 split :: IsNat n => Vec (n :+: m) a -> (Vec n a, Vec m a)
 split = split' nat
@@ -425,8 +447,44 @@
 --     at /Users/conal/Haskell/type-unary/src/TypeUnary/Vec.hs:488:1-18
 --   NB: `:+:' is a type function, and may not be injective
 
+
+-- Alternatively:
+
 {-
+take :: forall m n a. (IsNat n, IsNat m) => Vec (n :+: m) a -> Vec n a
+take = take' (nat :: Nat n) (nat :: Nat m)
 
+take' :: Nat n -> Nat m -> Vec (n :+: m) a -> Vec n a
+take' Zero _ _             = ZVec
+take' (Succ n) m (a :< as) = a :< take' n m as
+-}
+
+-- I think it'd be hard to use take. I guess we'd have to subtract in the type
+-- system.
+
+{-
+
+take :: forall m n a. (IsNat n, IsNat m) =>
+        Vec (n :+: m) a -> (Vec n a,Nat m)
+take = take' (nat :: Nat n)
+
+take' :: Nat n -> Vec (n :+: m) a -> (Vec n a,Nat m)
+take' Zero as             = (ZVec,lengthV as)
+take' (Succ n) (a :< as) = (a :< as', m)
+ where
+   (as',m) = take' n as
+
+lengthV :: Vec n a -> Nat n
+lengthV ZVec      = Zero
+lengthV (a :< as) = Succ (lengthV as)
+
+--     Could not deduce (IsNat n1) arising from a use of `Succ'
+--     from the context (n ~ S n1)
+
+-}
+
+{-
+
 -- 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.
@@ -477,10 +535,39 @@
 t3 = swizzle t2 t1
 -}
 
--- | Unzip a list of pairs into a pair of lists
+-- | Zip two vectors into one. Like @'liftA2' '(,)'@, but the former requires
+-- @IsNat n@.
+zipV :: Vec n a -> Vec n b -> Vec n (a,b)
+zipV = zipWithV (,)
+
+-- | Zip three vectors into one. Like @'liftA3' '(,)'@, but the former requires
+-- @IsNat n@.
+zipV3 :: Vec n a -> Vec n b -> Vec n c -> Vec n (a,b,c)
+zipV3 = zipWithV3 (,,)
+
+-- | Unzip one vector into two. Like 'liftA2', but the former requires
+-- @IsNat n@.
+zipWithV :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
+zipWithV _ ZVec      ZVec      = ZVec
+zipWithV f (a :< as) (b :< bs) = f a b :< zipWithV f as bs
+
+-- | Unzip one vector into two. Like 'liftA2', but the former requires
+-- @IsNat n@.
+zipWithV3 :: (a -> b -> c -> d) -> Vec n a -> Vec n b -> Vec n c -> Vec n d
+zipWithV3 _ ZVec      ZVec      ZVec      = ZVec
+zipWithV3 f (a :< as) (b :< bs) (c :< cs) = f a b c :< zipWithV3 f as bs cs
+
+-- | Unzip a vector of pairs into a pair of vectors
 unzipV :: Vec n (a,b) -> (Vec n a, Vec n b)
 unzipV ZVec = (ZVec,ZVec)
 unzipV ((a,b) :< ps) = (a :< as, b :< bs) where (as,bs) = unzipV ps
+
+-- | Unzip a vector of pairs into a pair of vectors
+unzipV3 :: Vec n (a,b,c) -> (Vec n a, Vec n b, Vec n c)
+unzipV3 ZVec = (ZVec,ZVec,ZVec)
+unzipV3 ((a,b,c) :< ps) = (a :< as, b :< bs, c :< cs) 
+  where (as,bs,cs) = unzipV3 ps
+
 
 {--------------------------------------------------------------------
     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.2.1
+Version:             0.2.2
 Cabal-Version:       >= 1.2
 Synopsis:            
   Type-level and typed unary natural numbers, inequality proofs, vectors