diff --git a/Data/TypeNat/Fin.hs b/Data/TypeNat/Fin.hs
new file mode 100644
--- /dev/null
+++ b/Data/TypeNat/Fin.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE GADTs #-}
+
+module Data.TypeNat.Fin (
+
+    Fin(..)
+
+  , ix1
+  , ix2
+  , ix3
+  , ix4
+  , ix5
+  , ix6
+  , ix7
+  , ix8
+  , ix9
+  , ix10
+
+  , safeIndex
+
+  , module Data.TypeNat.Nat
+
+  ) where
+
+import Data.TypeNat.Nat
+import Data.TypeNat.Vect
+
+-- | Finite set datatype.
+data Fin :: Nat -> * where
+  FZ :: Fin (S n)
+  FS :: Fin k -> Fin (S k)
+
+ix1 = FZ
+ix2 = FS ix1
+ix3 = FS ix2
+ix4 = FS ix3
+ix5 = FS ix4
+ix6 = FS ix5
+ix7 = FS ix6
+ix8 = FS ix7
+ix9 = FS ix8
+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
diff --git a/Data/TypeNat/Nat.hs b/Data/TypeNat/Nat.hs
new file mode 100644
--- /dev/null
+++ b/Data/TypeNat/Nat.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE Rank2Types #-}
+
+module Data.TypeNat.Nat (
+
+    Nat(..)
+  , IsNat
+  , natRecursion
+
+  , One
+  , Two
+  , Three
+  , Four
+  , Five
+  , Six
+  , Seven
+  , Eight
+  , Nine
+  , Ten
+
+  ) where
+
+data Nat = Z | S Nat
+
+type One = S Z
+type Two = S One
+type Three = S Two
+type Four = S Three
+type Five = S Four
+type Six = S Five
+type Seven = S Six
+type Eight = S Seven
+type Nine = S Eight
+type Ten = S Nine
+
+-- | Proof that a given type is a Nat.
+--   With this fact, you can do type-directed computation.
+class IsNat (n :: Nat) where
+  natRecursion :: (forall m . b -> a m -> a (S m)) -> (b -> a Z) -> (b -> b) -> b -> a n
+
+instance IsNat Z where
+  natRecursion _ ifZ _ = ifZ
+
+instance IsNat n => IsNat (S n) where
+  natRecursion ifS ifZ reduce x = ifS x (natRecursion ifS ifZ reduce (reduce x))
diff --git a/Data/TypeNat/Vect.hs b/Data/TypeNat/Vect.hs
new file mode 100644
--- /dev/null
+++ b/Data/TypeNat/Vect.hs
@@ -0,0 +1,78 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE GADTs #-}
+
+module Data.TypeNat.Vect (
+
+    Vect(..)
+
+  , vectMap
+  , vectSnoc
+  , vectToList
+  , listToVect
+  , showVect
+
+  , module Data.TypeNat.Nat
+
+  ) where
+
+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)
+
+-- | A kind of fmap for Vect.
+vectMap :: (a -> b) -> Vect a n -> Vect b n
+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 x vect = case vect of
+  VNil -> VCons x VNil
+  VCons y v -> VCons y (vectSnoc x v)
+
+showVect :: Show a => Vect a l -> 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 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)
+  }
+
+-- | 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 = unMV . listToVect'
+
+  where
+
+    listToVect':: IsNat n => [a] -> MaybeVect a n
+    listToVect' = natRecursion inductive base reduce
+    
+    inductive :: [a] -> MaybeVect a m -> MaybeVect a (S m)
+    inductive xs maybeVect = case maybeVect of
+      MV Nothing -> MV Nothing
+      MV (Just vect) -> case xs of 
+        [] -> MV Nothing
+        (x : _) -> MV (Just (VCons x vect))
+
+    base :: [a] -> MaybeVect a Z
+    base xs = case xs of
+      [] -> MV (Just VNil)
+      _ -> MV Nothing
+
+    reduce :: [a] -> [a]
+    reduce xs = case xs of
+      [] -> []
+      (x : xs) -> xs
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,20 @@
+Copyright (c) 2015 Alexander Vieth
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/TypeNat.cabal b/TypeNat.cabal
new file mode 100644
--- /dev/null
+++ b/TypeNat.cabal
@@ -0,0 +1,24 @@
+-- Initial TypeNat.cabal generated by cabal init.  For further 
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                TypeNat
+version:             0.1.0.0
+synopsis:            Some Nat-indexed types for GHC
+-- description:         
+homepage:            https://github.com/avieth/TypeNat
+license:             MIT
+license-file:        LICENSE
+author:              Alexander Vieth
+maintainer:          aovieth@gmail.com
+-- copyright:           
+category:            Data
+build-type:          Simple
+cabal-version:       >=1.10
+
+library
+  exposed-modules:     Data.TypeNat.Fin, Data.TypeNat.Nat, Data.TypeNat.Vect
+  -- other-modules:       
+  other-extensions:    DataKinds, KindSignatures, GADTs, Rank2Types
+  build-depends:       base >=4.7 && <4.8
+  -- hs-source-dirs:      
+  default-language:    Haskell2010