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.4
+Version:         0.0.5
 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/Combinators.hs b/src/Generics/Pointless/Lenses/Combinators.hs
--- a/src/Generics/Pointless/Lenses/Combinators.hs
+++ b/src/Generics/Pointless/Lenses/Combinators.hs
@@ -119,38 +119,48 @@
           create' = (c!)
 
 -- | 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@.
 infix 4 !\/<
-(!\/<) :: Eq a => a -> Lens c a -> Lens (Either c b) a
-(!\/<) a f = Lens get' put' create'
+(!\/<) :: Eq a => a -> Lens b a -> c -> Lens (Either c b) a
+(!\/<) a f c = Lens get' put' create'
+    where get' = (a!) \/ get f
+          put' = (id \/ inr) . ((snd -|- create f . fst) -|- id) . ((((==a) . fst)?) -|- put f) . distr
+          create' = ((c!) -|- create f) . ((==a)?)
+          
+-- | The @f \/ (a!)@ point-free expression, where @a@ is a constant and @f@ a function.
+-- The additional argument of type @b@ is the default value when the view matches the constant of type @a@.
+infix 4 \/!<
+(\/!<) :: Eq a => a -> Lens c a -> b -> Lens (Either c b) a
+(\/!<) a f b = Lens get' put' create'
     where get' = get f \/ (a!)
           put' = (inl \/ coswap) . (id -|- (snd -|- create f . fst)) . (put f -|- (((==a) . fst)?)) . distr
-          create' = inl . create f
+          create' =  (create f -|- (b!)). ((==a)?)
 
--- | The @f \/ (a!)@ point-free expression, where @a@ is a constant and @f@ a function.
-infix 4 \/!<
-(\/!<) :: Eq a => a -> Lens b a -> Lens (Either c b) a
-(\/!<) a f = Lens get' put' create'
-    where get' = (a!) \/ get f
-          put' = (id \/ inr) . ((snd -|- create f . fst) -|- id) . ((((==a) . fst)?) -|- put f) . distr
-          create' = inr . create f
+-- | 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
 
+-- | 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
+
 -- * Point-free isomorphism combinators
 
 -- | The lens identity combinator.
 id_lns :: Lens c c
 id_lns = Lens id fst id
 
--- | The product distribution combinator
-distp :: ((c,d),(a,b)) -> ((c,a),(d,b))
-distp = fst >< fst /\ snd >< snd
-
 -- | The @distp@ point-free combinator.
 distp_lns :: Lens ((c,d),(a,b)) ((c,a),(d,b))
 distp_lns = Lens distp (distp . fst) distp
-
--- | The sum distribution combinator.
-dists :: (Either a b,Either c d) -> Either (Either (a,c) (a,d)) (Either (b,c) (b,d))
-dists = (distr -|- distr) . distl
 
 -- | The @dists@ point-free combinator.
 dists_lns :: Lens (Either a b,Either c d) (Either (Either (a,c) (a,d)) (Either (b,c) (b,d)))
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
@@ -22,44 +22,93 @@
 import Generics.Pointless.Fctrable
 import Generics.Pointless.Bifunctors
 import Generics.Pointless.Bifctrable
+import Generics.Pointless.Examples.Examples
 import Generics.Pointless.Lenses
 import Generics.Pointless.Lenses.Combinators
 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
+
 -- | List length lens.
 length_lns :: a -> Lens [a] Nat
 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
+
 -- | List zipping lens.
 -- The aux transformation is merely for simplifying the constant argument
-zip_lns :: Either (Either One (b,[b])) (a,[a]) -> Lens ([a],[b]) [(a,b)]
-zip_lns c = ana_lns _L (((!<) c .< aux -|-< distp_lns) .< coassocl_lns .< dists_lns .< (out_lns ><< out_lns))
+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])
+          -- 1st option: do nothing
+          -- 2nd option: append to the left source list
+          -- 3rd option: append to right source list
+          c = Left (Left _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)
+         -- 1st option: do nothing
+         -- 2nd option: append to the source list
+         -- 3rd option: increment the source number by
+         c = 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))
 
 -- | 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 = Lens get' put' create'
-    where get' = uncurry (++)
-          put' (l,(e,d)) = splitAt (length e) l
-          create' l = splitAt (length l `div` 2) l
+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)
 
-data Tree a = Empty | Node a (Tree a) (Tree a) deriving (Eq,Show)
+-- | 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)
+          h = (snd_lns _L -|-< (id_lns ><< swap_lns) .< assocr_lns) .< distl_lns .< (out_lns ><< id_lns)
+          t = _L :: K [a] :+!: (K a :*!: I)
 
-type instance BF Tree = BConst One :+| (BPar :*| (BId :*| BId))
+-- 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)
 
-type instance PF (Tree a) = Const One :+: (Const a :*: (Id :*: Id))
+-- | Sum of a list of integers.
+sumInt_lns :: Lens [Int] Int
+sumInt_lns = cata_lns _L ((0 !\/< add_lns) _L)
 
-instance Mu (Tree a) where
-   inn (Left _) = Empty
-   inn (Right (a,(b,c))) = Node a b c
-   out Empty = Left _L
-   out (Node a b c) = Right (a,(b,c))
+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))
+
+type instance BF Tree = BConst One :+| (BPar :*| (BId :*| BId))
 
 -- | Flatten a tree.
 flatten_lns :: Lens (Tree a) [a]
diff --git a/src/Generics/Pointless/Lenses/RecursionPatterns.hs b/src/Generics/Pointless/Lenses/RecursionPatterns.hs
--- a/src/Generics/Pointless/Lenses/RecursionPatterns.hs
+++ b/src/Generics/Pointless/Lenses/RecursionPatterns.hs
@@ -53,6 +53,10 @@
     where l = fzip f create \/ fmap (fixF f) (id /\ create) . fst
           r = fmap (fixF g) (id /\ create) . fst \/ fzip g create
 
+-- | The @hylo@ recursion pattern as the composition of a lens catamorphism after a lens anamorphism .
+hylo_lns :: (Mu b,Fctrable (PF b)) => b -> Lens (F b c) c -> Lens a (F b a) -> Lens a c
+hylo_lns b g h = cata_lns b g .< ana_lns b h
+
 -- | The @ana@ recursion pattern as a lens.
 -- For @ana_lns@ to be a well-behaved lens, we MUST prove termination of |get| for each instance.
 ana_lns :: (Mu b,Fctrable (PF b)) => b -> Lens a (F b a) -> Lens a b