diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,136 @@
+typelits-witnesses
+==================
+
+Provides witnesses for `KnownNat` and `KnownSymbol` instances for various
+operations on GHC TypeLits --- in particular, the arithmetic operations
+defined in `GHC.TypeLits`, and also for type-level lists of `KnownNat` and
+`KnownSymbol` instances.
+
+This is useful for situations where you have `KnownNat n`, and you want to
+prove to GHC `KnownNat (n + 3)`, or `KnownNat (2*n + 4)`.
+
+It's also useful for when you want to work with type level lists of
+`KnownNat`/`KnownSymbol` instances and singletons for traversing them, and be
+able to apply analogies of `natVal`/`symbolVal` to lists with analogies for
+`SomeNat` and `SomeSymbol`.
+
+`GHC.TypeLits.Witnesses`
+------------------------
+
+Provides witnesses for instances arising from the arithmetic operations
+defined in `GHC.TypeLits`.
+
+In general, if you have `KnownNat n`, GHC can't infer `KnownNat (n + 1)`;
+and if you have `KnownNat m`, as well, GHC can't infer `KnownNat (n + m)`.
+
+This can be extremely annoying when dealing with libraries and applications
+where one regularly adds and subtracts type-level nats and expects `KnownNat`
+instances to follow.  For example, vector concatenation of length-encoded
+vector types can be:
+
+~~~haskell
+concat :: (KnownNat n, KnownNat m)
+       => Vector n       a
+       -> Vector m       a
+       -> Vector (n + m) a
+~~~
+
+But, `n + m` now does not have a `KnownNat` instance, which severely hinders
+what you can do with this!
+
+Consider this concrete (but silly) example:
+
+~~~haskell
+getDoubled :: KnownNat n => Proxy n -> Integer
+getDoubled p = natVal (Proxy :: Proxy (n * 2))
+~~~
+
+Which is supposed to call `natVal` with `n * 2`.  However, this fails, because
+while `n` is a `KnownNat`, `n * 2` is not necessarily so.  This module lets
+you re-assure GHC that this is okay.
+
+The most straightforward/high-level usage is with `withNatOp`:
+
+~~~haskell
+getDoubled :: forall n. KnownNat n => Proxy n -> Integer
+getDoubled p = withNatOp (%*) p (Proxy :: Proxy 2) $
+    natVal (Proxy :: Proxy (n * 2))
+~~~
+
+Within the scope of the argument of
+`withNatOp (%*) (Proxy :: Proxy n) (Proxy :: Proxy m)`, `n * m` is an instance
+of `KnownNat`, so you can use `natVal` on it, and get the expected result:
+
+~~~haskell
+> getDoubled (Proxy :: Proxy 12)
+24
+~~~
+
+There are four "nat operations" defined here, corresponding to the four
+type-level operations on `Nat` provided in `GHC.TypeLits`: `(%+)`, `(%-)`,
+`(%*)`, and `(%^)`, corresponding to addition, subtraction, multiplication,
+and exponentiation, respectively.
+
+Note that `(%-)` is implemented in a way that allows for the result to be a
+*negative* `Nat`.
+
+There are more advanced operations dealing with low-level machinery, as well,
+in the module.  See module documentation for more detail.
+
+`GHC.TypeLits.List`
+-------------------
+
+Provides analogies of `KnownNat`, `SomeNat`, `natVal`, etc., to type-level
+lists of `KnownNat` instances, and also singletons for iterating over
+type-level lists of `Nat`s and `Symbol`s.
+
+If you had `KnownNats ns`, then you have two things you can do with it; first,
+`natsVal`, which is like `natVal` but for type-level lists of `KnownNats`:
+
+~~~haskell
+> natsVal (Proxy :: Proxy [1,2,3])
+[1,2,3]
+~~~
+
+And more importantly, `natsList`, which provides singletons that you can
+pattern match on to "reify" the structure of the list, getting a `Proxy n` for
+every item in the list with a `KnownNat`/`KnownSymbol` instance in scope for
+you to use:
+
+~~~haskell
+printNats :: NatList ns -> IO ()
+printNats nl = case nl of
+                 ØNL       ->
+                   return ()
+                 p :># nl' -> do
+                   print $ natVal p
+                   printNats nl'
+~~~
+
+~~~haskell
+> printNats (natsList :: NatList [1,2,3])
+1
+2
+3
+~~~
+
+Without this, there is no way to "iterate over" and "access" every `Nat` in a
+list of `KnownNat`s.  You can't "iterate" over `[1,2,3]` in `Proxy [1,2,3]`,
+but you can iterate over them in `NatList [1,2,3]`.
+
+This module also lets you "reify" lists of `Integer`s or `String`s into
+`NatList`s and `SymbolList`s, so you can access them at the type level for
+some dependent types fun.
+
+~~~haskell
+> reifyNats [1,2,3] $ \nl -> do
+    print nl
+    printNats nl
+Proxy :<# Proxy :<# Proxy :<# ØNL
+1
+2
+3
+~~~
+
+See module documentation for more details and variations.
+
diff --git a/typelits-witnesses.cabal b/typelits-witnesses.cabal
--- a/typelits-witnesses.cabal
+++ b/typelits-witnesses.cabal
@@ -1,5 +1,5 @@
 name:                typelits-witnesses
-version:             0.1.0.0
+version:             0.1.0.1
 synopsis:            Existential witnesses, singletons, and classes for operations on GHC TypeLits
 description:         Provides witnesses for 'KnownNat' and 'KnownSymbol'
                      instances for various operations on GHC TypeLits - in
@@ -26,7 +26,7 @@
 copyright:           (c) Justin Le 2015
 category:            Data
 build-type:          Simple
--- extra-source-files:  
+extra-source-files:  README.md
 cabal-version:       >=1.10
 
 source-repository head