diff --git a/Test.hs b/Test.hs
--- a/Test.hs
+++ b/Test.hs
@@ -1,5 +1,3 @@
 module Test where
 
-import Test.QuickCheck.Test
-import Generics.Pointless.Lenses
 import Generics.Pointless.Lenses.Examples.Examples
diff --git a/pointless-lenses.cabal b/pointless-lenses.cabal
--- a/pointless-lenses.cabal
+++ b/pointless-lenses.cabal
@@ -1,5 +1,5 @@
 Name:            pointless-lenses
-Version:         0.0.5
+Version:         0.0.6
 License:         BSD3
 License-file:    LICENSE
 Author:          Alcino Cunha <alcino@di.uminho.pt>, Hugo Pacheco <hpacheco@di.uminho.pt>
diff --git a/src/Generics/Pointless/Lenses.hs b/src/Generics/Pointless/Lenses.hs
--- a/src/Generics/Pointless/Lenses.hs
+++ b/src/Generics/Pointless/Lenses.hs
@@ -37,6 +37,19 @@
 dec_lns :: Enum a => Lens a a
 dec_lns = Lens pred (succ . fst) succ
 
+-- | QuickCheck procedure to test if two lenses are equivalent.
+lnsEq :: (Eq a,Eq c) => Lens c a -> Lens c a -> a -> c -> Bool
+lnsEq l l' a c = getEq l l' c && putEq l l' a c && createEq l l' a
+
+getEq :: Eq a => Lens c a -> Lens c a -> c -> Bool
+getEq l l' c = get l c == get l' c
+
+putEq :: (Eq a,Eq c) => Lens c a -> Lens c a -> a -> c -> Bool
+putEq l l' a c = put l (a,c) == put l' (a,c)
+
+createEq :: Eq c => Lens c a -> Lens c a -> a -> Bool
+createEq l l' a = create l a == create l' a
+
 -- | QuickCheck procedure to test if a lens is well-behaved.
 wb :: (Eq a,Eq c) => Lens c a -> a -> c -> Bool
 wb l a c = putget l a c && getput l c && createget l a
diff --git a/src/Generics/Pointless/Lenses/Combinators.hs b/src/Generics/Pointless/Lenses/Combinators.hs
--- a/src/Generics/Pointless/Lenses/Combinators.hs
+++ b/src/Generics/Pointless/Lenses/Combinators.hs
@@ -24,12 +24,17 @@
 -- * Point-free lens combinators
 
 -- | Function application is a lens.
-ap_lns :: Eq a => a -> Lens ((a -> b),a) b
-ap_lns a = Lens get' put' create'
+ap_lns :: Eq a => (b -> a) -> Lens ((a -> b),a) b
+ap_lns f = Lens get' put' create'
     where get' = app
-          put' (b,(f,a)) = (\x -> if x==a then b else f x,a)
-          create' = const /\ const a
+          --put' = (ext /\ fst . snd) . assocr . swap
+          put' (y,(g,x)) = let h x' = if x == x' then y else g x in (h,x)
+          create' = const /\ f              
 
+--ext :: Eq a => ((a -> b),(a,b)) -> (a -> b)
+--ext = curry f
+--    where f = (snd . snd . fst \/ app . (fst >< id)) . ((eq . (fst . snd >< id))?)
+
 -- | Predicate application is a lens.
 infix 0 ?<
 (?<) :: Eq a => Lens (a -> Bool,a) (Either a a)
@@ -43,10 +48,22 @@
 -- Applies a lens to the domain of a function.
 rexp_lns :: Lens b c -> Lens (a -> b) (a -> c)
 rexp_lns l = Lens get' put' create'
-    where get' = curry (get l . app)
-          put' = curry ((put l) . app . (split >< id))
-          create' = curry (create l . app)
+    where get' = rexp (get l)
+          put' = rexp (put l) . split
+          create' = rexp (create l)
 
