diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,5 @@
+# Revision history for vec
+
+## 0.3
+
+- Split out of `vec`
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2017-2019, Oleg Grenrus
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Oleg Grenrus nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/src/Data/Vec/DataFamily/SpineStrict/Lens.hs b/src/Data/Vec/DataFamily/SpineStrict/Lens.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vec/DataFamily/SpineStrict/Lens.hs
@@ -0,0 +1,154 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+module Data.Vec.DataFamily.SpineStrict.Lens (
+    -- * Indexing
+    ix,
+    _Cons,
+    _head,
+    _tail,
+    -- * Conversions
+    _Pull,
+    _Vec,
+    ) where
+
+import Control.Applicative ((<$>))
+import Data.Fin            (Fin (..))
+import Data.Nat            (Nat (..))
+import Prelude             (($), (.), Functor (..))
+
+import qualified Control.Lens  as L
+import qualified Data.Fin      as F
+import qualified Data.Type.Nat as N
+import qualified Data.Vec.Pull as P
+
+import Data.Vec.DataFamily.SpineStrict
+
+-- $setup
+-- >>> :set -XScopedTypeVariables
+-- >>> import Prelude (Maybe (..), Char, Bool (..))
+-- >>> import Control.Lens ((^.), (&), (.~), over, (^?), (#))
+
+-------------------------------------------------------------------------------
+-- Indexing
+-------------------------------------------------------------------------------
+
+-- | Match on non-empty 'Vec'.
+--
+-- /Note:/ @lens@ 'L._Cons' is a 'L.Prism'.
+-- In fact, @'Vec' n a@ cannot have an instance of 'L.Cons' as types don't match.
+--
+_Cons :: L.Iso (Vec ('S n) a) (Vec ('S n) b) (a, Vec n a) (b, Vec n b)
+_Cons = L.iso (\(x ::: xs) -> (x, xs)) (\(x, xs) -> x ::: xs)
+
+-- | Head lens. /Note:/ @lens@ 'L._head' is a 'L.Traversal''.
+--
+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. _head
+-- 'a'
+--
+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) & _head .~ 'x'
+-- 'x' ::: 'b' ::: 'c' ::: VNil
+--
+_head :: L.Lens' (Vec ('S n) a) a
+_head f (x ::: xs) = (::: xs) <$> f x
+{-# INLINE _head #-}
+
+-- | Head lens. /Note:/ @lens@ 'L._head' is a 'L.Traversal''.
+_tail :: L.Lens' (Vec ('S n) a) (Vec n a)
+_tail f (x ::: xs) = (x :::) <$> f xs
+{-# INLINE _tail #-}
+
+-- | An 'I.Iso' from 'toPull' and 'fromPull'.
+_Pull :: N.InlineInduction n => L.Iso (Vec n a) (Vec n b) (P.Vec n a) (P.Vec n b)
+_Pull = L.iso toPull fromPull
+
+-- | Prism from list.
+--
+-- >>> "foo" ^? _Vec :: Maybe (Vec N.Nat3 Char)
+-- Just ('f' ::: 'o' ::: 'o' ::: VNil)
+--
+-- >>> "foo" ^? _Vec :: Maybe (Vec N.Nat2 Char)
+-- Nothing
+--
+-- >>> _Vec # (True ::: False ::: VNil)
+-- [True,False]
+--
+_Vec :: N.InlineInduction n => L.Prism' [a] (Vec n a)
+_Vec = L.prism' toList fromList
+
+-- | Index lens.
+--
+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (FS FZ)
+-- 'b'
+--
+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (FS FZ) .~ 'x'
+-- 'a' ::: 'x' ::: 'c' ::: VNil
+--
+ix :: forall n f a. (N.InlineInduction n, Functor f) => Fin n -> L.LensLike' f (Vec n a) a
+ix = getIxLens $ N.inlineInduction1 start step where
+    start :: IxLens f 'Z a
+    start = IxLens F.absurd
+
+    step :: IxLens f m a -> IxLens f ('S m) a
+    step (IxLens l) = IxLens $ \i -> case i of
+        FZ   -> _head
+        FS j -> _tail . l j
+
+newtype IxLens f n a = IxLens { getIxLens :: Fin n -> L.LensLike' f (Vec n a) a }
+
+
+-------------------------------------------------------------------------------
+-- Instances
+-------------------------------------------------------------------------------
+
+instance N.InlineInduction n => L.FunctorWithIndex (Fin n) (Vec n) where
+    imap = imap
+
+instance N.InlineInduction n => L.FoldableWithIndex (Fin n) (Vec n) where
+    ifoldMap = ifoldMap
+    ifoldr   = ifoldr
+
+instance N.InlineInduction n => L.TraversableWithIndex (Fin n) (Vec n) where
+    itraverse = itraverse
+
+instance N.InlineInduction n => L.Each (Vec n a) (Vec n b) a b where
+    each = traverse
+
+type instance L.Index (Vec n a)   = Fin n
+type instance L.IxValue (Vec n a) = a
+
+-- | 'Vec' doesn't have 'L.At' instance, as we __cannot__ remove value from 'Vec'.
+-- See 'ix' in "Data.Vec.DataFamily.SpineStrict" module for an 'L.Lens' (not 'L.Traversal').
+instance N.InlineInduction n => L.Ixed (Vec n a) where
+    ix = ix
+
+instance L.Field1 (Vec ('S n) a) (Vec ('S n) a) a a where
+    _1 = _head
+
+instance L.Field2 (Vec ('S ('S n)) a) (Vec ('S ('S n)) a) a a where
+    _2 = _tail . _head
+
+instance L.Field3 (Vec ('S ('S ('S n))) a) (Vec ('S ('S ('S n))) a) a a where
+    _3 = _tail . _tail . _head
+
+instance L.Field4 (Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S ('S n)))) a) a a where
+    _4 = _tail . _tail . _tail . _head
+
+instance L.Field5 (Vec ('S ('S ('S ('S ('S n))))) a) (Vec ('S ('S ('S ('S ('S n))))) a) a a where
+    _5 = _tail . _tail . _tail . _tail . _head
+
+instance L.Field6 (Vec ('S ('S ('S ('S ('S ('S n)))))) a) (Vec ('S ('S ('S ('S ('S ('S n)))))) a) a a where
+    _6 = _tail . _tail . _tail . _tail . _tail . _head
+
+instance L.Field7 (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a) (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a) a a where
+    _7 = _tail . _tail . _tail . _tail . _tail . _tail . _head
+
+instance L.Field8 (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a) (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a) a a where
+    _8 = _tail . _tail . _tail . _tail . _tail . _tail . _tail . _head
+
+instance L.Field9 (Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a) (Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a) a a where
+    _9 = _tail . _tail . _tail . _tail . _tail . _tail . _tail . _tail . _head
diff --git a/src/Data/Vec/Lazy/Inline/Lens.hs b/src/Data/Vec/Lazy/Inline/Lens.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vec/Lazy/Inline/Lens.hs
@@ -0,0 +1,77 @@
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module Data.Vec.Lazy.Inline.Lens (
+    -- * Indexing
+    ix,
+    _Cons,
+    _head,
+    _tail,
+    -- * Conversions
+    _Pull,
+    _Vec,
+    ) where
+
+import Data.Fin           (Fin (..))
+import Data.Nat           (Nat (..))
+import Data.Vec.Lazy.Lens (_Cons, _head, _tail)
+import Prelude            (Functor, ($), (.))
+
+import qualified Control.Lens  as L
+import qualified Data.Fin      as F
+import qualified Data.Type.Nat as N
+import qualified Data.Vec.Pull as P
+
+import Data.Vec.Lazy.Inline
+
+-- $setup
+-- >>> :set -XScopedTypeVariables
+-- >>> import Prelude (Maybe (..), Char, Bool (..))
+-- >>> import Control.Lens ((^.), (&), (.~), over, (^?), (#))
+
+-------------------------------------------------------------------------------
+-- Indexing
+-------------------------------------------------------------------------------
+
+-- | Index lens.
+--
+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (FS FZ)
+-- 'b'
+--
+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (FS FZ) .~ 'x'
+-- 'a' ::: 'x' ::: 'c' ::: VNil
+--
+ix :: forall n f a. (N.InlineInduction n, Functor f) => Fin n -> L.LensLike' f (Vec n a) a
+ix = getIxLens $ N.inlineInduction1 start step where
+    start :: IxLens f 'Z a
+    start = IxLens F.absurd
+
+    step :: IxLens f m a -> IxLens f ('S m) a
+    step (IxLens l) = IxLens $ \i -> case i of
+        FZ   -> _head
+        FS j -> _tail . l j
+
+newtype IxLens f n a = IxLens { getIxLens :: Fin n -> L.LensLike' f (Vec n a) a }
+
+-------------------------------------------------------------------------------
+-- Conversions
+-------------------------------------------------------------------------------
+
+-- | An 'L.Iso' from 'toPull' and 'fromPull'.
+_Pull :: N.InlineInduction n => L.Iso (Vec n a) (Vec n b) (P.Vec n a) (P.Vec n b)
+_Pull = L.iso toPull fromPull
+
+-- | Prism from list.
+--
+-- >>> "foo" ^? _Vec :: Maybe (Vec N.Nat3 Char)
+-- Just ('f' ::: 'o' ::: 'o' ::: VNil)
+--
+-- >>> "foo" ^? _Vec :: Maybe (Vec N.Nat2 Char)
+-- Nothing
+--
+-- >>> _Vec # (True ::: False ::: VNil)
+-- [True,False]
+--
+_Vec :: N.InlineInduction n => L.Prism' [a] (Vec n a)
+_Vec = L.prism' toList fromList
diff --git a/src/Data/Vec/Lazy/Lens.hs b/src/Data/Vec/Lazy/Lens.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vec/Lazy/Lens.hs
@@ -0,0 +1,148 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+module Data.Vec.Lazy.Lens  (
+    -- * Indexing
+    ix,
+    _Cons,
+    _head,
+    _tail,
+    -- * Conversions
+    _Pull,
+    _Vec,
+    ) where
+
+import Control.Applicative ((<$>))
+import Data.Fin            (Fin (..))
+import Data.Nat            (Nat (..))
+import Prelude             ((.))
+
+import qualified Control.Lens  as L
+import qualified Data.Type.Nat as N
+import qualified Data.Vec.Pull as P
+
+import Data.Vec.Lazy
+
+-- $setup
+-- >>> :set -XScopedTypeVariables
+-- >>> import Prelude (Maybe (..), Char, Bool (..))
+-- >>> import Control.Lens ((^.), (&), (.~), over, (^?), (#))
+
+-------------------------------------------------------------------------------
+-- Indexing
+-------------------------------------------------------------------------------
+
+-- | Index lens.
+--
+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. ix (FS FZ)
+-- 'b'
+--
+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) & ix (FS FZ) .~ 'x'
+-- 'a' ::: 'x' ::: 'c' ::: VNil
+--
+ix :: Fin n -> L.Lens' (Vec n a) a
+ix FZ     f (x ::: xs) = (::: xs) <$> f x
+ix (FS n) f (x ::: xs) = (x :::)  <$> ix n f xs
+
+-- | Match on non-empty 'Vec'.
+--
+-- /Note:/ @lens@ 'L._Cons' is a 'L.Prism'.
+-- In fact, @'Vec' n a@ cannot have an instance of 'L.Cons' as types don't match.
+--
+_Cons :: L.Iso (Vec ('S n) a) (Vec ('S n) b) (a, Vec n a) (b, Vec n b)
+_Cons = L.iso (\(x ::: xs) -> (x, xs)) (\(x, xs) -> x ::: xs)
+
+-- | Head lens. /Note:/ @lens@ 'L._head' is a 'L.Traversal''.
+--
+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) ^. _head
+-- 'a'
+--
+-- >>> ('a' ::: 'b' ::: 'c' ::: VNil) & _head .~ 'x'
+-- 'x' ::: 'b' ::: 'c' ::: VNil
+--
+_head :: L.Lens' (Vec ('S n) a) a
+_head f (x ::: xs) = (::: xs) <$> f x
+{-# INLINE _head #-}
+
+-- | Tail lens.
+_tail :: L.Lens' (Vec ('S n) a) (Vec n a)
+_tail f (x ::: xs) = (x :::) <$> f xs
+{-# INLINE _tail #-}
+
+-------------------------------------------------------------------------------
+-- Conversions
+-------------------------------------------------------------------------------
+
+-- | An 'I.Iso' from 'toPull' and 'fromPull'.
+_Pull :: N.SNatI n => L.Iso (Vec n a) (Vec n b) (P.Vec n a) (P.Vec n b)
+_Pull = L.iso toPull fromPull
+
+-- | Prism from list.
+--
+-- >>> "foo" ^? _Vec :: Maybe (Vec N.Nat3 Char)
+-- Just ('f' ::: 'o' ::: 'o' ::: VNil)
+--
+-- >>> "foo" ^? _Vec :: Maybe (Vec N.Nat2 Char)
+-- Nothing
+--
+-- >>> _Vec # (True ::: False ::: VNil)
+-- [True,False]
+--
+_Vec :: N.SNatI n => L.Prism' [a] (Vec n a)
+_Vec = L.prism' toList fromList
+
+-------------------------------------------------------------------------------
+-- Instances
+-------------------------------------------------------------------------------
+
+instance L.FunctorWithIndex (Fin n) (Vec n) where
+    imap = imap
+
+instance L.FoldableWithIndex (Fin n) (Vec n) where
+    ifoldMap = ifoldMap
+    ifoldr   = ifoldr
+
+instance L.TraversableWithIndex (Fin n) (Vec n) where
+    itraverse = itraverse
+
+instance L.Each (Vec n a) (Vec n b) a b where
+    each = traverse
+
+type instance L.Index (Vec n a)   = Fin n
+type instance L.IxValue (Vec n a) = a
+
+-- | 'Vec' doesn't have 'L.At' instance, as we __cannot__ remove value from 'Vec'.
+-- See 'ix' in "Data.Vec.Lazy" module for an 'L.Lens' (not 'L.Traversal').
+instance L.Ixed (Vec n a) where
+    ix = ix
+
+instance L.Field1 (Vec ('S n) a) (Vec ('S n) a) a a where
+    _1 = _head
+
+instance L.Field2 (Vec ('S ('S n)) a) (Vec ('S ('S n)) a) a a where
+    _2 = _tail . _head
+
+instance L.Field3 (Vec ('S ('S ('S n))) a) (Vec ('S ('S ('S n))) a) a a where
+    _3 = _tail . _tail . _head
+
+instance L.Field4 (Vec ('S ('S ('S ('S n)))) a) (Vec ('S ('S ('S ('S n)))) a) a a where
+    _4 = _tail . _tail . _tail . _head
+
+instance L.Field5 (Vec ('S ('S ('S ('S ('S n))))) a) (Vec ('S ('S ('S ('S ('S n))))) a) a a where
+    _5 = _tail . _tail . _tail . _tail . _head
+
+instance L.Field6 (Vec ('S ('S ('S ('S ('S ('S n)))))) a) (Vec ('S ('S ('S ('S ('S ('S n)))))) a) a a where
+    _6 = _tail . _tail . _tail . _tail . _tail . _head
+
+instance L.Field7 (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a) (Vec ('S ('S ('S ('S ('S ('S ('S n))))))) a) a a where
+    _7 = _tail . _tail . _tail . _tail . _tail . _tail . _head
+
+instance L.Field8 (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a) (Vec ('S ('S ('S ('S ('S ('S ('S ('S n)))))))) a) a a where
+    _8 = _tail . _tail . _tail . _tail . _tail . _tail . _tail . _head
+
+instance L.Field9 (Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a) (Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))) a) a a where
+    _9 = _tail . _tail . _tail . _tail . _tail . _tail . _tail . _tail . _head
diff --git a/src/Data/Vec/Lens/Instances.hs b/src/Data/Vec/Lens/Instances.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vec/Lens/Instances.hs
@@ -0,0 +1,7 @@
+-- | This module re-exports instances from all the modules defined
+-- in @vec-lens@ package.
+module Data.Vec.Lens.Instances () where
+
+import Data.Vec.Lazy.Lens ()
+import Data.Vec.Pull.Lens ()
+import Data.Vec.DataFamily.SpineStrict.Lens ()
diff --git a/src/Data/Vec/Pull/Lens.hs b/src/Data/Vec/Pull/Lens.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vec/Pull/Lens.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+module Data.Vec.Pull.Lens (
+    -- * Indexing
+    ix,
+    _Cons,
+    _head,
+    _tail,
+    -- * Conversions
+    _Vec,
+    ) where
+
+import Control.Lens ((<&>))
+import Data.Fin     (Fin (..))
+import Data.Nat     (Nat (..))
+
+import qualified Control.Lens  as L
+import qualified Data.Type.Nat as N
+
+import Data.Vec.Pull
+
+-- $setup
+-- >>> :set -XScopedTypeVariables
+-- >>> import Control.Lens ((^.), (&), (.~), over)
+-- >>> import qualified Data.Vec.Lazy as L
+-- >>> import qualified Data.Vec.Lazy.Lens as L
+
+-------------------------------------------------------------------------------
+-- Indexing
+-------------------------------------------------------------------------------
+
+-- | Index lens.
+--
+-- >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) ^. L._Pull . ix (FS FZ)
+-- 'b'
+--
+-- >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) & L._Pull . ix (FS FZ) .~ 'x'
+-- 'a' ::: 'x' ::: 'c' ::: VNil
+--
+ix :: Fin n -> L.Lens' (Vec n a) a
+ix i f (Vec v) = f (v i) <&> \a -> Vec $ \j ->
+    if i == j
+    then a
+    else v j
+
+-- | Match on non-empty 'Vec'.
+--
+-- /Note:/ @lens@ 'L._Cons' is a 'L.Prism'.
+-- In fact, @'Vec' n a@ cannot have an instance of 'L.Cons' as types don't match.
+--
+_Cons :: L.Iso (Vec ('S n) a) (Vec ('S n) b) (a, Vec n a) (b, Vec n b)
+_Cons = L.iso (\(Vec v) -> (v FZ, Vec (v . FS))) (\(x, xs) -> cons x xs)
+
+-- | Head lens. /Note:/ @lens@ 'L._head' is a 'L.Traversal''.
+--
+-- >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) ^. L._Pull . _head
+-- 'a'
+--
+-- >>> ('a' L.::: 'b' L.::: 'c' L.::: L.VNil) & L._Pull . _head .~ 'x'
+-- 'x' ::: 'b' ::: 'c' ::: VNil
+--
+_head :: L.Lens' (Vec ('S n) a) a
+_head f (Vec v) = f (v FZ) <&> \a -> Vec $ \j -> case j of
+    FZ -> a
+    _   -> v j
+{-# INLINE _head #-}
+
+-- | Head lens. /Note:/ @lens@ 'L._head' is a 'L.Traversal''.
+_tail :: L.Lens' (Vec ('S n) a) (Vec n a)
+_tail f (Vec v) = f (Vec (v . FS)) <&> \xs -> cons (v FZ) xs
+{-# INLINE _tail #-}
+
+-------------------------------------------------------------------------------
+-- Conversions
+-------------------------------------------------------------------------------
+
+-- | Prism from list.
+_Vec :: N.SNatI n => L.Prism' [a] (Vec n a)
+_Vec = L.prism' toList fromList
+
+-------------------------------------------------------------------------------
+-- Instances
+-------------------------------------------------------------------------------
+
+instance L.FunctorWithIndex (Fin n) (Vec n) where
+    imap = imap
+
+instance N.SNatI n => L.FoldableWithIndex (Fin n) (Vec n) where
+    ifoldMap = ifoldMap
+    ifoldr   = ifoldr
diff --git a/vec-lens.cabal b/vec-lens.cabal
new file mode 100644
--- /dev/null
+++ b/vec-lens.cabal
@@ -0,0 +1,61 @@
+cabal-version:      2.2
+name:               vec-lens
+version:            0.3
+synopsis:           Vec: length-indexed (sized) list: lens support
+category:           Data, Dependent Types, Lens
+description:
+  This package provides [lenses](https://hackage.haskell.org/package/lens) and instances
+  for data types in [vec](https://hackage.haskell.org/package/vec) package.
+  .
+  "Data.Vec.Lens.Instances" provides all the instances.
+  the other modules provide some named lenses too.
+
+homepage:           https://github.com/phadej/vec
+bug-reports:        https://github.com/phadej/vec/issues
+license:            BSD-3-Clause
+license-file:       LICENSE
+author:             Oleg Grenrus <oleg.grenrus@iki.fi>
+maintainer:         Oleg.Grenrus <oleg.grenrus@iki.fi>
+copyright:          (c) 2017-2019 Oleg Grenrus
+build-type:         Simple
+extra-source-files: ChangeLog.md
+tested-with:
+  GHC ==7.8.4
+   || ==7.10.3
+   || ==8.0.2
+   || ==8.2.2
+   || ==8.4.4
+   || ==8.6.5
+   || ==8.8.1
+
+source-repository head
+  type:     git
+  location: https://github.com/phadej/vec.git
+  subdir:   vec-lens
+
+library
+  default-language: Haskell2010
+  ghc-options:      -Wall -fprint-explicit-kinds
+  hs-source-dirs:   src
+  exposed-modules:
+    Data.Vec.DataFamily.SpineStrict.Lens
+    Data.Vec.Lazy.Inline.Lens
+    Data.Vec.Lazy.Lens
+    Data.Vec.Lens.Instances
+    Data.Vec.Pull.Lens
+
+  -- GHC boot libs
+  build-depends:    base >=4.7 && <4.14
+
+  -- siblings
+  build-depends:
+    , fin  ^>=0.1.1
+    , vec  ^>=0.3
+
+  -- other dependencies
+  build-depends:    lens ^>=4.18.1
+  other-extensions:
+    CPP
+    FlexibleContexts
+    GADTs
+    TypeOperators