diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,17 @@
 Changelog
 =========
 
+Version 0.1.0.1
+---------------
+
+*October 28, 2018*
+
+<https://github.com/mstksg/lens-typelevel/releases/tag/v0.1.0.1>
+
+*   Instances for `N`.
+*   Export value-level `mkLens`.
+*   Extensive documentation additions.
+
 Version 0.1.0.0
 ---------------
 
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -44,8 +44,12 @@
 implemented using type-level versions of `Context` and `Bazaar`:
 
 ```haskell
-ghci> :kind! '("hello", 6) ^. CloneLens_ L1_
-"hello"
+ghci> type CloneExample l   = ('( 'True, 'False ) & CloneLens_ l %~ NotSym0)
+                                                  ^. CloneLens_ l
+ghci> :kind! CloneExample L1_
+'False
+ghci> :kind! CloneExample L2_
+'True
 ```
 
 Using prefix function names:
@@ -79,3 +83,57 @@
 ghci> :kind! Set (IxList_ ('S 'Z)) "haskell" '["hello", "world", "curry"]
 '["hello", "haskell", "curry"]
 ```
+
+Defining lenses
+---------------
+
+There are two main ways to define optics.
+
+First, you can write them by hand using `singletonsOnly`:
+
+```haskell
+$(singletonsOnly [d|
+  l1 :: Functor f => LensLike (a, c) (b, c) a b
+  l1 f (x, y) = (\x' -> (x', y)) <$> f x
+
+  l1Alt :: Functor f => LensLike (a, c) (b, c) a b
+  l1Alt = mkLens fst (\(_, y) x -> (x', y))
+
+  getFirst :: Getting a (a, b) a
+  getFirst = to fst
+  |])
+```
+
+This creates the *type families* `L1`, `L1Alt`, and `GetFirst`; however, these
+aren't lenses, because they aren't partially applied.  The lactual lenses are
+`L1Sym0`, `L1AltSym0`, and `GetFirstSym0`.  As a convention, I
+recommend aliasing the *actual* lenses with an underscore suffix:
+
+```haskell
+-- L1_       :: Functor f => LensLike f (a, c) (b, c) a b
+type L1_       = L1Sym0
+
+-- L1Alt_    :: Functor f => LensLike f (a, c) (b, c) a b
+type L1Alt     = L1AltSym0
+
+-- GetFirst_ :: Getting a (a, b) a
+type GetFirst_ = GetFirstSym0
+```
+
+The number after the `Sym` is determined by how many arguments you need to
+apply to your function before you get to the actual lens.  For example,
+`IxList` requires one argument (the index) to get to the actual traversal, so
+the definition in the library is:
+
+```haskell
+type IxList_ i = IxListSym1 i
+```
+
+Second, you can write them directly at the type level using combinators like
+`MkLens_` and `To_`:
+
+```haskell
+type GetFirst_ = To_ FstSym0
+```
+
+(`FstSym0` is the promotion of `fst` from the *singletons* library)
diff --git a/lens-typelevel.cabal b/lens-typelevel.cabal
--- a/lens-typelevel.cabal
+++ b/lens-typelevel.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 32f70c034e55d2e4260473946cb22d88f640b361e30facad3d2b1c3fbcc524fe
+-- hash: dfd21a7ef669689f415cd15d00ef83ac7337dda223309f4d30ee56efddc44c71
 
 name:           lens-typelevel
-version:        0.1.0.0
+version:        0.1.0.1
 synopsis:       Type-level lenses using singletons
 description:    Type-level lenses using singletons and its defunctionalization system,
                 implemented using the same van Laarhoven encoding as the /lens/ package.
diff --git a/src/Data/Type/Lens.hs b/src/Data/Type/Lens.hs
--- a/src/Data/Type/Lens.hs
+++ b/src/Data/Type/Lens.hs
@@ -1,5 +1,9 @@
+{-# LANGUAGE DeriveDataTypeable   #-}
+{-# LANGUAGE DeriveGeneric        #-}
+{-# LANGUAGE EmptyCase            #-}
 {-# LANGUAGE FlexibleInstances    #-}
 {-# LANGUAGE GADTs                #-}
+{-# LANGUAGE InstanceSigs         #-}
 {-# LANGUAGE PolyKinds            #-}
 {-# LANGUAGE ScopedTypeVariables  #-}
 {-# LANGUAGE TemplateHaskell      #-}
@@ -31,6 +35,64 @@
 -- 'To_', 'MkLens_', etc. are all suffixed with @_@ for convenience, to
 -- reserve the underscoreless identifiers for the fully applied type family
 -- as per /singletons/ library convention.
+--
+-- "Value level" versions of these lenses and functions are not exported,
+-- because they would be more or less completely compatible with the same
+-- functions from /microlens/ and /lens/ packages.  However, when the names
+-- of these functions differ from the names of their /lens/ counterpart
+-- ('mkLens' and 'ixList'), value-level versions are provided.
+--
+-- There are two main ways to define optics.
+--
+-- First, you can write them by hand using 'singletonsOnly':
+--
+-- @
+--  $(singletonsOnly [d|
+--    l1 :: Functor f => LensLike (a, c) (b, c) a b
+--    l1 f (x, y) = (\x' -> (x', y)) <$> f x
+--
+--    l1Alt :: Functor f => LensLike (a, c) (b, c) a b
+--    l1Alt = mkLens fst (\(_, y) x -> (x', y))
+--
+--    getFirst :: Getting a (a, b) a
+--    getFirst = to fst
+--    |])
+-- @
+--
+-- This creates the /type families/ @L1@, @L1Alt@, and @GetFirst@; however,
+-- these aren't lenses, because they aren't partially applied.  The lactual
+-- lenses are @L1Sym0@, @L1AltSym0@, and @GetFirstSym0@.  As a convention,
+-- it is recommend to alias the /actual/ lenses with an underscore suffix:
+--
+-- @
+-- -- L1_       :: Functor f => LensLike f (a, c) (b, c) a b
+-- type L1_       = L1Sym0
+--
+-- -- L1Alt_    :: Functor f => LensLike f (a, c) (b, c) a b
+-- type L1Alt     = L1AltSym0
+--
+-- -- GetFirst_ :: Getting a (a, b) a
+-- type GetFirst_ = GetFirstSym0
+-- @
+--
+-- The number after the @Sym@ is determined by how many arguments you need
+-- to apply to your function before you get to the actual lens.  For
+-- example, `IxList` requires one argument (the index) to get to the actual
+-- traversal, so the definition in the library is:
+--
+-- @
+-- type IxList_ i = IxListSym1 i
+-- @
+--
+-- Second, you can write them directly at the type level using combinators
+-- like 'MkLens_' and 'To_':
+--
+-- @
+-- type GetFirst_ = 'To_' 'FstSym0'
+-- @
+--
+-- ('FstSym0' is the promotion of 'fst' from
+-- "Data.Singletons.Prelude.Tuple")
 module Data.Type.Lens (
     LensLike, LensLike'
   -- * Setting
@@ -54,9 +116,9 @@
   , ALens
   -- ** Making
   -- | Ways of creating a lens
-  , MkLens_, MkLens, sMkLens
+  , MkLens_, MkLens, sMkLens, mkLens
   -- ** Cloning
-  , CloneLens_, CloneLens, sCloneLens
+  , CloneLens_, CloneLens
   -- * Traversals and Folds
   , ATraversal
   -- ** Using
@@ -79,7 +141,7 @@
   , L2_, L2, sL2
   -- ** List
   , N(..), SN
-  , IxList_, IxList, sIxList
+  , IxList_, IxList, sIxList, ixList
   -- * Util
   , type (.@)
   , Sing (SZ, SS, SMkContext)
@@ -117,6 +179,8 @@
 import           Data.Singletons.Prelude.Monoid
 import           Data.Singletons.TH
 import           Data.Type.Lens.Internal
+import           Data.Typeable                           (Typeable)
+import           GHC.Generics                            (Generic)
 
 -- | The general shape of optics in this library. ("van Laarhoven")
 --
@@ -161,8 +225,13 @@
 -- | Peano nats, used for implementation of list index traversals in
 -- a termination-sane way.
 data N = Z | S N
+  deriving (Show, Eq, Ord, Read, Generic, Typeable)
 
 genSingletons [''LensLike, ''LensLike', ''ASetter, ''Getting, ''N]
+singEqInstance ''N
+singOrdInstance ''N
+singDecideInstance ''N
+singShowInstance ''N
 
 -- | If a function expects an 'ALens', it can be given any Lens (a
 -- @'LensLike' f@ that works for any 'Functor' f).
@@ -196,20 +265,6 @@
   to f g x = case g (f x) of
       Const y -> Const y
 
-  mkLens
-      :: Functor f
-      => (s -> a)
-      -> (s -> b -> t)
-      -> LensLike f s t a b
-  mkLens v s f x = s x <$> f (v x)
-
-  cloneLens
-      :: Functor f
-      => LensLike (Context a b) s t a b
-      -> LensLike f s t a b
-  cloneLens l f x = case l (\y -> MkContext id y) x of
-      MkContext g y -> g <$> f y
-
   toListOf :: Getting [a] s a -> s -> [a]
   toListOf l x = case l (Const . (:[])) x of
       Const ys -> ys
@@ -231,6 +286,13 @@
   folded f x = case traverse_ f x of
       Const y -> Const y
 
+  cloneLens
+      :: Functor f
+      => LensLike (Context a b) s t a b
+      -> LensLike f s t a b
+  cloneLens l f x = case l (\y -> MkContext id y) x of
+      MkContext g y -> g <$> f y
+
   cloneTraversal
       :: Applicative f
       => LensLike (Bazaar a b) s t a b
@@ -242,7 +304,16 @@
 
   l2 :: Functor f => LensLike f (a, b) (a, c) b c
   l2 f (x, y) = (\y' -> (x, y')) <$> f y
+  |])
 
+$(singletons [d|
+  mkLens
+      :: Functor f
+      => (s -> a)
+      -> (s -> b -> t)
+      -> LensLike f s t a b
+  mkLens v s f x = s x <$> f (v x)
+
   ixList :: Applicative f => N -> LensLike' f [a] a
   ixList _     _ []     = pure []
   ixList Z     f (x:xs) = (:xs) <$> f x
@@ -377,4 +448,3 @@
 --     -> 'LensLike'' f [a] a
 -- @
 type IxList_ i = IxListSym1 i
-
diff --git a/src/Data/Type/Lens/Example.hs b/src/Data/Type/Lens/Example.hs
--- a/src/Data/Type/Lens/Example.hs
+++ b/src/Data/Type/Lens/Example.hs
@@ -92,9 +92,11 @@
                           '["hello", "world", "curry"]
 
 -- |
--- >>> :kind! CloneExample
--- "hello"
-type CloneExample     = View (CloneLens_ L1_)  '("hello", 6     )
+-- >>> :kind! CloneExample L1_
+-- 'False
+-- >>> :kind! CloneExample L2_
+-- 'True
+type CloneExample l   = View (CloneLens_ l) (Over (CloneLens_ l) NotSym0 '( 'True, 'False ))
 
 
 type SetExample'       = '("hello", 6     )         &  L1_             .~ 'True
@@ -109,4 +111,4 @@
                           ] ^.. Traverse_ .@ L1_
 type UnsafeExample'    = '[] ^?! Traverse_
 type IxExample'        = '["hello","world","curry"] &  IxList_ ('S 'Z) .~ "haskell"
-type CloneExample'     = '("hello", 6     )         ^. CloneLens_ L1_
+type CloneExample' l   = ('( 'True, 'False ) & CloneLens_ l %~ NotSym0) ^. CloneLens_ l