+curry_lns :: Lens ((a,b) -> c) (a -> b -> c)
+curry_lns = Lens get' put' create'
+    where get' = curry
+          put' = uncurry . fst
+          create' = uncurry
+
+uncurry_lns :: Lens (a -> b -> c) ((a,b) -> c)
+uncurry_lns = Lens get' put' create'
+    where get' = uncurry
+          put' = curry . fst
+          create' = curry
+
 -- | The lens composition operator.
 infixr 9 .<
 (.<) :: Lens b a -> Lens c b -> Lens c a
@@ -56,18 +73,18 @@
           create' = create g . create f
 
 -- | The @fst@ point-free combinator.
-fst_lns :: b -> Lens (a,b) a
-fst_lns b = Lens get' put' create'
+fst_lns :: (a -> b) -> Lens (a,b) a
+fst_lns f = Lens get' put' create'
     where get' = fst
           put' = id >< snd
-          create' = id /\ (b!)
+          create' = id /\ f
 
 -- | The @snd@ point-free combinator.
-snd_lns :: a -> Lens (a,b) b
-snd_lns a = Lens get' put' create'
+snd_lns :: (b -> a) -> Lens (a,b) b
+snd_lns f = Lens get' put' create'
     where get' = snd
           put' = swap . (id >< fst)
-          create' = (a!) /\ id
+          create' = f /\ id
 
 -- | The @><@ point-free combinator.
 infix 7 ><<
@@ -77,6 +94,13 @@
           put' = (put f >< put g) . distp
           create' = create f >< create g
 
+infix 4 \/<
+(\/<) :: (c -> Either One One) -> Lens a c -> Lens b c -> Lens (Either a b) c
+(\/<) p f g = Lens get' put' create'
+    where get' = get f \/ get g
+          put' = (put f -|- put g) . distr
+          create' = (create f -|- create g) . (p??)
+
 -- | The left-biased @\/@ point-free combinator.
 -- It chooses left values over right values in the @create@ direction.
 infix 4 .\/<
@@ -112,11 +136,11 @@
 
 -- | The @pnt@ point-free combinator.
 infix 0 !<
-(!<) :: c -> Lens c One
-(!<) c = Lens get' put' create'
+(!<) :: (One -> c) -> Lens c One
+(!<) f = Lens get' put' create'
     where get' = bang
           put' = snd
-          create' = (c!)
+          create' = f
 
 -- | The @(a!) \/ f@ point-free expression, where @a@ is a constant and @f@ a function.
 -- The additional argument of type @c@ is the default value when the view matches the constant of type @a@.
@@ -138,25 +162,60 @@
 
 -- | The @inl \/ f@ point-free expression, where @f@ is a function.
 infix 4 #\/<
-(#\/<) :: Lens b (Either a c) -> Lens (Either a b) (Either a c)
-(#\/<) f = Lens get' put' create'
-    where get' = inl \/ get f
-          put' = ((id -|- create f . inr) . fst \/ inr . put f) . distr
-          create' = id -|- create f . inr
+(#\/<) :: Lens a c -> Lens b (Either c d) -> Lens (Either a b) (Either c d)
+(#\/<) f g = ((id_lns .\/< id_lns) -|-< id_lns) .< coassocl_lns .< (f -|-< g)
+{-(#\/<) f g = Lens get' put' create'
+    where get' = inl . get f \/ get g
+          put' = ((put f -|- create g . inr . fst) . distl \/ inr . put g) . distr
+          create' = create f -|- create g . inr-}
+          
 
 -- | The @f \/ inr@ point-free expression, where @f@ is a function.
 infix 4 \/$<
-(\/$<) :: Lens a (Either c b) -> Lens (Either a b) (Either c b)
-(\/$<) f = Lens get' put' create'
-    where get' = get f \/ inr
-          put' = (inl . put f \/ (create f . inl -|- id) . fst) . distr
-          create' = create f . inl -|- id
+(\/$<) :: Lens a (Either c d) -> Lens b d -> Lens (Either a b) (Either c d)
+(\/$<) f g = (id_lns -|-< (id_lns \/.< id_lns)) .< coassocr_lns .< (f -|-< g)
+{-(\/$<) f g = Lens get' put' create'
+    where get' = get f \/ inr . get g
+          put' = (inl . put f \/ (create f . inl . fst -|- put g) . distl) . distr
+          create' = create f . inl -|- create g-}
 
+-- | The @bang /\ f@ point-free expression, where @f@ is a function.
+infix 4 !/\<
+(!/\<) :: Lens c a -> Lens c (One,a)
+(!/\<) f = Lens get' put' create'
+    where get' = bang /\ get f
+          put' = put f . (snd >< id)
+          create' = create f . snd
+
+-- | The @f /\ bang@ point-free expression, where @f@ is a function.
+infix 4 /\!<
+(/\!<) :: Lens c a -> Lens c (a,One)
+(/\!<) f = Lens get' put' create'
+    where get' = get f /\ bang
+          put' = put f . (fst >< id)
+          create' = create f . fst
+
 -- * Point-free isomorphism combinators
 
 -- | The lens identity combinator.
 id_lns :: Lens c c
 id_lns = Lens id fst id
+
+-- | The @subr@ point-free combinator.
+subr_lns :: Lens (a,(b,c)) (b,(a,c))
+subr_lns = Lens subr (subr . fst) subr
+
+-- | The @subl@ point-free combinator.
+subl_lns :: Lens ((a,b),c) ((a,c),b)
+subl_lns = Lens subl (subl . fst) subl
+
+-- | The @cosubr@ point-free combinator.
+cosubr_lns :: Lens (Either a (Either b c)) (Either b (Either a c))
+cosubr_lns = Lens cosubr (cosubr . fst) cosubr
+
+-- | The @cosubl@ point-free combinator.
+cosubl_lns :: Lens (Either (Either a b) c) (Either (Either a c) b)
+cosubl_lns = Lens cosubl (cosubl . fst) cosubl
 
 -- | The @distp@ point-free combinator.
 distp_lns :: Lens ((c,d),(a,b)) ((c,a),(d,b))
diff --git a/src/Generics/Pointless/Lenses/Examples/Examples.hs b/src/Generics/Pointless/Lenses/Examples/Examples.hs
--- a/src/Generics/Pointless/Lenses/Examples/Examples.hs
+++ b/src/Generics/Pointless/Lenses/Examples/Examples.hs
@@ -28,117 +28,172 @@
 import Generics.Pointless.Lenses.RecursionPatterns
 import Generics.Pointless.Lenses.Reader.RecursionPatterns
 
--- | Integer successor lens.
-succ_lns :: Lens Int Int
-succ_lns = Lens succ (pred . fst) pred
+import Data.Char
 
+-- * Lenses over trees
+
+type instance BF Tree = BConst One :+| (BPar :*| (BId :*| BId))
+
+-- | Flatten a tree into a list.
+preOrd_lns :: Lens (Tree a) [a]
+preOrd_lns = cata_lns _L (inn_lns .< (id_lns -|-< id_lns ><< cat_lns))
+
+-- | Flatten a tree into a list.
+postOrd_lns :: Lens (Tree a) [a]
+postOrd_lns = cata_lns _L (eitherNilSnoc .< (id_lns -|-< id_lns ><< cat_lns))
+
+-- * Lenses over lists and natural numbers
+
 -- | List length lens.
 length_lns :: a -> Lens [a] Nat
-length_lns a = nat_lns _L (\x -> id_lns -|-< snd_lns a)
+length_lns a = nat_lns _L (\x -> id_lns -|-< snd_lns (a!))
 
--- | List length using an accumulation (after simplification into an hylomorphism).
--- Uses @Int@ instead of @Nat@ because @succ@ on @Nat@ is not a valid lens.
-len_lns :: Lens ([Char],Int) Int
-len_lns = hylo_lns t g h
-    where g = id_lns .\/< id_lns
-          h = (snd_lns _L -|-< snd_lns _L .< assocr_lns .< (id_lns ><< succ_lns)) .< distl_lns .< (out_lns ><< id_lns)
-          t = _L :: K Int :+!: I
+zipWith_lns :: Lens (a,b) c -> Lens ([a],[b]) [c]
+zipWith_lns f = ana_lns _L (((!<) c -|-< (f ><< id_lns) .< distp_lns) .< coassocl_lns .< dists_lns .< (out_lns ><< out_lns))
+    where 
+          -- 1st option: do nothing
+          -- 2nd option: append to the left source list
+          -- 3rd option: append to right source list
+          c = const $ Left (Left (_L,_L))
 
 -- | List zipping lens.
--- The aux transformation is merely for simplifying the constant argument
-zip_lns :: Lens ([a],[a]) [(a,a)]
-zip_lns = ana_lns _L (((!<) c .< aux -|-< distp_lns) .< coassocl_lns .< dists_lns .< (out_lns ><< out_lns))
-    where aux = (fst_lns _L -|-< snd_lns _L) -|-< fst_lns _L
-          c :: Either (Either One (b,[b])) (a,[a])
+zip_lns :: Lens ([a],[b]) [(a,b)]
+zip_lns = ana_lns _L (((!<) c -|-< distp_lns) .< coassocl_lns .< dists_lns .< (out_lns ><< out_lns))
+    where 
           -- 1st option: do nothing
           -- 2nd option: append to the left source list
           -- 3rd option: append to right source list
-          c = Left (Left _L)
+          c = const $ Left (Left (_L,_L))
 
 -- | Take the first n elements from a list
 take_lns :: Lens (Nat,[a]) [a]
 take_lns = ana_lns _L h
-   where h = ((!<) c -|-< aux) .< coassocl_lns .< dists_lns .< (out_lns ><< out_lns)
-         aux = assocr_lns .< (swap_lns ><< id_lns) .< assocl_lns
-         c :: Either (Either (One, One) (One,(a,[a]))) (Nat,One)
+   where h = ((!<) c -|-< subr_lns) .< coassocl_lns .< dists_lns .< (out_lns ><< out_lns)
+         --c :: One -> Either (Either (One, One) (One,(a,[a]))) (Nat,One)
          -- 1st option: do nothing
          -- 2nd option: append to the source list
          -- 3rd option: increment the source number by
-         c = Left (Left (_L,_L))
+         c = const $ Left (Left (_L,_L))     
 
 -- | List filtering lens.
 -- The argument passed to @snd_lns@ can be undefined because it will never be used
-filter_lns :: Lens [Either a b] [a]
-filter_lns = cata_lns _L ((inn_lns .\/< snd_lns _L) .< coassocl_lns .< (id_lns -|-< distl_lns))
+filter_left_lns :: Lens [Either a b] [a]
+filter_left_lns = cata_lns _L ((inn_lns .\/< snd_lns _L) .< coassocl_lns .< (id_lns -|-< distl_lns))
 
+filter_right_lns :: Lens [Either a b] [b]
+filter_right_lns = cata_lns _L ((inn_lns .\/< snd_lns _L) .< coassocl_lns .< (id_lns -|-< coswap_lns .< distl_lns))
+
 -- | Binary list concatenation.
 -- Lens hylomorphisms can be defined as the composition of a catamorphism after an anamorphism.
 cat_lns :: Lens ([a],[a]) [a]
 cat_lns = hylo_lns (_L :: NeList [a] a) g h
-    where g = inn_lns .< ((\/$<) out_lns)
-          h = (snd_lns _L -|-< assocr_lns) .< distl_lns .< (out_lns ><< id_lns)
+    where g = inn_lns .< (out_lns \/$< id_lns)
+          h = (snd_lns bang -|-< assocr_lns) .< distl_lns .< (out_lns ><< id_lns)
 
 -- | Binary list transposition.
 -- Binary version of @transpose@.
 transpose_lns :: Lens ([a],[a]) [a]
 transpose_lns = hylo_lns t g h
-    where g = inn_lns .< ((\/$<) out_lns)
+    where g = inn_lns .< (out_lns \/$< id_lns)
           h = (snd_lns _L -|-< (id_lns ><< swap_lns) .< assocr_lns) .< distl_lns .< (out_lns ><< id_lns)
           t = _L :: K [a] :+!: (K a :*!: I)
 
--- Integer addition
-add_lns :: Lens (Int,Int) Int
-add_lns = Lens get' put' create'
-    where get' (x,y) = x+y
-          put' (x,(a,b)) = (a,x-a)
-          -- needs to be strictly decreasing in the first argument, that will be the recursive argument of sumInt_lns
-          create' x | x > 0 = (div x 2 + mod x 2,div x 2)
-                    | otherwise = (div x 2,div x 2 + mod x 2)
-
--- | Sum of a list of integers.
-sumInt_lns :: Lens [Int] Int
-sumInt_lns = cata_lns _L ((0 !\/< add_lns) _L)
-
+-- | Addition of two natural numbers.
 plus_lns :: Lens (Nat,Nat) Nat
 plus_lns = hylo_lns (_L::From Nat) f g
-   where f = inn_lns .< ((\/$<) out_lns)
-         g = (snd_lns _L -|-< id_lns) .< distl_lns .< (out_lns ><< id_lns)
-
-sumNat_lns :: Lens [Nat] Nat
-sumNat_lns = cata_lns _L g
-    where g = inn_lns .< ((#\/<) (out_lns .< plus_lns))
+   where f = inn_lns .< (out_lns \/$< id_lns)
+         g = (snd_lns bang -|-< id_lns) .< distl_lns .< (out_lns ><< id_lns)
 
-type instance BF Tree = BConst One :+| (BPar :*| (BId :*| BId))
+suml_lns :: Lens [Nat] Nat
+suml_lns = cata_lns _L g
+    where g = inn_lns .< (id_lns #\/< (out_lns .< plus_lns))
 
--- | Flatten a tree.
-flatten_lns :: Lens (Tree a) [a]
-flatten_lns = cata_lns _L (inn_lns .< (id_lns -|-< id_lns ><< cat_lns))
+concatMap_lns :: Lens a [b] -> Lens [a] [b]
+concatMap_lns l = cata_lns _L f
+    where f = inn_lns .< (id_lns #\/< out_lns .< cat_lns .< (l ><< id_lns))
 
 -- | List concatenation.
 concat_lns :: Lens [[a]] [a]
-concat_lns = cata_lns _L (inn_lns .< (((id_lns .\/< id_lns) -|-< id_lns) .< coassocl_lns .< (id_lns -|-< out_lns .< cat_lns)))
+concat_lns = cata_lns _L (inn_lns .< (id_lns #\/< out_lns .< cat_lns))
 
+-- | Partitions a list of options into two lists.
+-- Note that this imposes some redefinement of the traditional definition in order to fit our framework.
+partition_lns :: Lens [Either a b] ([a],[b])
+partition_lns = cata_lns _L f where
+        f = (inn_lns ><< id_lns) .< undistl_lns .< ((!/\<) id_lns -|-< (id_lns ><< g) .< undistr_lns) .< coassocr_lns
+          .< ((inn_lns -|-< id_lns) .< coassocl_lns .< (id_lns -|-< (snd_lns _L -|-< id_lns) .< distl_lns .< (out_lns ><< id_lns) .< subr_lns) -|-< assocl_lns)
+          .< coswap_lns .< cosubr_lns .< (id_lns -|-< distl_lns)
+        g = inn_lns .< (out_lns \/$< id_lns) .< coswap_lns
+
 -- | List mapping lens.
 map_lns :: Lens c a -> Lens [c] [a]
 map_lns f = nat_lns _L (\x -> id_lns -|-< f ><< id_lns)
 
--- | Generic mapping example using user-defined concrete generators
-data T a = Fst a | Next (T a) deriving (Eq,Show)
+head_lns :: [a] -> Lens [a] (Either One a)
+head_lns l = (id_lns -|-< fst_lns (l!)) .< out_lns
 
-type instance BF T = BPar :+| BId
-type instance PF (T a) = Const a :+: Id
+tail_lns :: a -> Lens [a] (Either One [a])
+tail_lns v = (id_lns -|-< snd_lns (v!)) .< out_lns
 
-instance Mu (T a) where
-    inn (Left x) = Fst x
-    inn (Right x) = Next x
-    out (Fst x) = Left x
-    out (Next x) = Right x
+-- ** Reverse
 
-aux :: T a -> a
-aux (Fst x) = x
-aux (Next x) = aux x
+-- | Inserts an element at the end of a list, thus making it non-empty.
+snoc_lns :: Lens (a,[a]) (Some a)
+snoc_lns = hylo_lns (_L :: NeList a a) f g
+   where f = inn_lns
+         g = (fst_lns _L -|-< subr_lns) .< distr_lns .< (id_lns ><< out_lns)
 
-tmap_lns l = gmap_lns' (aux . snd) snd l
+-- | Isomorphism between a list and an optional non-empty list.
+toSome_lns :: Lens [a] (Either One (Some a))
+toSome_lns = cata_lns _L f
+    where f = (id_lns -|-< inn_lns) .< (id_lns -|-< (fst_lns _L -|-< id_lns) .< distr_lns)
 
-exampleT = put (tmap_lns (fst_lns 'c')) (Fst 1,(Next (Fst (2,'a'))))
+-- | Converts a list into a non-empty list.
+some_lns :: Eq a => a -> Lens [a] (Some a)
+some_lns c = (Wrap c !\/< id_lns) _L .< toSome_lns
 
+-- | Isomorphism between a list and an optional non-empty list.
+fromSome_lns :: Lens (Either One (Some a)) [a]
+fromSome_lns = ana_lns _L g
+    where g = (id_lns -|-< undistr_lns) .< (id_lns -|-< ((/\!<) id_lns  -|-< id_lns)) .< (id_lns -|-< out_lns)
+
+eitherNilSnoc :: Lens (Either One (a,[a])) [a]
+eitherNilSnoc = fromSome_lns .< (id_lns -|-< snoc_lns)
+
+-- | The list reversal lens is an isomorphism.
+reverse_lns :: Lens [a] [a]
+reverse_lns = cata_lns _L eitherNilSnoc
+
+-- * Non-natural lenses
+
+-- | List length using an accumulation (after simplification into an hylomorphism).
+-- Uses @Int@ instead of @Nat@ because @succ@ on @Nat@ is not a valid lens.
+len_lns :: Lens ([a],Int) Int
+len_lns = hylo_lns t g h
+    where g = id_lns .\/< id_lns
+          h = (snd_lns _L -|-< snd_lns _L .< assocr_lns .< (id_lns ><< inc_lns)) .< distl_lns .< (out_lns ><< id_lns)
+          t = _L :: K Int :+!: I
+
+-- Integer addition
+add_lns :: Lens (Int,Int) Int
+add_lns = Lens get' put' create'
+    where get' (x,y) = x+y
+          put' (x,(a,b)) = (a,x-a)
+          -- needs to be strictly decreasing in the first argument, that will be the recursive argument of sumInt_lns
+          create' x | x > 0 = (div x 2 + mod x 2,div x 2)
+                    | otherwise = (div x 2,div x 2 + mod x 2)
+
+-- | Sum of a list of integers.
+sumInt_lns :: Lens [Int] Int
+sumInt_lns = cata_lns _L ((0 !\/< add_lns) _L)
+
+-- | Incremental summation of a list.
+-- Since general splitting is not a lens, we need to provide user-defined put and create functions that serve our purpose and construct a valid lens.
+isum_lns :: Lens [Int] [Int]
+isum_lns = cata_lns _L f
+    where f = inn_lns .< (id_lns -|-< fstmapadd)
+          fstmapadd :: Lens (Int,[Int]) (Int,[Int])
+          fstmapadd = Lens get' put' create'
+            where get' = fst /\ (\(i,l) -> map (+i) l)
+                  put' = create' . fst
+                  create' (i,l) = (i,map (\x -> x-i) l)