diff --git a/DeepControl/Applicative.hs b/DeepControl/Applicative.hs
--- a/DeepControl/Applicative.hs
+++ b/DeepControl/Applicative.hs
@@ -1,7 +1,7 @@
 {-|
 Module      : DeepControl.Applicative
 Description : Enable deep level Applicative style programming.
-Copyright   : (C) 2015 KONISHI Yohsuke 
+Copyright   : (c) 2015 KONISHI Yohsuke 
 License     : BSD-style (see the LICENSE file in the distribution)
 Maintainer  : ocean0yohsuke@gmail.com
 Stability   : experimental
@@ -9,7 +9,6 @@
 
 This module enables you to program in applicative style for more __deeper__ level than the usual 'Control.Applicative' module expresses.
 You would soon realize exactly what __/more deeper level/__ means by reading the example codes in order, which are attached on the functions below.
-Note: all the braket-cover notation for Level-4 and Level-5 haven't been written yet.
 -}
 module DeepControl.Applicative (
     module Control.Applicative,
@@ -46,14 +45,19 @@
     -- ** bra-ket notation
     (|$>>>), (<<<$|), (|*>>>), (<<<*|),
     -- ** braket-cover notation
-    (|***), (***|),
-    (|-**), (|*-*), (|**-), (|--*), (|-*-), (|*--),
-    (-**|), (*-*|), (**-|), (--*|), (-*-|), (*--|),
+    (|***), 
+    (|-**), (|*-*), (|**-), 
+    (|--*), (|-*-), (|*--),
+    (***|),
+    (-**|), (*-*|), (**-|), 
+    (--*|), (-*-|), (*--|),
     -- ** sequnce notation
     (*>>>), (<<<*),
     -- ** sequnce-cover notation
-    (*-->), (-*->), (--*>), (**->), (*-*>), (-**>),
-    (<*--), (<-*-), (<--*), (<**-), (<*-*), (<-**),
+    (*-->), (-*->), (--*>), 
+    (**->), (*-*>), (-**>),
+    (<*--), (<-*-), (<--*), 
+    (<**-), (<*-*), (<-**),
 
     -- * Level-4
     -- ** cover notation
@@ -63,20 +67,50 @@
     (-***), (*-**), (**-*),
     -- ** bra-ket notation
     (|$>>>>), (<<<<$|), (|*>>>>), (<<<<*|),
+    -- ** braket-cover notation
+    (|****), 
+    (|-***), (|*-**), (|**-*), (|***-),  
+    (|--**), (|-*-*), (|*--*), (|*-*-), (|-**-), (|**--),
+    (|---*), (|--*-), (|-*--), (|*---),
+    (****|),
+    (-***|), (*-**|), (**-*|), (***-|),  
+    (--**|), (-*-*|), (*--*|), (*-*-|), (-**-|), (**--|),
+    (---*|), (--*-|), (-*--|), (*---|),
     -- ** sequnce notation
     (*>>>>), (<<<<*),
+    -- ** sequnce-cover notation
+    (<---*), (<--*-), (<-*--), (<*---),
+    (<--**), (<-*-*), (<*--*), (<*-*-), (<-**-), (<**--),
+    (<-***), (<*-**), (<**-*), (<***-),
+    (---*>), (--*->), (-*-->), (*--->),
+    (--**>), (-*-*>), (*--*>), (*-*->), (-**->), (**-->),
+    (-***>), (*-**>), (**-*>), (***->),
 
     -- * Level-5
     -- ** cover notation
     (*****:), 
     (----*), 
-    (---**), (--*-*), (-*--*),
-    (--***), (-*-**), (*--**), (*-*-*), (**--*),
+    (---**), (--*-*), (-*--*), (*---*),
+    (--***), (-*-**), (*--**), (*-*-*), (-**-*), (**--*),
     (-****), (*-***), (**-**), (***-*),
     -- ** bra-ket notation
     (|$>>>>>), (<<<<<$|), (|*>>>>>), (<<<<<*|),
+    -- ** braket-cover notation
+    (|-****), (|*-***), (|**-**), (|***-*), (|****-),
+    (|--***), (|-*-**), (|*--**), (|*-*-*), (|-**-*), (|**--*), (|**-*-), (|*-**-), (|-***-), (|***--),
+    (|---**), (|--*-*), (|-*--*), (|*---*), (|*--*-), (|-*-*-), (|--**-), (|-**--), (|*-*--), (|**---),
+    (|----*), (|---*-), (|--*--), (|-*---), (|*----),
+    (-****|), (*-***|), (**-**|), (***-*|), (****-|),
+    (--***|), (-*-**|), (*--**|), (*-*-*|), (-**-*|), (**--*|), (**-*-|), (*-**-|), (-***-|), (***--|),
+    (---**|), (--*-*|), (-*--*|), (*---*|), (*--*-|), (-*-*-|), (--**-|), (-**--|), (*-*--|), (**---|),
+    (----*|), (---*-|), (--*--|), (-*---|), (*----|),
     -- ** sequnce notation
     (*>>>>>), (<<<<<*),
+    -- ** sequnce-cover notation
+    (<----*), (<---*-), (<--*--), (<-*---), (<*----),
+    (<---**), (<--*-*), (<-*--*), (<*---*), (<*--*-), (<-*-*-), (<--**-), (<-**--), (<*-*--), (<**---),
+    (<--***), (<-*-**), (<*--**), (<*-*-*), (<-**-*), (<**--*), (<**-*-), (<*-**-), (<-***-), (<***--),
+    (<-****), (<*-***), (<**-**), (<***-*), (<****-),
 
     ) where 
 
@@ -87,7 +121,7 @@
 
 infixl 4  |>, <|
 
--- | Alias for @'$'@. 
+-- | Alias to @'$'@. 
 -- 
 -- >>> (1+) |> 2
 -- 3
@@ -172,11 +206,18 @@
 -- [3]
 -- >>> [1] <$|(+)|* 2 
 -- [3]
--- >>> [1] <$|(+)|* 2 <$|(*)|* 3
--- [9]
 --
--- >>> Just 1 <$|(,)|* 2 
--- Just (1,2)
+-- >>> (,) |$> ["a1","a2"] |* 'b'
+-- [("a1",'b'),("a2",'b')]
+--
+-- >>> (,,) 'a' |$> ["b1","b2"] |* 'c'
+-- [('a',"b1",'c'),('a',"b2",'c')]
+--
+-- >>> (,,,) 'a' |$> ["b1","b2"] |* 'c' |* 'd'
+-- [('a',"b1",'c','d'),('a',"b2",'c','d')]
+-- >>> (,,,) 'a' |$> ["b1","b2"] |* 'c' |*> ["d1","d2"]
+-- [('a',"b1",'c',"d1"),('a',"b1",'c',"d2"),('a',"b2",'c',"d1"),('a',"b2",'c',"d2")]
+--
 (|*) :: Applicative f => f (a -> b) -> a -> f b
 f |* x = f |*> (*:) x
 
@@ -406,9 +447,6 @@
 (|$>>>) = (|$>) . (|$>>)
 
 infixl 3  <<<$|, |*>>>, <<<*|
-infixl 3  |***, ***|
-infixl 3  |-**, |*-*, |**-, |--*, |-*-, |*--
-infixl 3  -**|, *-*|, **-|, --*|, -*-|, *--|
 (<<<$|) :: (Functor f1, Functor f2, Functor f3) => f1 (f2 (f3 a)) -> (a -> b) -> f1 (f2 (f3 b))
 (<<<$|) = flip (|$>>>)
 (|*>>>) :: (Applicative f1, Applicative f2, Applicative f3) => f1 (f2 (f3 (a -> b))) -> f1 (f2 (f3 a)) -> f1 (f2 (f3 b))
@@ -416,11 +454,13 @@
 (<<<*|) :: (Applicative f1, Applicative f2, Applicative f3) => f1 (f2 (f3 a)) -> f1 (f2 (f3 (a -> b))) -> f1 (f2 (f3 b))
 (<<<*|) = flip (|*>>>)
 
+infixl 3  |***, ***|
 (|***) :: (Applicative f1, Applicative f2, Applicative f3) => f1 (f2 (f3 (a -> b))) -> a -> f1 (f2 (f3 b))
 f |*** x = f |*>>> (***:) x
 (***|) :: (Applicative f1, Applicative f2, Applicative f3) => a -> f1 (f2 (f3 (a -> b))) -> f1 (f2 (f3 b))
 (***|)  = flip (|***)
 
+infixl 3  |-**, |*-*, |**-, |--*, |-*-, |*--
 (|-**) :: (Applicative f1, Applicative f2, Applicative f3) => f1 (f2 (f3 (a -> b))) -> f1 a -> f1 (f2 (f3 b))
 f |-** x = f |*>>> (-**) x
 (|*-*) :: (Applicative f1, Applicative f2, Applicative f3) => f1 (f2 (f3 (a -> b))) -> f2 a -> f1 (f2 (f3 b))
@@ -434,6 +474,7 @@
 (|-*-) :: (Applicative f1, Applicative f2, Applicative f3) => f1 (f2 (f3 (a -> b))) -> f1 (f3 a) -> f1 (f2 (f3 b))
 f |-*- x = f |*>>> (-*) x
 
+infixl 3  -**|, *-*|, **-|, --*|, -*-|, *--|
 (-**|) :: (Applicative f1, Applicative f2, Applicative f3) => f1 a -> f1 (f2 (f3 (a -> b))) -> f1 (f2 (f3 b))
 (-**|) = flip (|-**)
 (*-*|) :: (Applicative f1, Applicative f2, Applicative f3) => f2 a -> f1 (f2 (f3 (a -> b))) -> f1 (f2 (f3 b))
@@ -481,7 +522,7 @@
 (<-**) :: (Applicative f1, Applicative f2, Applicative f3) => f1 (f2 (f3 b)) -> f1 a -> f1 (f2 (f3 b))
 x <-** a = x <<<* (-**) a
 
--- -----------------------------------------------------------------------------
+--------------------------------------------------------------------------------
 -- Level-4 functions
 
 infixl 6  ****:
@@ -517,70 +558,191 @@
 (<<<<*|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 a))) -> f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f2 (f3 (f4 b)))
 (<<<<*|) = flip (|*>>>>)
 
+infixl 3  |****
+(|****) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 (a -> b)))) -> a -> f1 (f2 (f3 (f4 b)))
+f |**** x = f |*>>>> (****:) x
+infixl 3  |-***, |*-**, |**-*, |***-  
+(|-***) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 (a -> b)))) -> f1 a -> f1 (f2 (f3 (f4 b)))
+f |-*** x = f |*>>>> (-***) x
+(|*-**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 (a -> b)))) -> f2 a -> f1 (f2 (f3 (f4 b)))
+f |*-** x = f |*>>>> (*-**) x
+(|**-*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 (a -> b)))) -> f3 a -> f1 (f2 (f3 (f4 b)))
+f |**-* x = f |*>>>> (**-*) x
+(|***-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 (a -> b)))) -> f4 a -> f1 (f2 (f3 (f4 b)))
+f |***- x = f |*>>>> (***:) x
+infixl 3  |--**, |-*-*, |*--*, |*-*-, |-**-, |**--
+(|--**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f2 a) -> f1 (f2 (f3 (f4 b)))
+f |--** x = f |*>>>> (--**) x
+(|-*-*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f3 a) -> f1 (f2 (f3 (f4 b)))
+f |-*-* x = f |*>>>> (-*-*) x
+(|*--*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 (a -> b)))) -> f2 (f3 a) -> f1 (f2 (f3 (f4 b)))
+f |*--* x = f |*>>>> (*--*) x
+(|*-*-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 (a -> b)))) -> f2 (f4 a) -> f1 (f2 (f3 (f4 b)))
+f |*-*- x = f |*>>>> (*-*) x
+(|-**-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f4 a) -> f1 (f2 (f3 (f4 b)))
+f |-**- x = f |*>>>> (-**) x
+(|**--) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 (a -> b)))) -> f3 (f4 a) -> f1 (f2 (f3 (f4 b)))
+f |**-- x = f |*>>>> (**:) x
+infixl 3  |---*, |--*-, |-*--, |*---
+(|---*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f2 (f3 a)) -> f1 (f2 (f3 (f4 b)))
+f |---* x = f |*>>>> (---*) x
+(|--*-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f2 (f4 a)) -> f1 (f2 (f3 (f4 b)))
+f |--*- x = f |*>>>> (--*) x
+(|-*--) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f3 (f4 a)) -> f1 (f2 (f3 (f4 b)))
+f |-*-- x = f |*>>>> (-*) x
+(|*---) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 (a -> b)))) -> f2 (f3 (f4 a)) -> f1 (f2 (f3 (f4 b)))
+f |*--- x = f |*>>>> (*:) x
+
+infixl 3  ****|
+(****|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => a -> f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f2 (f3 (f4 b)))
+(****|)  = flip (|****)
+infixl 3  -***|, *-**|, **-*|, ***-|  
+
+(-***|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 a -> f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f2 (f3 (f4 b)))
+x -***| f = f |*>>>> (-***) x
+(*-**|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f2 a -> f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f2 (f3 (f4 b)))
+x *-**| f = f |*>>>> (*-**) x
+(**-*|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f3 a -> f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f2 (f3 (f4 b)))
+x **-*| f = f |*>>>> (**-*) x
+(***-|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f4 a -> f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f2 (f3 (f4 b)))
+x ***-| f = f |*>>>> (***:) x
+infixl 3  --**|, -*-*|, *--*|, *-*-|, -**-|, **--|
+(--**|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 a) -> f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f2 (f3 (f4 b)))
+x --**| f = f |*>>>> (--**) x
+(-*-*|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f3 a) -> f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f2 (f3 (f4 b)))
+x -*-*| f = f |*>>>> (-*-*) x
+(*--*|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f2 (f3 a) -> f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f2 (f3 (f4 b)))
+x *--*| f = f |*>>>> (*--*) x
+(*-*-|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f2 (f4 a) -> f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f2 (f3 (f4 b)))
+x *-*-| f = f |*>>>> (*-*) x
+(-**-|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f4 a) -> f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f2 (f3 (f4 b)))
+x -**-| f = f |*>>>> (-**) x
+(**--|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f3 (f4 a) -> f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f2 (f3 (f4 b)))
+x **--| f = f |*>>>> (**:) x
+infixl 3  ---*|, --*-|, -*--|, *---|
+(---*|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 a)) -> f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f2 (f3 (f4 b)))
+x ---*| f = f |*>>>> (---*) x
+(--*-|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f4 a)) -> f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f2 (f3 (f4 b)))
+x --*-| f = f |*>>>> (--*) x
+(-*--|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f3 (f4 a)) -> f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f2 (f3 (f4 b)))
+x -*--| f = f |*>>>> (-*) x
+(*---|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f2 (f3 (f4 a)) -> f1 (f2 (f3 (f4 (a -> b)))) -> f1 (f2 (f3 (f4 b)))
+x *---| f = f |*>>>> (*:) x
+
 infixl 5  <<<<*, *>>>>
 (*>>>>) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 a))) -> f1 (f2 (f3 (f4 b))) -> f1 (f2 (f3 (f4 b)))
 (*>>>>) = liftA2 (*>>>)
 (<<<<*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 a))) -> f1 (f2 (f3 (f4 b))) -> f1 (f2 (f3 (f4 a)))
 (<<<<*) = liftA2 (<<<*)
 
+infixl 5  <---*, <--*-, <-*--, <*---
+(<---*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 b))) -> f1 (f2 (f3 a)) -> f1 (f2 (f3 (f4 b)))
+x <---* a = x <<<<* (---*) a
+(<--*-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 b))) -> f1 (f2 (f4 a)) -> f1 (f2 (f3 (f4 b)))
+x <--*- a = x <<<<* (--*) a
+(<-*--) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 b))) -> f1 (f3 (f4 a)) -> f1 (f2 (f3 (f4 b)))
+x <-*-- a = x <<<<* (-*) a
+(<*---) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 b))) -> f2 (f3 (f4 a)) -> f1 (f2 (f3 (f4 b)))
+x <*--- a = x <<<<* (*:) a
+infixl 5  <--**, <-*-*, <*--*, <*-*-, <-**-, <**--
+(<--**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 b))) -> f1 (f2 a) -> f1 (f2 (f3 (f4 b)))
+x <--** a = x <<<<* (--**) a
+(<-*-*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 b))) -> f1 (f3 a) -> f1 (f2 (f3 (f4 b)))
+x <-*-* a = x <<<<* (-*-*) a
+(<*--*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 b))) -> f2 (f3 a) -> f1 (f2 (f3 (f4 b)))
+x <*--* a = x <<<<* (*--*) a
+(<*-*-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 b))) -> f2 (f4 a) -> f1 (f2 (f3 (f4 b)))
+x <*-*- a = x <<<<* (*-*) a
+(<-**-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 b))) -> f1 (f4 a) -> f1 (f2 (f3 (f4 b)))
+x <-**- a = x <<<<* (-**) a
+(<**--) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 b))) -> f3 (f4 a) -> f1 (f2 (f3 (f4 b)))
+x <**-- a = x <<<<* (**:) a
+infixl 5  <-***, <*-**, <**-*, <***-
+(<-***) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 b))) -> f1 a -> f1 (f2 (f3 (f4 b)))
+x <-*** a = x <<<<* (-***) a
+(<*-**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 b))) -> f2 a -> f1 (f2 (f3 (f4 b)))
+x <*-** a = x <<<<* (*-**) a
+(<**-*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 b))) -> f3 a -> f1 (f2 (f3 (f4 b)))
+x <**-* a = x <<<<* (**-*) a
+(<***-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 (f4 b))) -> f4 a -> f1 (f2 (f3 (f4 b)))
+x <***- a = x <<<<* (***:) a
+
+infixl 5  ---*>, --*->, -*-->, *--->
+(---*>) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f3 a)) -> f1 (f2 (f3 (f4 b))) -> f1 (f2 (f3 (f4 b)))
+a ---*> x = x <<<<* (---*) a
+(--*->) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 (f4 a)) -> f1 (f2 (f3 (f4 b))) -> f1 (f2 (f3 (f4 b)))
+a --*-> x = x <<<<* (--*) a
+(-*-->) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f3 (f4 a)) -> f1 (f2 (f3 (f4 b))) -> f1 (f2 (f3 (f4 b)))
+a -*--> x = x <<<<* (-*) a
+(*--->) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f2 (f3 (f4 a)) -> f1 (f2 (f3 (f4 b))) -> f1 (f2 (f3 (f4 b)))
+a *---> x = x <<<<* (*:) a
+infixl 5  --**>, -*-*>, *--*>, *-*->, -**->, **-->
+(--**>) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f2 a) -> f1 (f2 (f3 (f4 b))) -> f1 (f2 (f3 (f4 b)))
+a --**> x = x <<<<* (--**) a
+(-*-*>) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f3 a) -> f1 (f2 (f3 (f4 b))) -> f1 (f2 (f3 (f4 b)))
+a -*-*> x = x <<<<* (-*-*) a
+(*--*>) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f2 (f3 a) -> f1 (f2 (f3 (f4 b))) -> f1 (f2 (f3 (f4 b)))
+a *--*> x = x <<<<* (*--*) a
+(*-*->) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f2 (f4 a) -> f1 (f2 (f3 (f4 b))) -> f1 (f2 (f3 (f4 b)))
+a *-*-> x = x <<<<* (*-*) a
+(-**->) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 (f4 a) -> f1 (f2 (f3 (f4 b))) -> f1 (f2 (f3 (f4 b)))
+a -**-> x = x <<<<* (-**) a
+(**-->) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f3 (f4 a) -> f1 (f2 (f3 (f4 b))) -> f1 (f2 (f3 (f4 b)))
+a **--> x = x <<<<* (**:) a
+infixl 5  -***>, *-**>, **-*>, ***->
+(-***>) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f1 a -> f1 (f2 (f3 (f4 b))) -> f1 (f2 (f3 (f4 b)))
+a -***> x = x <<<<* (-***) a
+(*-**>) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f2 a -> f1 (f2 (f3 (f4 b))) -> f1 (f2 (f3 (f4 b)))
+a *-**> x = x <<<<* (*-**) a
+(**-*>) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f3 a -> f1 (f2 (f3 (f4 b))) -> f1 (f2 (f3 (f4 b)))
+a **-*> x = x <<<<* (**-*) a
+(***->) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4) => f4 a -> f1 (f2 (f3 (f4 b))) -> f1 (f2 (f3 (f4 b)))
+a ***-> x = x <<<<* (***:) a
+
 -- -----------------------------------------------------------------------------
 -- Level-5 functions
 
 infixl 6  *****:
-(*****:) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => 
-            a -> f1 (f2 (f3 (f4 (f5 a))))
+(*****:) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => a -> f1 (f2 (f3 (f4 (f5 a))))
 (*****:) = (*:) . (****:)
 infixl 6  ----*
-(----*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => 
-            f1 (f2 (f3 (f4 a))) -> f1 (f2 (f3 (f4 (f5 a))))
+(----*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 a))) -> f1 (f2 (f3 (f4 (f5 a))))
 (----*) = ((---*)|$>)
-infixl 6  ---**, --*-*, -*--*
-(---**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => 
-            f1 (f2 (f3 a)) -> f1 (f2 (f3 (f4 (f5 a))))
+infixl 6  ---**, --*-*, -*--*, *---*
+(---**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 a)) -> f1 (f2 (f3 (f4 (f5 a))))
 (---**) = ((**:)|$>>>)
-(--*-*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => 
-            f1 (f2 (f4 a)) -> f1 (f2 (f3 (f4 (f5 a))))
+(--*-*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f4 a)) -> f1 (f2 (f3 (f4 (f5 a))))
 (--*-*) = (----*) . (--*)
-(-*--*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => 
-            f1 (f3 (f4 a)) -> f1 (f2 (f3 (f4 (f5 a))))
+(-*--*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f3 (f4 a)) -> f1 (f2 (f3 (f4 (f5 a))))
 (-*--*) = (----*) . (-*)
-(*---*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => 
-            f2 (f3 (f4 a)) -> f1 (f2 (f3 (f4 (f5 a))))
+(*---*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f2 (f3 (f4 a)) -> f1 (f2 (f3 (f4 (f5 a))))
 (*---*) = (----*) . (*:)
-infixl 6  --***, -*-**, *--**, *-*-*, **--*
-(--***) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => 
-            f1 (f2 a) -> f1 (f2 (f3 (f4 (f5 a))))
+infixl 6  --***, -*-**, *--**, *-*-*, -**-*, **--*
+(--***) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 a) -> f1 (f2 (f3 (f4 (f5 a))))
 (--***) = ((-***)|$>)
-(-*-**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => 
-            f1 (f3 a) -> f1 (f2 (f3 (f4 (f5 a))))
+(-*-**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f3 a) -> f1 (f2 (f3 (f4 (f5 a))))
 (-*-**) = (---**) . (-*)
-(*--**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => 
-            f2 (f3 a) -> f1 (f2 (f3 (f4 (f5 a))))
+(*--**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f2 (f3 a) -> f1 (f2 (f3 (f4 (f5 a))))
 (*--**) = (---**) . (*:)
-(*-*-*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => 
-            f2 (f4 a) -> f1 (f2 (f3 (f4 (f5 a))))
+(*-*-*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f2 (f4 a) -> f1 (f2 (f3 (f4 (f5 a))))
 (*-*-*) = (----*) . (*-*)
-(**--*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => 
-            f3 (f4 a) -> f1 (f2 (f3 (f4 (f5 a))))
+(-**-*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f4 a) -> f1 (f2 (f3 (f4 (f5 a))))
+(-**-*) = (----*) . (-**)
+(**--*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f3 (f4 a) -> f1 (f2 (f3 (f4 (f5 a))))
 (**--*) = (----*) . (**:)
 infixl 6  -****, *-***, **-**, ***-*
-(-****) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => 
-            f1 a -> f1 (f2 (f3 (f4 (f5 a))))
+(-****) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 a -> f1 (f2 (f3 (f4 (f5 a))))
 (-****) = ((****:)|$>)
-(*-***) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => 
-            f2 a -> f1 (f2 (f3 (f4 (f5 a))))
+(*-***) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f2 a -> f1 (f2 (f3 (f4 (f5 a))))
 (*-***) = (--***) . (*:)
-(**-**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => 
-            f3 a -> f1 (f2 (f3 (f4 (f5 a))))
+(**-**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f3 a -> f1 (f2 (f3 (f4 (f5 a))))
 (**-**) = (---**) . (**:)
-(***-*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => 
-            f4 a -> f1 (f2 (f3 (f4 (f5 a))))
+(***-*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f4 a -> f1 (f2 (f3 (f4 (f5 a))))
 (***-*) = (----*) . (***:)
 
 infixl 4  |$>>>>>
 (|$>>>>>) :: (Functor f1, Functor f2, Functor f3, Functor f4, Functor f5) => (a -> b) -> f1 (f2 (f3 (f4 (f5 a)))) -> f1 (f2 (f3 (f4 (f5 b))))
 (|$>>>>>) = (|$>) . (|$>>>>)
-
 infixl 3  <<<<<$|, |*>>>>>, <<<<<*|
 (<<<<<$|) :: (Functor f1, Functor f2, Functor f3, Functor f4, Functor f5) => f1 (f2 (f3 (f4 (f5 a)))) -> (a -> b) -> f1 (f2 (f3 (f4 (f5 b))))
 (<<<<<$|) = flip (|$>>>>>)
@@ -589,9 +751,204 @@
 (<<<<<*|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 a)))) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
 (<<<<<*|) = flip (|*>>>>>)
 
+infixl 3  |-****, |*-***, |**-**, |***-*, |****-
+(|-****) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 a -> f1 (f2 (f3 (f4 (f5 b))))
+f |-**** x = f |*>>>>> (-****) x
+(|*-***) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f2 a -> f1 (f2 (f3 (f4 (f5 b))))
+f |*-*** x = f |*>>>>> (*-***) x
+(|**-**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f3 a -> f1 (f2 (f3 (f4 (f5 b))))
+f |**-** x = f |*>>>>> (**-**) x
+(|***-*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f4 a -> f1 (f2 (f3 (f4 (f5 b))))
+f |***-* x = f |*>>>>> (***-*) x
+(|****-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f5 a -> f1 (f2 (f3 (f4 (f5 b))))
+f |****- x = f |*>>>>> (****:) x
+infixl 3  |--***, |-*-**, |*--**, |*-*-*, |-**-*, |**--*, |**-*-, |*-**-, |-***-, |***--
+(|--***) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 a) -> f1 (f2 (f3 (f4 (f5 b))))
+f |--*** x = f |*>>>>> (--***) x
+(|-*-**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f3 a) -> f1 (f2 (f3 (f4 (f5 b))))
+f |-*-** x = f |*>>>>> (-*-**) x
+(|*--**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f2 (f3 a) -> f1 (f2 (f3 (f4 (f5 b))))
+f |*--** x = f |*>>>>> (*--**) x
+(|*-*-*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f2 (f4 a) -> f1 (f2 (f3 (f4 (f5 b))))
+f |*-*-* x = f |*>>>>> (*-*-*) x
+(|-**-*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f4 a) -> f1 (f2 (f3 (f4 (f5 b))))
+f |-**-* x = f |*>>>>> (-**-*) x
+(|**--*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f3 (f4 a) -> f1 (f2 (f3 (f4 (f5 b))))
+f |**--* x = f |*>>>>> (**--*) x
+(|**-*-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f3 (f5 a) -> f1 (f2 (f3 (f4 (f5 b))))
+f |**-*- x = f |*>>>>> (**-*) x
+(|*-**-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f2 (f5 a) -> f1 (f2 (f3 (f4 (f5 b))))
+f |*-**- x = f |*>>>>> (*-**) x
+(|-***-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f5 a) -> f1 (f2 (f3 (f4 (f5 b))))
+f |-***- x = f |*>>>>> (-***) x
+(|***--) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f4 (f5 a) -> f1 (f2 (f3 (f4 (f5 b))))
+f |***-- x = f |*>>>>> (***:) x
+infixl 3  |---**, |--*-*, |-*--*, |*---*, |*--*-, |-*-*-, |--**-, |-**--, |*-*--, |**---
+(|---**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+f |---** x = f |*>>>>> (---**) x
+(|--*-*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f4 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+f |--*-* x = f |*>>>>> (--*-*) x
+(|-*--*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f3 (f4 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+f |-*--* x = f |*>>>>> (-*--*) x
+(|*---*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f2 (f3 (f4 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+f |*---* x = f |*>>>>> (*---*) x
+(|*--*-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f2 (f3 (f5 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+f |*--*- x = f |*>>>>> (*--*) x
+(|-*-*-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f3 (f5 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+f |-*-*- x = f |*>>>>> (-*-*) x
+(|--**-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f5 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+f |--**- x = f |*>>>>> (--**) x
+(|-**--) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f4 (f5 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+f |-**-- x = f |*>>>>> (-**) x
+(|*-*--) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f2 (f4 (f5 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+f |*-*-- x = f |*>>>>> (*-*) x
+(|**---) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f3 (f4 (f5 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+f |**--- x = f |*>>>>> (**:) x
+infixl 3  |----*, |---*-, |--*--, |-*---, |*----
+(|----*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 a))) -> f1 (f2 (f3 (f4 (f5 b))))
+f |----* x = f |*>>>>> (----*) x
+(|---*-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f5 a))) -> f1 (f2 (f3 (f4 (f5 b))))
+f |---*- x = f |*>>>>> (---*) x
+(|--*--) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f4 (f5 a))) -> f1 (f2 (f3 (f4 (f5 b))))
+f |--*-- x = f |*>>>>> (--*) x
+(|-*---) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f3 (f4 (f5 a))) -> f1 (f2 (f3 (f4 (f5 b))))
+f |-*--- x = f |*>>>>> (-*) x
+(|*----) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f2 (f3 (f4 (f5 a))) -> f1 (f2 (f3 (f4 (f5 b))))
+f |*---- x = f |*>>>>> (*:) x
+
+infixl 3  -****|, *-***|, **-**|, ***-*|, ****-|
+(-****|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 a -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x -****| f = f |*>>>>> (-****) x
+(*-***|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f2 a -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x *-***| f = f |*>>>>> (*-***) x
+(**-**|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f3 a -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x **-**| f = f |*>>>>> (**-**) x
+(***-*|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f4 a -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x ***-*| f = f |*>>>>> (***-*) x
+(****-|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f5 a -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x ****-| f = f |*>>>>> (****:) x
+infixl 3  --***|, -*-**|, *--**|, *-*-*|, -**-*|, **--*|, **-*-|, *-**-|, -***-|, ***--| 
+(--***|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 a) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x --***| f = f |*>>>>> (--***) x
+(-*-**|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f3 a) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x -*-**| f = f |*>>>>> (-*-**) x
+(*--**|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f2 (f3 a) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x *--**| f = f |*>>>>> (*--**) x
+(*-*-*|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f2 (f4 a) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x *-*-*| f = f |*>>>>> (*-*-*) x
+(-**-*|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f4 a) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x -**-*| f = f |*>>>>> (-**-*) x
+(**--*|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f3 (f4 a) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x **--*| f = f |*>>>>> (**--*) x
+(**-*-|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f3 (f5 a) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x **-*-| f = f |*>>>>> (**-*) x
+(*-**-|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f2 (f5 a) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x *-**-| f = f |*>>>>> (*-**) x
+(-***-|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f5 a) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x -***-| f = f |*>>>>> (-***) x
+(***--|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f4 (f5 a) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x ***--| f = f |*>>>>> (***:) x
+infixl 3  ---**|, --*-*|, -*--*|, *---*|, *--*-|, -*-*-|, --**-|, -**--|, *-*--|, **---|
+(---**|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 a)) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x ---**| f = f |*>>>>> (---**) x
+(--*-*|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f4 a)) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x --*-*| f = f |*>>>>> (--*-*) x
+(-*--*|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f3 (f4 a)) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x -*--*| f = f |*>>>>> (-*--*) x
+(*---*|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f2 (f3 (f4 a)) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x *---*| f = f |*>>>>> (*---*) x
+(*--*-|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f2 (f3 (f5 a)) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x *--*-| f = f |*>>>>> (*--*) x
+(-*-*-|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f3 (f5 a)) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x -*-*-| f = f |*>>>>> (-*-*) x
+(--**-|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f5 a)) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x --**-| f = f |*>>>>> (--**) x
+(-**--|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f4 (f5 a)) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x -**--| f = f |*>>>>> (-**) x
+(*-*--|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f2 (f4 (f5 a)) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x *-*--| f = f |*>>>>> (*-*) x
+(**---|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f3 (f4 (f5 a)) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x **---| f = f |*>>>>> (**:) x
+infixl 3  ----*|, ---*-|, --*--|, -*---|, *----|
+(----*|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 a))) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x ----*| f = f |*>>>>> (----*) x
+(---*-|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f5 a))) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x ---*-| f = f |*>>>>> (---*) x
+(--*--|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f4 (f5 a))) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x --*--| f = f |*>>>>> (--*) x
+(-*---|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f3 (f4 (f5 a))) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x -*---| f = f |*>>>>> (-*) x
+(*----|) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f2 (f3 (f4 (f5 a))) -> f1 (f2 (f3 (f4 (f5 (a -> b))))) -> f1 (f2 (f3 (f4 (f5 b))))
+x *----| f = f |*>>>>> (*:) x
+
 infixl 5  <<<<<*, *>>>>>
 (*>>>>>) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 a)))) -> f1 (f2 (f3 (f4 (f5 b)))) -> f1 (f2 (f3 (f4 (f5 b))))
 (*>>>>>) = liftA2 (*>>>>)
 (<<<<<*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 a)))) -> f1 (f2 (f3 (f4 (f5 b)))) -> f1 (f2 (f3 (f4 (f5 a))))
 (<<<<<*) = liftA2 (<<<<*)
+
+infixl 5  <----*, <---*-, <--*--, <-*---, <*----
+(<----*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f1 (f2 (f3 (f4 a))) -> f1 (f2 (f3 (f4 (f5 b))))
+x <----* a = x <<<<<* (----*) a
+(<---*-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f1 (f2 (f3 (f5 a))) -> f1 (f2 (f3 (f4 (f5 b))))
+x <---*- a = x <<<<<* (---*) a
+(<--*--) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f1 (f2 (f4 (f5 a))) -> f1 (f2 (f3 (f4 (f5 b))))
+x <--*-- a = x <<<<<* (--*) a
+(<-*---) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f1 (f3 (f4 (f5 a))) -> f1 (f2 (f3 (f4 (f5 b))))
+x <-*--- a = x <<<<<* (-*) a
+(<*----) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f2 (f3 (f4 (f5 a))) -> f1 (f2 (f3 (f4 (f5 b))))
+x <*---- a = x <<<<<* (*:) a
+infixl 5  <---**, <--*-*, <-*--*, <*---*, <*--*-, <-*-*-, <--**-, <-**--, <*-*--, <**---
+(<---**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f1 (f2 (f3 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+x <---** a = x <<<<<* (---**) a
+(<--*-*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f1 (f2 (f4 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+x <--*-* a = x <<<<<* (--*-*) a
+(<-*--*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f1 (f3 (f4 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+x <-*--* a = x <<<<<* (-*--*) a
+(<*---*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f2 (f3 (f4 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+x <*---* a = x <<<<<* (*---*) a
+(<*--*-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f2 (f3 (f5 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+x <*--*- a = x <<<<<* (*--*) a
+(<-*-*-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f1 (f3 (f5 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+x <-*-*- a = x <<<<<* (-*-*) a
+(<--**-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f1 (f2 (f5 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+x <--**- a = x <<<<<* (--**) a
+(<-**--) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f1 (f4 (f5 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+x <-**-- a = x <<<<<* (-**) a
+(<*-*--) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f2 (f4 (f5 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+x <*-*-- a = x <<<<<* (*-*) a
+(<**---) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f3 (f4 (f5 a)) -> f1 (f2 (f3 (f4 (f5 b))))
+x <**--- a = x <<<<<* (**:) a
+infixl 5  <--***, <-*-**, <*--**, <*-*-*, <-**-*, <**--*, <**-*-, <*-**-, <-***-, <***--
+(<--***) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f1 (f2 a) -> f1 (f2 (f3 (f4 (f5 b))))
+x <--*** a = x <<<<<* (--***) a
+(<-*-**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f1 (f3 a) -> f1 (f2 (f3 (f4 (f5 b))))
+x <-*-** a = x <<<<<* (-*-**) a
+(<*--**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f2 (f3 a) -> f1 (f2 (f3 (f4 (f5 b))))
+x <*--** a = x <<<<<* (*--**) a
+(<*-*-*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f2 (f4 a) -> f1 (f2 (f3 (f4 (f5 b))))
+x <*-*-* a = x <<<<<* (*-*-*) a
+(<-**-*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f1 (f4 a) -> f1 (f2 (f3 (f4 (f5 b))))
+x <-**-* a = x <<<<<* (-**-*) a
+(<**--*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f3 (f4 a) -> f1 (f2 (f3 (f4 (f5 b))))
+x <**--* a = x <<<<<* (**--*) a
+(<**-*-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f3 (f5 a) -> f1 (f2 (f3 (f4 (f5 b))))
+x <**-*- a = x <<<<<* (**-*) a
+(<*-**-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f2 (f5 a) -> f1 (f2 (f3 (f4 (f5 b))))
+x <*-**- a = x <<<<<* (*-**) a
+(<-***-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f1 (f5 a) -> f1 (f2 (f3 (f4 (f5 b))))
+x <-***- a = x <<<<<* (-***) a
+(<***--) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f4 (f5 a) -> f1 (f2 (f3 (f4 (f5 b))))
+x <***-- a = x <<<<<* (***:) a
+infixl 5  <-****, <*-***, <**-**, <***-*, <****-
+(<-****) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f1 a -> f1 (f2 (f3 (f4 (f5 b))))
+x <-**** a = x <<<<<* (-****) a
+(<*-***) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f2 a -> f1 (f2 (f3 (f4 (f5 b))))
+x <*-*** a = x <<<<<* (*-***) a
+(<**-**) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f3 a -> f1 (f2 (f3 (f4 (f5 b))))
+x <**-** a = x <<<<<* (**-**) a
+(<***-*) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f4 a -> f1 (f2 (f3 (f4 (f5 b))))
+x <***-* a = x <<<<<* (***-*) a
+(<****-) :: (Applicative f1, Applicative f2, Applicative f3, Applicative f4, Applicative f5) => f1 (f2 (f3 (f4 (f5 b)))) -> f5 a -> f1 (f2 (f3 (f4 (f5 b))))
+x <****- a = x <<<<<* (****:) a
 
diff --git a/DeepControl/Arrow.hs b/DeepControl/Arrow.hs
--- a/DeepControl/Arrow.hs
+++ b/DeepControl/Arrow.hs
@@ -2,7 +2,7 @@
 Module      : DeepControl.Arrow
 Description : Enable deep level Arrow programming.
 Copyright   : (c) Ross Paterson 2002,
-              (C) 2015 KONISHI Yohsuke 
+              (c) 2015 KONISHI Yohsuke 
 License     : BSD-style (see the LICENSE file in the distribution)
 Maintainer  : ocean0yohsuke@gmail.com
 Stability   : experimental
diff --git a/DeepControl/Commutative.hs b/DeepControl/Commutative.hs
--- a/DeepControl/Commutative.hs
+++ b/DeepControl/Commutative.hs
@@ -1,8 +1,8 @@
 {-|
 Module      : DeepControl.Commutative
-Description : Commutative Functor.
+Description : ---
 Copyright   : Conor McBride and Ross Paterson 2005,
-              (C) 2015 KONISHI Yohsuke 
+              (c) 2015 KONISHI Yohsuke 
 License     : BSD-style (see the LICENSE file in the distribution)
 Maintainer  : ocean0yohsuke@gmail.com
 Stability   : experimental
@@ -10,43 +10,57 @@
 
 This module is made of @'Data.Traversable'@, distilling most function names polluted with action kind of concepts into crystalized(static) ones.
 -}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
 module DeepControl.Commutative (
-    -- * Level-1
-    -- ** The 'Commutative' class
+    -- * The 'Commutative' class
     Commutative(..),
-    -- ** Utility functions
+    -- * Utility functions
     cmap,
     cfor,
-    -- ** General definitions for superclass methods
+    -- * General definitions for superclass methods
     fmapDefault,
     foldMapDefault,
 
-    -- * Level-2
+    -- * Utility functions 2
+    -- ** Level-2
     sink2, float2,
-
-    -- * Level-3
+    -- ** Level-3
     sink3, float3,
-
-    -- * Level-4
+    -- ** Level-4
     sink4, float4,
-
-    -- * Level-5
+    -- ** Level-5
     sink5, float5,
 
     ) where 
 
 import DeepControl.Applicative
-
 import Data.Monoid
 
+import Control.Monad.Identity (Identity(..))
+import Control.Monad.Except (Except, ExceptT(..), runExcept)
+import Control.Monad.Writer (Writer, WriterT(..), runWriter)
+
 ------------------------------------------------------------------------------
 -- Level-1
 
--- | 
+-- | [], Maybe, Either, Except and Writer are all commutative each other.
+--   So these monads can be deepened to Monad2, Monad3, Monad4 and Monad5.
 -- 
 class (Applicative c) => Commutative c where
-  -- | This method is equivalent for @'Data.Traversable.sequenceA'@ just except the name.
+  -- | This method is equivalent for @'Data.Traversable.sequenceA'@ except the name.
   --   The only difference is the name "commute", that is to say from which no action kind of concepts smell.
+  --
+  -- >>> commute $ Just [1]
+  -- [Just 1]
+  -- >>> commute $ [Just 1]
+  -- Just [1]
+  --
+  -- >>> commute $ Right (Just 1)
+  -- Just (Right 1)
+  -- >>> commute $ Just (Right 1)
+  -- Right (Just 1)
+  --
   commute :: Applicative f => c (f a) -> f (c a)
 
 -- | Do @fmap f@ then commute, equivalent for @'Data.Traversable.traverse'@.
@@ -63,11 +77,23 @@
 instance Commutative [] where
     commute = foldr (\x acc -> x <$|(:)|*> acc) ((*:) [])
   
+instance (Monoid w) => Commutative (Writer w) where
+    commute x = 
+        let (a, b) = runWriter x
+        in  (WriterT . Identity) |$> (a <$|(,)|* b)
+
 instance Commutative (Either a) where
     commute (Right x) = Right |$> x
     commute (Left x)  = (*:) $ Left x
+instance Commutative (Except e) where
+    commute x = ExceptT . Identity |$> commute (runExcept x)
 
 {-
+instance Commutative (Const m) where
+    commute (Const m) = (*:) $ Const m
+-}
+
+{-
 instance Commutative ((->) r) where
     -- TODO: If GHC could parse this expression, maybe I could write up DeepControl.Monad.
     commute ((r->) mv) = (r->) |$> mv
@@ -95,10 +121,20 @@
 ------------------------------------------------------------------------------
 -- Level-2
 
+-- | sink2 = (commute|$>) . commute
+--
+-- >>> sink2 $ Right (Just [1])
+-- Just [Right 1]
+--
 sink2 :: (Commutative m1, Commutative m2, Applicative m3) => 
          m1 (m2 (m3 a)) -> m2 (m3 (m1 a))
 sink2 = (commute|$>) . commute
 
+-- | float2 = commute . (commute|$>)
+--
+-- >>> float2 $ Just [Right 1]
+-- Right (Just [1])
+--
 float2 :: (Applicative m1, Commutative m2, Commutative m3) => 
           m2 (m3 (m1 a)) -> m1 (m2 (m3 a))
 float2 = commute . (commute|$>)
@@ -106,10 +142,20 @@
 ------------------------------------------------------------------------------
 -- Level-3
 
+-- | sink3 = (sink2|$>) . commute
+--
+-- >>> sink3 $ Right [Just [1]]
+-- [Just [Right 1]]
+--
 sink3 :: (Commutative m1, Commutative m2, Commutative m3, Applicative m4) => 
          m1 (m2 (m3 (m4 a))) -> m2 (m3 (m4 (m1 a)))
 sink3 = (sink2|$>) . commute
 
+-- | float3 = commute . (float2|$>)
+--
+-- >>> float3 $ [Just [Right 1]]
+-- Right [Just [1]]
+--
 float3 :: (Applicative m1, Commutative m2, Commutative m3, Commutative m4) => 
           m2 (m3 (m4 (m1 a))) -> m1 (m2 (m3 (m4 a)))
 float3 = commute . (float2|$>)
diff --git a/DeepControl/Monad.hs b/DeepControl/Monad.hs
--- a/DeepControl/Monad.hs
+++ b/DeepControl/Monad.hs
@@ -1,7 +1,7 @@
 {-|
 Module      : DeepControl.Monad
 Description : Enable deep level Monad programming.
-Copyright   : (C) 2015 KONISHI Yohsuke 
+Copyright   : (c) 2015 KONISHI Yohsuke 
 License     : BSD-style (see the LICENSE file in the distribution)
 Maintainer  : ocean0yohsuke@gmail.com
 Stability   : experimental
@@ -12,8 +12,8 @@
 
 Note: 
 
-    * This module never make mlt(monad-transformer-library) unnessasary. 
-      The range in which this module is helpful is regrettably confined to the range that the instances of deep Monads (namely Monad2, Monad3, etc) define.
+    * This module never makes mlt(monad-transformer-library) unnessasary. 
+      The range in which this module is helpful is regrettably confined to the range of deep monads (namely Monad2, Monad3, etc).
     
     * In my opinion this bad confinement is hard-wired with the ability of the compiler, that is to say GHC doesn't parse @(r->)@ or @((->) r)@ as a data constructor; 
       thus some fundamental expressions such as @(r->)|$>@ or @fmap (r->)@ are useless.
@@ -24,42 +24,67 @@
     module Control.Monad,
 
     -- * Level-0
-    -- ** bind function
+    -- ** bind 
     (-<), (>-), 
-    -- ** composite function
+    -- ** composite 
     (>->), (<-<),
 
-    -- * Level-1
-    -- ** bind-sequence function
-    (<<),
-
     -- * Level-2
+    -- ** bind
     Monad2(..),
-    -- ** bind-sequence function
-    (>>~), (>-==), (->==), (>-~), (->~),
-    -- ** composite function
+    -- ** sequence
+    (>>~), 
+    -- ** bind-cover
+    (>-==), (->==), 
+    -- ** sequence-cover
+    (>-~), (->~),
+    -- ** composite 
     (>==>), 
 
     -- * Level-3
-    Monad3(..),
-    -- ** bind-sequence function
+    -- ** bind
+    Monad3(..),  
+    -- ** sequence
+    (>>>~),
+    -- ** bind-cover 
     (>>-==), (->>==), (>->==) ,(>--==),(->-==), (-->==), 
-    (>>>~), (->-~), (-->~), (>>-~), (->>~), (>->~), (>--~),
-    -- ** composite function
+    -- ** sequence-cover 
+    (>--~), (->-~), (-->~), (>>-~), (->>~), (>->~), 
+    -- ** composite 
     (>===>),
 
     -- * Level-4
-    Monad4(..),
-    -- ** bind-sequence function
+    -- ** bind
+    Monad4(..), 
+    -- ** sequence
     (>>>>~), 
-    -- ** composite function
+    -- ** bind-cover 
+    (--->==), (-->-==), (->--==), (>---==),
+    (-->>==), (->->==), (>-->==), (>->-==), (->>-==), (>>--==),
+    (->>>==), (>->>==), (>>->==), (>>>-==),
+    -- ** sequence-cover 
+    (--->~), (-->-~), (->--~), (>---~),
+    (-->>~), (->->~), (>-->~), (>->-~), (->>-~), (>>--~),
+    (->>>~), (>->>~), (>>->~), (>>>-~),
+    -- ** composite 
     (>====>), 
 
     -- * Level-5
-    Monad5(..),
-    -- ** bind-sequence function
+    -- ** bind
+    Monad5(..), 
+    -- ** sequence
     (>>>>>~), 
-    -- ** composite function
+    -- ** bind-cover 
+    (---->==), (--->-==), (-->--==), (->---==), (>----==),
+    (--->>==), (-->->==), (->-->==), (>--->==), (>-->-==), (->->-==), (-->>-==), (->>--==), (>->--==), (>>---==),
+    (-->>>==), (->->>==), (>-->>==), (>->->==), (->>->==), (>>-->==), (>>->-==), (>->>-==), (->>>-==), (>>>--==),
+    (->>>>==), (>->>>==), (>>->>==), (>>>->==), (>>>>-==),
+    -- ** sequence-cover 
+    (---->~), (--->-~), (-->--~), (->---~), (>----~),
+    (--->>~), (-->->~), (->-->~), (>--->~), (>-->-~), (->->-~), (-->>-~), (->>--~), (>->--~), (>>---~),
+    (-->>>~), (->->>~), (>-->>~), (>->->~), (->>->~), (>>-->~), (>>->-~), (>->>-~), (->>>-~), (>>>--~),
+    (->>>>~), (>->>>~), (>>->>~), (>>>->~), (>>>>-~),
+    -- ** composite 
     (>=====>), 
     
     ) where 
@@ -67,11 +92,11 @@
 import DeepControl.Applicative
 import Control.Monad
 
--- -----------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 -- Level-0 functions
 
 infixl 1  -<, >-
--- | Alias for @'$'@.
+-- | Anologous for @'$'@; (-<) is left associative.
 --
 -- >>> Just -< 3
 -- Just 3
@@ -85,7 +110,7 @@
 -- >>> :{
 -- let plus :: Int -> Int -> Int
 --     plus x y = 
---         x >- \a ->
+--         x >- \a ->  -- (>-) is the level-0 bind function, analogous for (>>=)
 --         y >- \b ->
 --         a + b
 -- in plus 3 4
@@ -96,7 +121,7 @@
 (>-) = flip (-<)
 
 infixr 1  <-<, >->
--- | Alias for @'.'@. 
+-- | Anologous for @'.'@. 
 --
 -- >>> ((3+) <-< (2*) <-< (1+)) -< 1
 -- 7
@@ -109,39 +134,34 @@
 (>->) :: (a -> b) -> (b -> c) -> a -> c
 (>->) = flip (<-<)
 
--- -----------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 -- Level-1 functions
 
-infixr 1  <<
--- | The auguments-flipped function for @'>>'@. 
-(<<) :: Monad m => m b -> m a -> m b 
-(<<) = flip (>>)
-
--- -----------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 -- Level-2 functions
 
 infixr 1  >==>
-infixr 1  >>~, >>==
+infixr 1  >>==, >>~
 infixr 1  ->==, >-==
 infixr 1  ->~, >-~
 
--- | The 'Monad2' class defines the Monad functions for level-2 types @m1 (m2 a)@; such as [[a]], Maybe [a], Either () (Maybe a), a -> [b], IO [a], etc.
+-- | The 'Monad2' class defines the Monad function for level-2 types @m1 (m2 a)@; such as [[a]], Maybe [a], Either () (Maybe a), a -> [b], IO [a], etc.
 -- 
 -- >>> :{
---  -- List-List Monad
---  [["a","b"]] >>== \x -> 
+--  -- List-List monad
+--  [["a","b"]] >>== \x ->   -- (>>==) is the level-2 bind function, analogous for (>>=)
 --  [[0],[1,2]] >>== \y -> 
 --  (**:) (x ++ show y)
 -- :}
 -- [["a0","b0"],["a0","b1","b2"],["a1","a2","b0"],["a1","a2","b1","b2"]]
 --
 -- >>> :{
---  let lengthM :: [Int] -> Maybe Int   -- ((->) [Int])-Maybe Monad
+--  let lengthM :: [Int] -> Maybe Int      -- (->)-Maybe monad
 --      lengthM [] = Nothing
 --      lengthM xs = Just (length xs) 
---      averageM :: [Int] -> Maybe Double
+--      averageM :: [Int] -> Maybe Double  -- (->)-Maybe monad
 --      averageM = 
---          sum >-== \s ->      -- sum :: [Int] -> Int -- ((->) [Int]) Monad
+--          (-*) sum >>== \s ->
 --          lengthM >>== \l ->
 --          (**:) (fromIntegral s / fromIntegral l)
 --  in [averageM [10, 25, 70], averageM []]
@@ -149,25 +169,19 @@
 -- [Just 35.0,Nothing]
 -- 
 class (Monad m2) => Monad2 m2 where
-  -- | Bind function of level-2.
+  -- | The level-2 bind function.
   (>>==) :: (Monad m1) => m1 (m2 a) -> (a -> m1 (m2 b)) -> m1 (m2 b)
 
--- | Composite function of level-2.
 (>==>) :: (Monad m1, Monad2 m2) => (a -> m1 (m2 b)) -> (b -> m1 (m2 c)) -> a -> m1 (m2 c)
 f >==> g = \x -> f x >>== g
--- | Sequence function of level-2.
 (>>~) :: (Monad m1, Monad2 m2) => m1 (m2 a) -> m1 (m2 b) -> m1 (m2 b)
 m >>~ k = m >>== \_ -> k
--- | Bind-cover function made of bind @'>>=='@ and cover @'-*'@, defined as @m >-== k = (-*) m >>== k@.
 (>-==) :: (Monad m1, Monad2 m2) => m1 a -> (a -> m1 (m2 b)) -> m1 (m2 b)
 m >-== k = (-*) m >>== k
--- | Bind-cover function made of bind @'>>=='@ and cover @'*-'@, defined as @m >-== k = (*-) m >>== k@.
 (->==) :: (Monad m1, Monad2 m2) => m2 a -> (a -> m1 (m2 b)) -> m1 (m2 b)
 m ->== k = (*:) m >>== k
--- | Sequence-cover function made of sequence @'>>~'@ and cover @'-*'@, defined as @m >-~ k = (-*) m >>~ k@.
 (>-~) :: (Monad m1, Monad2 m2) => m1 a -> m1 (m2 b) -> m1 (m2 b)
 m >-~ k = (-*) m >>~ k
--- | Sequence-cover function made of sequence @'>>~'@ and cover @'*-'@, defined as @m >-~ k = (*-) m >>~ k@.
 (->~) :: (Monad m1, Monad2 m2) => m2 a -> m1 (m2 b) -> m1 (m2 b)
 m ->~ k = (*:) m >>~ k
 
@@ -190,21 +204,38 @@
             Left l  -> (*:) (Left l)
             Right r -> f r
 
--- -----------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 -- Level-3 functions
 
 infixr 1  >===>
-infixr 1  >>>~, >>>==
+infixr 1  >>>==, >>>~
 infixr 1  >--==, ->-==, -->==, >>-==, >->==, ->>==
 infixr 1  >--~, ->-~, -->~, >>-~, >->~, ->>~
 
--- | The 'Monad3' class defines the Monad functions for level-3 types @m1 (m2 (m3 a)@.
+-- | The 'Monad3' class defines the Monad function for level-3 types @m1 (m2 (m3 a)@.
 -- 
 -- >>> :{
---  -- IO-List-List Monad
---  [["a","b"]] ->>== \x ->
+--  -- IO-List-List monad
+--  (*:) [["a","b"]] >>>== \x ->   -- (>>>==) is the level-3 bind-cover function, analogous for (>>=)
+--  (*:) [[0],[1,2]] >>>== \y ->
+--  (-**) (print (x,y)) >>>~       -- (>>>~) is the level-3 sequence function, analogous for (>>)
+--  (***:) (x ++ show y)
+-- :}
+-- ("a",0)
+-- ("a",1)
+-- ("a",2)
+-- ("b",0)
+-- ("b",1)
+-- ("b",2)
+-- [["a0","b0"],["a0","b1","b2"],["a1","a2","b0"],["a1","a2","b1","b2"]]
+--
+-- This messy code above can be neatly rewritten to the code below.
+--
+-- >>> :{
+--  -- IO-List-List monad
+--  [["a","b"]] ->>== \x ->   -- (->>==) is a level-3 bind-cover function, analogous for (>>=)
 --  [[0],[1,2]] ->>== \y ->
---  print (x,y) >--~
+--  print (x,y) >--~          -- (>--~) is a level-3 bind-cover function, analogous for (>>)
 --  (***:) (x ++ show y)
 -- :}
 -- ("a",0)
@@ -222,6 +253,7 @@
 f >===> g = \x -> f x >>>== g
 (>>>~) :: (Monad m1, Monad2 m2, Monad3 m3) => m1 (m2 (m3 a)) -> m1 (m2 (m3 b)) -> m1 (m2 (m3 b))
 m >>>~ k = m >>>== \_ -> k
+
 (>--==) :: (Monad m1, Monad2 m2, Monad3 m3) => m1 a -> (a -> m1 (m2 (m3 b))) -> m1 (m2 (m3 b))
 m >--== k = (-**) m >>>== k
 (->-==) :: (Monad m1, Monad2 m2, Monad3 m3) => m2 a -> (a -> m1 (m2 (m3 b))) -> m1 (m2 (m3 b))
@@ -234,18 +266,18 @@
 m ->>== k = (*:) m >>>== k
 (>->==) :: (Monad m1, Monad2 m2, Monad3 m3) => m1 (m3 a) -> (a -> m1 (m2 (m3 b))) -> m1 (m2 (m3 b))
 m >->== k = (-*) m >>>== k
-(>--~) :: (Monad m1, Monad2 m2, Monad3 m3) => m1 a -> m1 (m2 (m3 b)) -> m1 (m2 (m3 b))
-m >--~ k = (-**) m >>>~ k
-(->-~) :: (Monad m1, Monad2 m2, Monad3 m3) => m2 a -> m1 (m2 (m3 b)) -> m1 (m2 (m3 b))
-m ->-~ k = (*-*) m >>>~ k
 (-->~) :: (Monad m1, Monad2 m2, Monad3 m3) => m3 a -> m1 (m2 (m3 b)) -> m1 (m2 (m3 b))
 m -->~ k = (**:) m >>>~ k
-(>>-~) :: (Monad m1, Monad2 m2, Monad3 m3) => m1 (m2 a) -> m1 (m2 (m3 b)) -> m1 (m2 (m3 b))
-m >>-~ k = (--*) m >>>~ k
+(->-~) :: (Monad m1, Monad2 m2, Monad3 m3) => m2 a -> m1 (m2 (m3 b)) -> m1 (m2 (m3 b))
+m ->-~ k = (*-*) m >>>~ k
+(>--~) :: (Monad m1, Monad2 m2, Monad3 m3) => m1 a -> m1 (m2 (m3 b)) -> m1 (m2 (m3 b))
+m >--~ k = (-**) m >>>~ k
 (->>~) :: (Monad m1, Monad2 m2, Monad3 m3) => m2 (m3 a) -> m1 (m2 (m3 b)) -> m1 (m2 (m3 b))
 m ->>~ k = (*:) m >>>~ k
 (>->~) :: (Monad m1, Monad2 m2, Monad3 m3) => m1 (m3 a) -> m1 (m2 (m3 b)) -> m1 (m2 (m3 b))
 m >->~ k = (-*) m >>>~ k
+(>>-~) :: (Monad m1, Monad2 m2, Monad3 m3) => m1 (m2 a) -> m1 (m2 (m3 b)) -> m1 (m2 (m3 b))
+m >>-~ k = (--*) m >>>~ k
 
 instance Monad3 Maybe where
     mmmv >>>== f = 
@@ -266,12 +298,17 @@
             Left l  -> (**:) (Left l)
             Right r -> f r
 
--- -----------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 -- Level-4 functions
 
 infixr 1  >====>
-infixr 1  >>>>~, >>>>==
--- TODO: >>>>~
+infixr 1  >>>>==, >>>>~
+infixr 1  --->==, -->-==, ->--==, >---==
+infixr 1  -->>==, ->->==, >-->==, >->-==, ->>-==, >>--==
+infixr 1  ->>>==, >->>==, >>->==, >>>-==
+infixr 1  --->~, -->-~, ->--~, >---~
+infixr 1  -->>~, ->->~, >-->~, >->-~, ->>-~, >>--~
+infixr 1  ->>>~, >->>~, >>->~, >>>-~
 
 class (Monad3 m4) => Monad4 m4 where
   (>>>>==) :: (Monad m1, Monad2 m2, Monad3 m3) => m1 (m2 (m3 (m4 a))) -> (a -> m1 (m2 (m3 (m4 b)))) -> m1 (m2 (m3 (m4 b)))
@@ -281,6 +318,68 @@
 (>>>>~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m1 (m2 (m3 (m4 a))) -> m1 (m2 (m3 (m4 b))) -> m1 (m2 (m3 (m4 b)))
 m >>>>~ k = m >>>>== \_ -> k
 
+(--->==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m4 a -> (a -> m1 (m2 (m3 (m4 b)))) -> m1 (m2 (m3 (m4 b)))
+m --->== k = (***:) m >>>>== k 
+(-->-==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m3 a -> (a -> m1 (m2 (m3 (m4 b)))) -> m1 (m2 (m3 (m4 b)))
+m -->-== k = (**-*) m >>>>== k 
+(->--==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m2 a -> (a -> m1 (m2 (m3 (m4 b)))) -> m1 (m2 (m3 (m4 b)))
+m ->--== k = (*-**) m >>>>== k 
+(>---==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m1 a -> (a -> m1 (m2 (m3 (m4 b)))) -> m1 (m2 (m3 (m4 b)))
+m >---== k = (-***) m >>>>== k
+
+(-->>==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m3 (m4 a) -> (a -> m1 (m2 (m3 (m4 b)))) -> m1 (m2 (m3 (m4 b)))
+m -->>== k = (**:) m >>>>== k 
+(->->==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m2 (m4 a) -> (a -> m1 (m2 (m3 (m4 b)))) -> m1 (m2 (m3 (m4 b)))
+m ->->== k = (*-*) m >>>>== k 
+(>-->==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m1 (m4 a) -> (a -> m1 (m2 (m3 (m4 b)))) -> m1 (m2 (m3 (m4 b)))
+m >-->== k = (-**) m >>>>== k 
+(>->-==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m1 (m3 a) -> (a -> m1 (m2 (m3 (m4 b)))) -> m1 (m2 (m3 (m4 b)))
+m >->-== k = (-*-*) m >>>>== k 
+(->>-==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m2 (m3 a) -> (a -> m1 (m2 (m3 (m4 b)))) -> m1 (m2 (m3 (m4 b)))
+m ->>-== k = (*--*) m >>>>== k 
+(>>--==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m1 (m2 a) -> (a -> m1 (m2 (m3 (m4 b)))) -> m1 (m2 (m3 (m4 b)))
+m >>--== k = (--**) m >>>>== k 
+
+(->>>==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m2 (m3 (m4 a)) -> (a -> m1 (m2 (m3 (m4 b)))) -> m1 (m2 (m3 (m4 b)))
+m ->>>== k = (*:) m >>>>== k 
+(>->>==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m1 (m3 (m4 a)) -> (a -> m1 (m2 (m3 (m4 b)))) -> m1 (m2 (m3 (m4 b)))
+m >->>== k = (-*) m >>>>== k 
+(>>->==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m1 (m2 (m4 a)) -> (a -> m1 (m2 (m3 (m4 b)))) -> m1 (m2 (m3 (m4 b)))
+m >>->== k = (--*) m >>>>== k 
+(>>>-==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m1 (m2 (m3 a)) -> (a -> m1 (m2 (m3 (m4 b)))) -> m1 (m2 (m3 (m4 b)))
+m >>>-== k = (---*) m >>>>== k 
+
+(--->~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m4 a -> m1 (m2 (m3 (m4 b))) -> m1 (m2 (m3 (m4 b)))
+m --->~ k = (***:) m >>>>~ k
+(-->-~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m3 a -> m1 (m2 (m3 (m4 b))) -> m1 (m2 (m3 (m4 b)))
+m -->-~ k = (**-*) m >>>>~ k
+(->--~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m2 a -> m1 (m2 (m3 (m4 b))) -> m1 (m2 (m3 (m4 b)))
+m ->--~ k = (*-**) m >>>>~ k
+(>---~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m1 a -> m1 (m2 (m3 (m4 b))) -> m1 (m2 (m3 (m4 b)))
+m >---~ k = (-***) m >>>>~ k
+
+(-->>~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m3 (m4 a) -> m1 (m2 (m3 (m4 b))) -> m1 (m2 (m3 (m4 b)))
+m -->>~ k = (**:) m >>>>~ k
+(->->~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m2 (m4 a) -> m1 (m2 (m3 (m4 b))) -> m1 (m2 (m3 (m4 b)))
+m ->->~ k = (*-*) m >>>>~ k
+(>-->~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m1 (m4 a) -> m1 (m2 (m3 (m4 b))) -> m1 (m2 (m3 (m4 b)))
+m >-->~ k = (-**) m >>>>~ k
+(>->-~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m1 (m3 a) -> m1 (m2 (m3 (m4 b))) -> m1 (m2 (m3 (m4 b)))
+m >->-~ k = (-*-*) m >>>>~ k
+(->>-~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m2 (m3 a) -> m1 (m2 (m3 (m4 b))) -> m1 (m2 (m3 (m4 b)))
+m ->>-~ k = (*--*) m >>>>~ k
+(>>--~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m1 (m2 a) -> m1 (m2 (m3 (m4 b))) -> m1 (m2 (m3 (m4 b)))
+m >>--~ k = (--**) m >>>>~ k
+
+(->>>~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m2 (m3 (m4 a)) -> m1 (m2 (m3 (m4 b))) -> m1 (m2 (m3 (m4 b)))
+m ->>>~ k = (*:) m >>>>~ k
+(>->>~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m1 (m3 (m4 a)) -> m1 (m2 (m3 (m4 b))) -> m1 (m2 (m3 (m4 b)))
+m >->>~ k = (-*) m >>>>~ k
+(>>->~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m1 (m2 (m4 a)) -> m1 (m2 (m3 (m4 b))) -> m1 (m2 (m3 (m4 b)))
+m >>->~ k = (--*) m >>>>~ k
+(>>>-~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m1 (m2 (m3 a)) -> m1 (m2 (m3 (m4 b))) -> m1 (m2 (m3 (m4 b)))
+m >>>-~ k = (---*) m >>>>~ k
+
 instance Monad4 Maybe where
     mmmmv >>>>== f = 
         mmmmv >>>== \mv ->
@@ -300,13 +399,21 @@
             Left l  -> (***:) (Left l)
             Right r -> f r
 
--- -----------------------------------------------------------------------------
+-------------------------------------------------------------------------------
 -- Level-5 functions
 
 infixr 1  >=====>
-infixr 1  >>>>>~, >>>>>== 
--- TODO: >>>>>~
+infixr 1  >>>>>~, >>>>>==
+infixr 1  ---->==, --->-==, -->--==, ->---==, >----==
+infixr 1  --->>==, -->->==, ->-->==, >--->==, >-->-==, ->->-==, -->>-==, ->>--==, >->--==, >>---==
+infixr 1  -->>>==, ->->>==, >-->>==, >->->==, ->>->==, >>-->==, >>->-==, >->>-==, ->>>-==, >>>--==
+infixr 1  ->>>>==, >->>>==, >>->>==, >>>->==, >>>>-==
 
+infixr 1  ---->~, --->-~, -->--~, ->---~, >----~
+infixr 1  --->>~, -->->~, ->-->~, >--->~, >-->-~, ->->-~, -->>-~, ->>--~, >->--~, >>---~
+infixr 1  -->>>~, ->->>~, >-->>~, >->->~, ->>->~, >>-->~, >>->-~, >->>-~, ->>>-~, >>>--~
+infixr 1  ->>>>~, >->>>~, >>->>~, >>>->~, >>>>-~
+
 class (Monad4 m5) => Monad5 m5 where
   (>>>>>==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4) => m1 (m2 (m3 (m4 (m5 a)))) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
 
@@ -314,6 +421,136 @@
 f >=====> g = \x -> f x >>>>>== g
 (>>>>>~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m2 (m3 (m4 (m5 a)))) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
 m >>>>>~ k = m >>>>>== \_ -> k
+
+(---->==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m5 a -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m ---->== k = (****:) m >>>>>== k 
+(--->-==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m4 a -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m --->-== k = (***-*) m >>>>>== k 
+(-->--==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m3 a -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m -->--== k = (**-**) m >>>>>== k 
+(->---==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m2 a -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m ->---== k = (*-***) m >>>>>== k 
+(>----==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 a -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >----== k = (-****) m >>>>>== k 
+
+(--->>==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m4 (m5 a) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m --->>== k = (***:) m >>>>>== k 
+(-->->==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m3 (m5 a) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m -->->== k = (**-*) m >>>>>== k 
+(->-->==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m2 (m5 a) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m ->-->== k = (*-**) m >>>>>== k 
+(>--->==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m5 a) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >--->== k = (-***) m >>>>>== k 
+(>-->-==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m4 a) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >-->-== k = (-**-*) m >>>>>== k 
+(->->-==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m2 (m4 a) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m ->->-== k = (*-*-*) m >>>>>== k 
+(-->>-==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m3 (m4 a) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m -->>-== k = (**--*) m >>>>>== k 
+(->>--==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m2 (m3 a) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m ->>--== k = (*--**) m >>>>>== k 
+(>->--==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m3 a) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >->--== k = (-*-**) m >>>>>== k 
+(>>---==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m2 a) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >>---== k = (--***) m >>>>>== k 
+
+(-->>>==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m3 (m4 (m5 a)) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m -->>>== k = (**:) m >>>>>== k 
+(->->>==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m2 (m4 (m5 a)) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m ->->>== k = (*-*) m >>>>>== k 
+(>-->>==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m4 (m5 a)) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >-->>== k = (-**) m >>>>>== k 
+(>->->==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m3 (m5 a)) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >->->== k = (-*-*) m >>>>>== k 
+(->>->==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m2 (m3 (m5 a)) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m ->>->== k = (*--*) m >>>>>== k 
+(>>-->==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m2 (m5 a)) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >>-->== k = (--**) m >>>>>== k 
+(>>->-==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m2 (m4 a)) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >>->-== k = (--*-*) m >>>>>== k 
+(>->>-==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m3 (m4 a)) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >->>-== k = (-*--*) m >>>>>== k 
+(->>>-==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m2 (m3 (m4 a)) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m ->>>-== k = (*---*) m >>>>>== k 
+(>>>--==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m2 (m3 a)) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >>>--== k = (---**) m >>>>>== k 
+
+(->>>>==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m2 (m3 (m4 (m5 a))) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m ->>>>== k = (*:) m >>>>>== k 
+(>->>>==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m3 (m4 (m5 a))) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >->>>== k = (-*) m >>>>>== k 
+(>>->>==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m2 (m4 (m5 a))) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >>->>== k = (--*) m >>>>>== k 
+(>>>->==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m2 (m3 (m5 a))) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >>>->== k = (---*) m >>>>>== k 
+(>>>>-==) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m2 (m3 (m4 a))) -> (a -> m1 (m2 (m3 (m4 (m5 b))))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >>>>-== k = (----*) m >>>>>== k 
+
+
+(---->~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m5 a -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m ---->~ k = (****:) m >>>>>~ k 
+(--->-~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m4 a -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m --->-~ k = (***-*) m >>>>>~ k 
+(-->--~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m3 a -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m -->--~ k = (**-**) m >>>>>~ k 
+(->---~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m2 a -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m ->---~ k = (*-***) m >>>>>~ k 
+(>----~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 a -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >----~ k = (-****) m >>>>>~ k 
+
+
+(--->>~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m4 (m5 a) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m --->>~ k = (***:) m >>>>>~ k 
+(-->->~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m3 (m5 a) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m -->->~ k = (**-*) m >>>>>~ k 
+(->-->~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m2 (m5 a) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m ->-->~ k = (*-**) m >>>>>~ k 
+(>--->~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m5 a) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >--->~ k = (-***) m >>>>>~ k 
+(>-->-~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m4 a) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >-->-~ k = (-**-*) m >>>>>~ k 
+(->->-~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m2 (m4 a) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m ->->-~ k = (*-*-*) m >>>>>~ k 
+(-->>-~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m3 (m4 a) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m -->>-~ k = (**--*) m >>>>>~ k 
+(->>--~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m2 (m3 a) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m ->>--~ k = (*--**) m >>>>>~ k 
+(>->--~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m3 a) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >->--~ k = (-*-**) m >>>>>~ k 
+(>>---~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m2 a) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >>---~ k = (--***) m >>>>>~ k 
+
+(-->>>~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m3 (m4 (m5 a)) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m -->>>~ k = (**:) m >>>>>~ k 
+(->->>~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m2 (m4 (m5 a)) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m ->->>~ k = (*-*) m >>>>>~ k 
+(>-->>~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m4 (m5 a)) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >-->>~ k = (-**) m >>>>>~ k 
+(>->->~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m3 (m5 a)) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >->->~ k = (-*-*) m >>>>>~ k 
+(->>->~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m2 (m3 (m5 a)) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m ->>->~ k = (*--*) m >>>>>~ k 
+(>>-->~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m2 (m5 a)) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >>-->~ k = (--**) m >>>>>~ k 
+(>>->-~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m2 (m4 a)) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >>->-~ k = (--*-*) m >>>>>~ k 
+(>->>-~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m3 (m4 a)) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >->>-~ k = (-*--*) m >>>>>~ k 
+(->>>-~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m2 (m3 (m4 a)) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m ->>>-~ k = (*---*) m >>>>>~ k 
+(>>>--~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m2 (m3 a)) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >>>--~ k = (---**) m >>>>>~ k 
+
+(->>>>~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m2 (m3 (m4 (m5 a))) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m ->>>>~ k = (*:) m >>>>>~ k 
+(>->>>~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m3 (m4 (m5 a))) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >->>>~ k = (-*) m >>>>>~ k 
+(>>->>~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m2 (m4 (m5 a))) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >>->>~ k = (--*) m >>>>>~ k 
+(>>>->~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m2 (m3 (m5 a))) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >>>->~ k = (---*) m >>>>>~ k 
+(>>>>-~) :: (Monad m1, Monad2 m2, Monad3 m3, Monad4 m4, Monad5 m5) => m1 (m2 (m3 (m4 a))) -> m1 (m2 (m3 (m4 (m5 b)))) -> m1 (m2 (m3 (m4 (m5 b))))
+m >>>>-~ k = (----*) m >>>>>~ k 
 
 instance Monad5 Maybe where
     mmmmmv >>>>>== f = 
diff --git a/DeepControl/Monad/Morph.hs b/DeepControl/Monad/Morph.hs
--- a/DeepControl/Monad/Morph.hs
+++ b/DeepControl/Monad/Morph.hs
@@ -2,7 +2,7 @@
 Module      : DeepControl.Monad.Morph
 Description : Extension for mmorph's Contrl.Monad.Morph.
 Copyright   : 2013 Gabriel Gonzalez,
-              (C) 2015 KONISHI Yohsuke 
+              (c) 2015 KONISHI Yohsuke 
 License     : BSD-style (see the LICENSE file in the distribution)
 Maintainer  : ocean0yohsuke@gmail.com
 Stability   : experimental
@@ -10,7 +10,6 @@
 
 This module enables you to program in Monad-Morphic style for more __deeper__ level than the usual @Control.Monad.Morph@ module expresses.
 You would realize exactly what __/more deeper level/__ means by reading the example codes, which are attached on the page bottom.
-Note: many instances for Level-4 and Level-5 haven't been written yet.
 -}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -20,18 +19,23 @@
     module Control.Monad.Morph,
 
     -- * Level-1
+    -- ** trans-map
     (|>|), (|<|), 
 
     -- * Level-2
+    -- ** trans-map
     (|>>|), (|<<|),
 
     -- * Level-3
+    -- ** trans-map
     (|>>>|), (|<<<|),
 
     -- * Level-4
+    -- ** trans-map
     (|>>>>|), (|<<<<|),
 
     -- * Level-5
+    -- ** trans-map
     (|>>>>>|), (|<<<<<|),
 
     -- * Level-2 example
@@ -47,7 +51,7 @@
 -- Level-1 functions
 
 infixl 2  |>|
--- | Alias for @'hoist'@.
+-- | Alias to @'hoist'@.
 (|>|) :: (Monad m, MFunctor t) => (forall a . m a -> n a) -> t m b -> t n b
 (|>|) = hoist
 
@@ -142,7 +146,7 @@
 >
 >tock                        ::                   StateT Int IO ()
 >tock = do
->    generalize |>| tick     :: (Monad      m) => StateT Int m  ()
+>    generalize |>| tick     :: (Monad      m) => StateT Int m  ()  -- (|>|) is the level-1 trans-map function, analogous for (|$>) 
 >    lift $ putStrLn "Tock!" :: (MonadTrans t) => t          IO ()
 >
 >-- λ> runStateT tock 0
@@ -159,7 +163,7 @@
 >program = replicateM_ 4 $ do
 >    lift |>| tock
 >        :: (MonadTrans t) => StateT Int (t             IO) ()
->    generalize |>>| save
+>    generalize |>>| save                                         -- (|>>|) is the level-2 trans-map function, analogous for (|$>>)
 >        :: (Monad      m) => StateT Int (WriterT [Int] m ) ()
 >
 >-- λ> execWriterT (runStateT program 0)
diff --git a/DeepControl/Monad/Trans.hs b/DeepControl/Monad/Trans.hs
--- a/DeepControl/Monad/Trans.hs
+++ b/DeepControl/Monad/Trans.hs
@@ -3,7 +3,7 @@
 Description : Enable deep level Monad-Transform programming.
 Copyright   : (c) Andy Gill 2001,
               (c) Oregon Graduate Institute of Science and Technology, 2001,
-              (C) 2015 KONISHI Yohsuke
+              (c) 2015 KONISHI Yohsuke
 License     : BSD-style (see the file LICENSE)
 Maintainer  : ocean0yohsuke@gmail.com
 Stability   : experimental
@@ -11,7 +11,6 @@
 
 This module enables you to program in Monad-Transformer style for more __deeper__ level than the usual @Control.Monad.Trans@ module expresses.
 You would realize exactly what __/more deeper level/__ means by reading the example codes, which are attached on the page bottom.
-Note: many instances for Level-4 and Level-5 haven't been written yet.
 -}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeSynonymInstances #-}
@@ -20,80 +19,79 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE FlexibleContexts #-}
 module DeepControl.Monad.Trans (
-    -- * MonadIO
-    MonadIO(..),
-
-    -- * MonadTrans
-    -- ** Level-1
-    -- *** lift
+    -- * Level-1
+    -- ** trans-lift
     MonadTrans(..), 
     liftT, liftTT, liftTTT, liftTTTT, liftTTTTT,
-    -- *** transdown
+    -- ** trans-down
     MonadTransDown(..), M,
-    -- *** cover  
+    -- ** trans-cover  
     MonadTransCover(..),
-    -- *** other  
+    -- ** other  
     MonadTrans_(..), 
 
-    -- ** Level-2
-    -- *** lift
+    -- * Level-2
+    -- ** trans-lift
     MonadTrans2(..), 
     liftTT2, liftTTT2, liftTTTT2, liftTTTTT2,
-    -- *** transdown
+    -- ** trans-down
     MonadTrans2Down(..), M_, T_, 
-    -- *** fold 
+    -- ** trans-fold 
     MonadTransFold2(..), 
-    -- *** cover  
+    -- ** trans-cover  
     MonadTransCover2(..),
     (|**|),
-    -- *** other  
+    -- ** other  
     trans2, untrans2, 
 
-    -- ** Level-3
-    -- *** lift
+    -- * Level-3
+    -- ** trans-lift
     MonadTrans3(..), 
     liftTT3, liftTTT3, liftTTTT3, liftTTTTT3,
-    -- *** transdown
+    -- ** trans-down
     MonadTrans3Down(..), M__, T__, 
-    -- *** fold 
+    -- ** trans-fold 
     MonadTransFold3(..), 
-    -- *** cover 
+    -- ** trans-cover 
     MonadTransCover3(..),
     (|***|), 
     (|-**|), (|*-*|), (|**-|),
-    -- *** other  
+    -- ** other  
     trans3, untrans3, 
 
-    -- ** Level-4
-    -- *** lift
+    -- * Level-4
+    -- ** trans-lift
     MonadTrans4(..),
-    -- *** transdown
+    -- ** trans-down
     MonadTrans4Down(..), M___, T___, T2__,
-    -- *** fold 
+    -- ** trans-fold 
     MonadTransFold4(..), 
-    -- *** cover 
+    -- ** trans-cover 
     MonadTransCover4(..),
     (|****|), 
     (|--**|), (|-*-*|), (|-**-|), (|*-*-|), (|**--|), (|*--*|),
     (|-***|), (|*-**|), (|**-*|), (|***-|), 
-    -- *** other  
+    -- ** other  
     trans4, untrans4, 
 
-    -- ** Level-5
-    -- *** lift
+    -- * Level-5
+    -- ** trans-lift
     MonadTrans5(..),
-    -- *** transdown
+    -- ** trans-down
     MonadTrans5Down(..), M____, T____, T2___, T3___,
-    -- *** fold 
+    -- ** trans-fold 
     MonadTransFold5(..), 
-    -- *** cover 
+    -- ** trans-cover 
     MonadTransCover5(..),
     (|---**|), (|--*-*|), (|-*--*|), (|*---*|), (|*--*-|), (|*-*--|), (|**---|),
     (|--***|), (|-*-**|), (|*--**|), (|*-*-*|), (|**--*|), (|**-*-|), (|***--|),
     (|-****|), (|*-***|), (|**-**|), (|***-*|), (|****-|),
-    -- *** other  
+    -- ** other  
     trans5, untrans5, 
 
+    -- * MonadIO
+    MonadIO(..),
+
     -- * Level-2 example
     -- $Example_Level2
 
@@ -111,11 +109,14 @@
 import qualified Control.Monad.Trans.Maybe   as M
 import qualified Control.Monad.Except        as E
 import Control.Monad.Identity
+import Control.Monad.RWS (RWS, RWST(..), runRWS)
+import Control.Monad.Reader (Reader, ReaderT(..), runReader)
+import Control.Monad.State (State, StateT(..), runState)
 
 ----------------------------------------------------------------------
 -- Level-1
 
--- | Alias for @'lift'@
+-- | Alias to @'lift'@
 liftT :: (Monad m, MonadTrans t) => m a -> t m a 
 liftT = lift
 
@@ -153,9 +154,14 @@
     type TransDown M.MaybeT = Maybe
 instance MonadTransDown (E.ExceptT e) where
     type TransDown (E.ExceptT e) = E.Except e
+instance (Monoid w) => MonadTransDown (RWST r w s) where
+    type TransDown (RWST r w s) = RWS r w s
+instance MonadTransDown (ReaderT r) where
+    type TransDown (ReaderT r) = Reader r
+instance MonadTransDown (StateT s) where
+    type TransDown (StateT s) = State s
 
 infixl 3  |*|
-
 class (MonadTransDown t1) => MonadTransCover t1 where
     (|*|) :: Monad m1 => (TransDown t1) a -> t1 m1 a
 
@@ -165,6 +171,12 @@
     (|*|) = M.MaybeT . (*:)
 instance MonadTransCover (E.ExceptT e) where
     (|*|) = E.ExceptT . (*:) . E.runExcept
+instance (Monoid w) => MonadTransCover (RWST r w s) where
+    (|*|) = RWST . ((*:)|$>>) . runRWS
+instance MonadTransCover (ReaderT s) where
+    (|*|) = ReaderT . ((*:)|$>) . runReader
+instance MonadTransCover (StateT s) where
+    (|*|) = StateT . ((*:)|$>) . runState
 
 -- | Required only for @'MonadTransFold2'@ and @'MonadTransFold3'@ 
 class MonadTrans_ t where
@@ -544,7 +556,7 @@
 >import DeepControl.Monad.Morph ((|>|))
 >import DeepControl.Monad.Trans (liftTT2, transfold2, untransfold2)
 >import DeepControl.Monad.Trans.Identity
->import DeepControl.Monad.Trans.Reader
+>import Control.Monad.Reader
 >import Control.Monad.Trans.Maybe
 >
 >import System.Timeout (timeout)
@@ -583,7 +595,7 @@
 -}
 
 {- $Example_Level2_cover
-Here is a monad transformer example showing how to use cover functions.
+Here is a monad transformer example showing how to use trans-cover functions.
 
 >import DeepControl.Applicative ((|$>))
 >import DeepControl.Monad (Monad2)
@@ -591,30 +603,30 @@
 >import DeepControl.Monad.Trans (liftT, (|*|), (|-*|), (|*-|))
 >import DeepControl.Monad.Trans.Writer
 >import DeepControl.Monad.Trans.Identity
->import DeepControl.Monad.Trans.State
+>import Control.Monad.State
 >
 >tick :: State Int ()
 >tick = modify (+1)
 >
 >tock                         ::                   StateT Int IO ()
 >tock = do
->    (|*|) tick               :: (Monad      m) => StateT Int m  ()
->    liftT $ putStrLn "Tock!" :: (MonadTrans t) => t          IO ()
+>    (|*|) tick               :: (Monad      m) => StateT Int m  ()  -- (|*|) is the level-1 trans-cover function, analogous for (*:)
+>    liftT $ putStrLn "Tock!" :: (MonadTrans t) => t          IO ()  -- 'liftT' is the level-1 trans-lift function, alias to 'lift'
 >
 >-- λ> runStateT tock 0
 >-- Tock!
 >-- ((),1)
 >
->save    :: StateT Int (Writer [Int]) ()
+>save :: StateT Int (Writer [Int]) ()
 >save = do
 >    n <- get
 >    liftT $ tell [n]
 >
->program ::               StateT Int (IdentityT2 IO (Writer [Int])) ()
+>program ::               StateT Int (IdentityT2 IO (Writer [Int])) ()  -- StateT-IdentityT2-IO-Writer monad, a level-2 monad-transform
 >program = replicateM_ 4 $ do
->    ((|-*|).liftT) |>| tock
+>    ((|-*|).liftT) |>| tock                                            -- (|-*|) is a level-2 trans-cover function, analogous for (-*)
 >        :: (Monad2 m) => StateT Int (IdentityT2 IO m             ) ()
->    ((|*-|).liftT) |>| save
+>    ((|*-|).liftT) |>| save                                            -- (|*-|) is a level-2 trans-cover function, analogous for (*-)
 >        :: (Monad  m) => StateT Int (IdentityT2 m  (Writer [Int])) ()
 >
 >-- λ> execWriter |$> runIdentityT2 (runStateT program 0)
diff --git a/DeepControl/Monad/Trans/Except.hs b/DeepControl/Monad/Trans/Except.hs
--- a/DeepControl/Monad/Trans/Except.hs
+++ b/DeepControl/Monad/Trans/Except.hs
@@ -2,7 +2,7 @@
 Module      : DeepControl.Monad.Trans.Except
 Description : Extension for mtl's Contrl.Monad.Except.
 Copyright   : (C) 2013 Ross Paterson,
-              (C) 2015 KONISHI Yohsuke 
+              (c) 2015 KONISHI Yohsuke 
 License     : BSD-style (see the file LICENSE)
 Maintainer  : ocean0yohsuke@gmail.com
 Stability   : experimental
@@ -13,7 +13,6 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE RankNTypes #-}
 module DeepControl.Monad.Trans.Except (
-    -- * Level-1
     module Control.Monad.Except,
 
     -- * Level-2
@@ -35,41 +34,29 @@
     ) where 
 
 import DeepControl.Applicative
-import DeepControl.Monad
 import DeepControl.Commutative
+import DeepControl.Monad
+import DeepControl.Monad.Signatures
 
 import Control.Monad.Except
 import Control.Monad.Identity
 
 ----------------------------------------------------------------
--- Level-1
-
-instance Commutative (Except e) where
-    commute x = ExceptT . Identity |$> commute (runExcept x)
+-- Level-2
 
 instance Monad2 (Except e) where
     m >>== f = (ExceptT . Identity |$>) $ (runExcept |$> m) >>== runExcept |$>> f
-instance Monad3 (Except e) where
-    m >>>== f = (ExceptT . Identity |$>>) $ (runExcept |$>> m) >>>== runExcept |$>>> f
-instance Monad4 (Except e) where
-    m >>>>== f = (ExceptT . Identity |$>>>) $ (runExcept |$>>> m) >>>>== runExcept |$>>>> f
-instance Monad5 (Except e) where
-    m >>>>>== f = (ExceptT . Identity |$>>>>) $ (runExcept |$>>>> m) >>>>>== runExcept |$>>>>> f
 
-----------------------------------------------------------------
--- Level-2
-
 throwError2 :: (MonadError e m2, Applicative m1) => e -> m1 (m2 a)
 throwError2 = (*:) |$> throwError
 
 catchError2 :: (MonadError e m2, Commutative m1, Commutative m2) => 
                 m1 (m2 a) -> (e -> m1 (m2 a)) -> m1 (m2 a)
-catchError2 = coverCatch catchError
+catchError2 = liftCatch catchError
   where
-    coverCatch :: (Commutative m1, Commutative m2) => 
-                  (forall a. m2 a -> (e -> m2 a) -> m2 a) -> 
-                   m1 (m2 a) -> (e -> m1 (m2 a)) -> m1 (m2 a)
-    coverCatch catch m h = 
+    liftCatch :: (Commutative m1, Commutative m2) => 
+                 (forall a. Catch e m2 a) -> Catch2 e m1 m2 a
+    liftCatch catch m h = 
         let m' = commute m
             h' = commute |$> h
         in commute $ catch m' h'
@@ -77,17 +64,19 @@
 ----------------------------------------------------------------
 -- Level-3
 
+instance Monad3 (Except e) where
+    m >>>== f = (ExceptT . Identity |$>>) $ (runExcept |$>> m) >>>== runExcept |$>>> f
+
 throwError3 :: (MonadError e m3, Applicative m1, Applicative m2) => e -> m1 (m2 (m3 a))
 throwError3 = (**:) |$> throwError
 
 catchError3 :: (MonadError e m3, Commutative m1, Commutative m2, Commutative m3) => 
                 m1 (m2 (m3 a)) -> (e -> m1 (m2 (m3 a))) -> m1 (m2 (m3 a))
-catchError3 = cover2Catch catchError
+catchError3 = liftCatch catchError
   where
-    cover2Catch :: (Commutative m1, Commutative m2, Commutative m3) => 
-                   (forall a. m3 a -> (e -> m3 a) -> m3 a) -> 
-                    m1 (m2 (m3 a)) -> (e -> m1 (m2 (m3 a))) -> m1 (m2 (m3 a))
-    cover2Catch catch m h = 
+    liftCatch :: (Commutative m1, Commutative m2, Commutative m3) => 
+                 (forall a. Catch e m3 a) -> Catch3 e m1 m2 m3 a
+    liftCatch catch m h = 
         let m' = float2 m
             h' = float2 |$> h
         in sink2 $ catch m' h'
@@ -95,17 +84,19 @@
 ----------------------------------------------------------------
 -- Level-4
 
+instance Monad4 (Except e) where
+    m >>>>== f = (ExceptT . Identity |$>>>) $ (runExcept |$>>> m) >>>>== runExcept |$>>>> f
+
 throwError4 :: (MonadError e m4, Applicative m1, Applicative m2, Applicative m3) => e -> m1 (m2 (m3 (m4 a)))
 throwError4 = (***:) |$> throwError
 
 catchError4 :: (MonadError e m4, Commutative m1, Commutative m2, Commutative m3, Commutative m4) => 
                 m1 (m2 (m3 (m4 a))) -> (e -> m1 (m2 (m3 (m4 a)))) -> m1 (m2 (m3 (m4 a)))
-catchError4 = cover3Catch catchError
+catchError4 = liftCatch catchError
   where
-    cover3Catch :: (Commutative m1, Commutative m2, Commutative m3, Commutative m4) => 
-                   (forall a. m4 a -> (e -> m4 a) -> m4 a) -> 
-                    m1 (m2 (m3 (m4 a))) -> (e -> m1 (m2 (m3 (m4 a)))) -> m1 (m2 (m3 (m4 a)))
-    cover3Catch catch m h = 
+    liftCatch :: (Commutative m1, Commutative m2, Commutative m3, Commutative m4) => 
+                 (forall a. Catch e m4 a) -> Catch4 e m1 m2 m3 m4 a
+    liftCatch catch m h = 
         let m' = float3 m
             h' = float3 |$> h
         in sink3 $ catch m' h'
@@ -113,30 +104,20 @@
 ----------------------------------------------------------------
 -- Level-5
 
+instance Monad5 (Except e) where
+    m >>>>>== f = (ExceptT . Identity |$>>>>) $ (runExcept |$>>>> m) >>>>>== runExcept |$>>>>> f
+
 throwError5 :: (MonadError e m5, Applicative m1, Applicative m2, Applicative m3, Applicative m4) => e -> m1 (m2 (m3 (m4 (m5 a))))
 throwError5 = (****:) |$> throwError
 
 catchError5 :: (MonadError e m5, Commutative m1, Commutative m2, Commutative m3, Commutative m4, Commutative m5) => 
                 m1 (m2 (m3 (m4 (m5 a)))) -> (e -> m1 (m2 (m3 (m4 (m5 a))))) -> m1 (m2 (m3 (m4 (m5 a))))
-catchError5 = cover4Catch catchError
+catchError5 = liftCatch catchError
   where
-    cover4Catch :: (Commutative m1, Commutative m2, Commutative m3, Commutative m4, Commutative m5) => 
-                   (forall a. m5 a -> (e -> m5 a) -> m5 a) -> 
-                    m1 (m2 (m3 (m4 (m5 a)))) -> (e -> m1 (m2 (m3 (m4 (m5 a))))) -> m1 (m2 (m3 (m4 (m5 a))))
-    cover4Catch catch m h = 
+    liftCatch :: (Commutative m1, Commutative m2, Commutative m3, Commutative m4, Commutative m5) => 
+                 (forall a. Catch e m5 a) -> Catch5 e m1 m2 m3 m4 m5 a
+    liftCatch catch m h = 
         let m' = float4 m
             h' = float4 |$> h
         in sink4 $ catch m' h'
 
-----------------------------------------------------------------
--- Level-6
-
-{-
-cover5Catch :: (Commutative m1, Commutative m2, Commutative m3, Commutative m4, Commutative m5, Commutative m6) => 
-               (forall a. m6 a -> (e -> m6 a) -> m6 a) -> 
-                m1 (m2 (m3 (m4 (m5 (m6 a))))) -> (e -> m1 (m2 (m3 (m4 (m5 (m6 a)))))) -> m1 (m2 (m3 (m4 (m5 (m6 a)))))
-cover5Catch catch m h = 
-    let m' = float5 m
-        h' = float5 |$> h
-    in sink5 $ catch m' h'
--}
diff --git a/DeepControl/Monad/Trans/Identity.hs b/DeepControl/Monad/Trans/Identity.hs
--- a/DeepControl/Monad/Trans/Identity.hs
+++ b/DeepControl/Monad/Trans/Identity.hs
@@ -1,19 +1,20 @@
 {-|
 Module      : DeepControl.Monad.Trans.Identity
-Description : ---
+Description : Enables dealing with deep monads in monad-transformer
 Copyright   : (c) 2007 Magnus Therning,
-              (C) 2015 KONISHI Yohsuke
+              (c) 2015 KONISHI Yohsuke
 License     : BSD-style (see the file LICENSE)
 Maintainer  : ocean0yohsuke@gmail.com
 Stability   : experimental
 Portability : ---
 
-
+This module enables dealing with deep monads in monad-transformer. 
 -}
 {-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE TypeFamilies #-}
 module DeepControl.Monad.Trans.Identity (
+    -- * Level-1
     module Data.Functor.Identity,
     module Control.Monad.Trans.Identity,
 
diff --git a/DeepControl/Monad/Trans/RWS.hs b/DeepControl/Monad/Trans/RWS.hs
deleted file mode 100644
--- a/DeepControl/Monad/Trans/RWS.hs
+++ /dev/null
@@ -1,39 +0,0 @@
-{-|
-Module      : DeepControl.Monad.Trans.RWS
-Description : Extension for mtl's Contrl.Monad.RWS.
-Copyright   : (C) 2015 KONISHI Yohsuke,
-              (c) Andy Gill 2001,
-              (c) Oregon Graduate Institute of Science and Technology, 2001
-License     : BSD-style (see the file LICENSE)
-Maintainer  : ocean0yohsuke@gmail.com
-Stability   : experimental
-Portability : ---
-
-This module extended RWS monad in mtl(monad-transformer-library).
--}
-{-# LANGUAGE TypeFamilies #-}
-module DeepControl.Monad.Trans.RWS (
-    module Control.Monad.RWS,
-    MonadReader(..), MonadWriter(..), MonadState(..),
-
-    ) where 
-
-import DeepControl.Applicative
-import DeepControl.Monad.Trans
-
-import Control.Monad.Reader (MonadReader(..))
-import Control.Monad.Writer (MonadWriter(..))
-import Control.Monad.State (MonadState(..))
-import Control.Monad.RWS
-import Data.Monoid
-
-----------------------------------------------------------------------
--- Level-1
-
-instance (Monoid w) => MonadTransDown (RWST r w s) where
-    type TransDown (RWST r w s) = RWS r w s
-
-instance (Monoid w) => MonadTransCover (RWST r w s) where
-    (|*|) = RWST . ((*:)|$>>) . runRWS
-
-
diff --git a/DeepControl/Monad/Trans/Reader.hs b/DeepControl/Monad/Trans/Reader.hs
deleted file mode 100644
--- a/DeepControl/Monad/Trans/Reader.hs
+++ /dev/null
@@ -1,36 +0,0 @@
-{-|
-Module      : DeepControl.Monad.Trans.Reader
-Description : Extension for mtl's Contrl.Monad.Reader.
-Copyright   : (c) Andy Gill 2001,
-              (c) Oregon Graduate Institute of Science and Technology 2001,
-              (c) Jeff Newbern 2003-2007,
-              (c) Andriy Palamarchuk 2007,
-              (C) 2015 KONISHI Yohsuke,
-License     : BSD-style (see the file LICENSE)
-Maintainer  : ocean0yohsuke@gmail.com
-Stability   : experimental
-Portability : ---
-
-This module extended Reader monad of mtl(monad-transformer-library).
--}
-{-# LANGUAGE TypeFamilies #-}
-module DeepControl.Monad.Trans.Reader (
-    module Control.Monad.Reader,
-   
-    ) where 
-
-import DeepControl.Applicative
-import DeepControl.Monad.Trans
-
-import Control.Monad.Reader 
-
-----------------------------------------------------------------------
--- Level-1
-
-instance MonadTransDown (ReaderT r) where
-    type TransDown (ReaderT r) = Reader r
-
-instance MonadTransCover (ReaderT s) where
-    (|*|) = ReaderT . ((*:)|$>) . runReader
-
-
diff --git a/DeepControl/Monad/Trans/State.hs b/DeepControl/Monad/Trans/State.hs
deleted file mode 100644
--- a/DeepControl/Monad/Trans/State.hs
+++ /dev/null
@@ -1,90 +0,0 @@
-{-|
-Module      : DeepControl.Monad.Trans.State
-Description : Extension for mtl's Contrl.Monad.State.
-Copyright   : (c) Andy Gill 2001,
-              (c) Oregon Graduate Institute of Science and Technology, 2001,
-              (C) 2015 KONISHI Yohsuke,
-License     : BSD-style (see the file LICENSE)
-Maintainer  : ocean0yohsuke@gmail.com
-Stability   : experimental
-Portability : ---
-
-This module extended State monad of mtl(monad-transformer-library).
--}
-{-# LANGUAGE TypeFamilies #-}
---{-# LANGUAGE TypeSynonymInstances #-}
---{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-module DeepControl.Monad.Trans.State (
-    module Control.Monad.State,
-
-    -- * Level-2
-    -- StateT2(..), runStateT2,
-
-    ) where 
-
-import DeepControl.Applicative
-import DeepControl.Monad.Trans
-
-import Control.Monad.State 
-
--- import DeepControl.Monad
--- import DeepControl.Monad.Trans.Identity
-
-----------------------------------------------------------------------
--- Level-1
-
-instance MonadTransDown (StateT s) where
-    type TransDown (StateT s) = State s
-
-instance MonadTransCover (StateT s) where
-    (|*|) = StateT . ((*:)|$>) . runState
-
-----------------------------------------------------------------------
--- Level-2
-
-{-
-newtype StateT2 s m1 m2 a = StateT2 (StateT s (IdentityT2 m1 m2) a)
-  deriving (Functor, Applicative, Monad, MonadIO)
-
-stateT2 :: (s -> m1 (m2 (a, s))) -> StateT2 s m1 m2 a
-stateT2 = StateT2 . StateT . (IdentityT2|$>)
-runStateT2 :: StateT2 s m1 m2 a -> s -> m1 (m2 (a, s))
-runStateT2 (StateT2 x) = (runIdentityT2|$>) . runStateT $ x 
-
-instance MonadTrans2 (StateT2 s) where
-    lift2 x = stateT2 $ \s -> x <<$|(,)|** s
-
-instance MonadTrans2Down (StateT2 s) where
-    type Trans2Down (StateT2 s) = StateT s
-
-instance MonadTransFold2 (StateT2 s) where
-    transfold2 x = StateT $ trans |$> runStateT2 x
-    untransfold2 x = stateT2 $ untrans |$> runStateT x
-
-instance MonadTransCover2 (StateT2 s) where
-    (|-*|) = stateT2 . ((-*)|$>) . runStateT
-    (|*-|) = stateT2 . ((*-)|$>) . runStateT
--}
-
-{-
-type StateT2 s m1 m2 a = StateT s (IdentityT2 m1 m2) a
-
-stateT2 :: (s -> m1 (m2 (a, s))) -> StateT2 s m1 m2 a
-stateT2 = StateT . (IdentityT2|$>)
-runStateT2 :: StateT2 s m1 m2 a -> s -> m1 (m2 (a, s))
-runStateT2 = (runIdentityT2|$>) . runStateT
-
-instance MonadTrans2Down (StateT2 s) where
-    type Trans2Down (StateT2 s) = StateT s
-
--- TODO: error
-instance MonadTransFold2 (StateT2 s) where
-    transfold2 x = StateT $ trans |$> runStateT2 x
-    untransfold2 x = stateT2 $ untrans |$> runStateT x
-
-instance MonadTransCover2 (StateT2 s) where
-    (|-*|) = stateT2 . ((-*)|$>) . runStateT
-    (|*-|) = stateT2 . ((*-)|$>) . runStateT
--}
-
-
diff --git a/DeepControl/Monad/Trans/Writer.hs b/DeepControl/Monad/Trans/Writer.hs
--- a/DeepControl/Monad/Trans/Writer.hs
+++ b/DeepControl/Monad/Trans/Writer.hs
@@ -3,7 +3,7 @@
 Description : Extension for mtl's Contrl.Monad.Writer.
 Copyright   : (c) Andy Gill 2001,
               (c) Oregon Graduate Institute of Science and Technology, 2001,
-              (C) 2015 KONISHI Yohsuke,
+              (c) 2015 KONISHI Yohsuke,
 License     : BSD-style (see the file LICENSE)
 Maintainer  : ocean0yohsuke@gmail.com
 Stability   : experimental
@@ -20,9 +20,9 @@
     -- * Level-3
     listen3, pass3,
     -- * Level-4
-    --listen4, pass4,
+    listen4, pass4,
     -- * Level-5
-    --listen5, pass5,
+    listen5, pass5,
 
     ) where 
 
@@ -37,14 +37,6 @@
 import Data.Monoid
 
 ----------------------------------------------------------------------
--- Level-1
-
-instance (Monoid w) => Commutative (Writer w) where
-    commute x = 
-        let (a, b) = runWriter x
-        in  (WriterT . Identity) |$> (a <$|(,)|* b)
-
-----------------------------------------------------------------------
 -- Level-2
 
 instance (Monoid w) => Monad2 (Writer w) where
@@ -81,6 +73,11 @@
         f a <<<$| (\x -> runWriterT x >- \(Identity (b, w')) ->
                          WriterT $ Identity (b, w <> w'))
 
+listen4 :: (MonadWriter w m4, Applicative m1, Applicative m2, Applicative m3) => m1 (m2 (m3 (m4 a))) -> m1 (m2 (m3 (m4 (a, w))))
+listen4 m = listen3 |$> m
+pass4 :: (MonadWriter w m4, Applicative m1, Applicative m2, Applicative m3) => m1 (m2 (m3 (m4 (a, w -> w)))) -> m1 (m2 (m3 (m4 a)))
+pass4 m = pass3 |$> m
+
 ----------------------------------------------------------------------
 -- Level-5
 
@@ -89,4 +86,9 @@
         mv >>>>== \x -> runWriterT x >- \(Identity (a, w)) ->
         f a <<<<$| (\x -> runWriterT x >- \(Identity (b, w')) ->
                           WriterT $ Identity (b, w <> w'))
+
+listen5 :: (MonadWriter w m5, Applicative m1, Applicative m2, Applicative m3, Applicative m4) => m1 (m2 (m3 (m4 (m5 a)))) -> m1 (m2 (m3 (m4 (m5 (a, w)))))
+listen5 m = listen4 |$> m
+pass5 :: (MonadWriter w m5, Applicative m1, Applicative m2, Applicative m3, Applicative m4) => m1 (m2 (m3 (m4 (m5 (a, w -> w))))) -> m1 (m2 (m3 (m4 (m5 a))))
+pass5 m = pass4 |$> m
 
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -2,124 +2,9 @@
 
 A Haskell library that enables more deeper level style programming than the usual Control.xxx modules provide, especially for Applicative and Monad.
 
-## Installing with [Stack](https://github.com/commercialhaskell/stack/blob/master/doc/GUIDE.md)
-
-If you haven't installed Stack yet, install [Stack](https://github.com/commercialhaskell/stack#readme).
-
-If you have never even used Stack, launch the terminal and go to your working directory:
-
-    .../yourworkingdirectory$
-
-To create your own Stack new project folder, type as below:
-
-    ../yourworkingdirectory$ stack new yourproject simple
-    Downloading template "simple" to create project "yourproject" in yourproject/ ...
-    ...
-
-Go into your project folder:
-
-    ../yourworkingdirectory$ cd yourproject/
-
-To install GHC on your Stack project folder, type as below:
-
-    .../yourproject$ stack setup
-    stack will use a locally installed GHC
-
-Now start ghci and see if it works well.
-
-    .../yourproject$ stack ghci
-    ...
-    Prelude>
-
-### Fetch from [Stackage](http://www.stackage.org/)
-
-Add `deepcontrol` to your .cabal file:
-
-yourproject.cabal:
-
-      ...
-      build-depends:       ...
-                         , deepcontrol
-
-On your project folder run "stack build" to get Stack to install `deepcontrol` into your project.
-
-    .../yourproject$ stack build
-
-If Stack yields a messeage below, it means that `deepcontrol` failed to be resolved on yourproject's Stack resolver.
-Probably you will get this message since `deepcontrol` is just one of miner libraries yet.
-
-    .../yourproject$ stack build
-    While constructing the BuildPlan the following exceptions were encountered:
-    ...
-
-If you want to try other resolver, type as below:
-
-    .../yourproject$ stack init
-    Refusing to overwrite existing stack.yaml, please delete before running stack init or if you are sure use "--force"
-
-Please follow the message direction.
-
-### Fetch from [Hackage](https://hackage.haskell.org/package/deepcontrol)
-
-Ok, I(you) got `deepcontrol` isn't in Stackage. Then let's fetch `deepcontrol` from Hackage.
-Add `deepcontrol-0.4.1.1` to your extra-deps field in stack.yaml too:
-
-stack.yaml:
-
-    extra-deps:
-    ...
-    - deepcontrol-0.4.1.1
-
-And type as below:
-
-    .../yourproject$ stack build
-
-Stack must fetch and install `deepcontrol` automatically.
-
-    ../yourproject$ stack build
-    deepcontrol-0.4.1.1: configure
-    ...
-
-Now start ghci and see if it works well.
-
-    .../yourproject$ stack ghci
-    ...
-    Prelude> :m DeepControl.Applicative
-
-## Installing with Cabal
-
-`deepcontrol` is available from
-[Hackage](https://hackage.haskell.org/package/deepcontrol).
-
-Launch the terminal and go to your project folder:
-
-    .../yourproject$
-
-If you haven't done setup cabal sandbox on your project folder yet, type as below so that `deepcontrol` will be installed locally on your project folder:
-
-    .../yourproject$ cabal sandbox init
-    Writing a default package environment file to
-    ...
-
-To install `deepcontrol` on your project folder, type as below:
-
-    .../yourproject$ cabal update
-    Downloading the latest package list from hackage.haskell.org
-    ...
-    .../yourproject$ cabal install deepcontrol
-    Resolving dependencies...
-    ...
-
-Now start ghci and see if it works well.
-
-    .../yourproject$ cabal repl
-    ...
-
-    Prelude> :m DeepControl.Applicative
-
 ## Examples
 
-### [Applicative](https://hackage.haskell.org/package/deepcontrol-0.4.1.1/docs/DeepControl-Applicative.html)
+### [Applicative](https://hackage.haskell.org/package/deepcontrol-0.4.2.0/docs/DeepControl-Applicative.html)
 
 This module enables you to program in applicative style for more deeper level than the usual Applicative module expresses.
 You would soon realize exactly what more deeper level means by reading the example codes below in order.
@@ -174,18 +59,24 @@
     > filter (even <$|(&&)|*> (10 >) <$|(&&)|*> (5 <)) [1..100]
     [6,8]
 
-braket-cover notation
+braket-cover notation:
 
     > [(1+)] |* 2
     [3]
     > [1] <$|(+)|* 2
     [3]
-    > [1] <$|(+)|* 2 <$|(*)|* 3
-    [9]
 
-    > Just 1 <$|(,)|* 2
-    Just (1,2)
+    > (,) |$> ["a1","a2"] |* 'b'
+    [("a1",'b'),("a2",'b')]
 
+    > (,,) 'a' |$> ["b1","b2"] |* 'c'
+    [('a',"b1",'c'),('a',"b2",'c')]
+
+    > (,,,) 'a' |$> ["b1","b2"] |* 'c' |* 'd'
+    [('a',"b1",'c','d'),('a',"b2",'c','d')]
+    > (,,,) 'a' |$> ["b1","b2"] |* 'c' |*> ["d1","d2"]
+    [('a',"b1",'c',"d1"),('a',"b1",'c',"d2"),('a',"b2",'c',"d1"),('a',"b2",'c',"d2")]
+
     > 1 *| [(+2)]
     [3]
     > 1 *| [(+)] |* 2
@@ -250,27 +141,54 @@
     >    [0,1]  -*|[Just (+), Just (-), Just (*), Nothing]|*- Just 2
     [Just 2,Just 3,Just (-2),Just (-1),Just 0,Just 2,Nothing,Nothing]
 
-#### Level-3
+#### Level-3, Level-4 and Level-5
 
 Work well likewise.
 
-#### Level-4, Level-5
+### [Commutative](https://hackage.haskell.org/package/deepcontrol-0.4.2.0/docs/DeepControl-Commutative.html)
 
-Not completely written up yet.
+[], Maybe, Either, Except and Writer monads are all commutative each other.
 
-### [Monad](https://hackage.haskell.org/package/deepcontrol-0.4.1.1/docs/DeepControl-Monad.html)
+    > commute $ Just [1]
+    [Just 1]
+    > commute $ [Just 1]
+    Just [1]
 
+    > commute $ Right (Just 1)
+    Just (Right 1)
+    > commute $ Just (Right 1)
+    Right (Just 1)
+
+So these monads can be deepened to Monad2, Monad3, Monad4 and Monad5.
+
+### [Monad](https://hackage.haskell.org/package/deepcontrol-0.4.2.0/docs/DeepControl-Monad.html)
+
 This module enables you to program in Monad for more deeper level than the usual Monad module expresses.
 You would soon realize exactly what more deeper level means by reading the example codes below in order.
 
+### Level-0
+
+```haskell
+import DeepControl.Monad ((>-))
+
+plus :: Int -> Int -> Int
+plus x y = 
+    x >- \a ->   -- (>-) is the level-0 bind function, analogous for (>>=)
+    y >- \b ->
+    a + b
+
+-- > plus 3 4
+-- 7
+```
+
 #### Level-2
 
 ```haskell
 import DeepControl.Applicative ((**:))
 import DeepControl.Monad
 
-listlist :: [[String]]             -- List-List Monad
-listlist = [["a","b"]] >>== \x ->
+listlist :: [[String]]             -- List-List monad
+listlist = [["a","b"]] >>== \x ->  -- (>>==) is the level-2 bind function, analogous for (>>=)
            [[0],[1,2]] >>== \y ->
            (**:) $ x ++ show y
 
@@ -284,11 +202,11 @@
 import DeepControl.Monad.Trans.Writer
 
 factorial :: Int ->
-             Maybe (Writer [Int] Int)  -- Maybe-Writer Monad
+             Maybe (Writer [Int] Int)               -- Maybe-Writer Monad
 factorial n | n < 0  = (-*) Nothing
             | n == 0 = (*:) $ tell [0] >> return 1
-            | n > 0  = factorial (n-1) >>== \v ->
-                       tell [v] ->~
+            | n > 0  = factorial (n-1) >>== \v ->   
+                       tell [v] ->~                 -- (->~) is a level-2 bind-cover function, analogous for (>>)
                        (**:) (n * v)
 
 -- > runWriter |$> factorial 5
@@ -303,12 +221,12 @@
 import DeepControl.Monad.Trans.Writer
 
 factorial :: Int ->
-             IO (Maybe (Writer [Int] Int))    -- IO-Maybe-Writer Monad
+             IO (Maybe (Writer [Int] Int))            -- IO-Maybe-Writer Monad
 factorial n | n < 0  = (*-*) Nothing
             | n == 0 = (**:) $ tell [0] >> return 1
-            | n > 0  = factorial (n-1) >>>== \v ->
-                       print v >--~
-                       tell [v] -->~
+            | n > 0  = factorial (n-1) >>>== \v ->    -- (>>>==) is the level-3 bind function, analogous for (>>=)
+                       print v >--~                   -- (>--~) is a level-3 bind-cover function, analogous for (>>)
+                       tell [v] -->~                  -- (-->~) is a level-3 bind-cover function too, analogous for (>>)
                        (***:) (n * v)
 
 -- > runWriter |$>> factorial 5
@@ -319,8 +237,12 @@
 -- 24
 -- Just (120,[0,1,1,2,6,24])
 ```
-### [Monad-Transformer](https://hackage.haskell.org/package/deepcontrol-0.4.1.1/docs/DeepControl-Monad-Trans.html)
+#### Level-3, Level-4 and Level-5
 
+Work well likewise.
+
+### [Monad-Transformer](https://hackage.haskell.org/package/deepcontrol-0.4.2.0/docs/DeepControl-Monad-Trans.html)
+
 #### Level-2
 
 Here is a monad transformer example how to implement Ackermann function, improved to stop within a certain limit of time, with ReaderT-IdentityT2-IO-Maybe monad, a level-2 monad-transformation.
@@ -332,7 +254,7 @@
 import DeepControl.Monad.Morph ((|>|))
 import DeepControl.Monad.Trans (liftTT2, transfold2, untransfold2)
 import DeepControl.Monad.Trans.Identity
-import DeepControl.Monad.Trans.Reader
+import Control.Monad.Reader
 import Control.Monad.Trans.Maybe
 
 import System.Timeout (timeout)
@@ -370,39 +292,39 @@
 ackermann'' x y = (untransfold2 . IdentityT) |>| ackermann' x y -- You can get ReaderT-IdentityT2-IO-Maybe function from usual ReaderT-MaybeT-IO function
 ```
 
-Here is a monad transformer example showing that the monad morph is usable.
+Here is a monad transformer example showing how to use trans-cover functions.
 
 ```haskell
 import DeepControl.Applicative ((|$>))
 import DeepControl.Monad (Monad2)
 import DeepControl.Monad.Morph ((|>|))
 import DeepControl.Monad.Trans (liftT, (|*|), (|-*|), (|*-|))
-import DeepControl.Monad.Trans.Writer
 import DeepControl.Monad.Trans.Identity
-import DeepControl.Monad.Trans.State
+import DeepControl.Monad.Trans.Writer
+import Control.Monad.State
 
 tick :: State Int ()
 tick = modify (+1)
 
 tock                         ::                   StateT Int IO ()
 tock = do
-    (|*|) tick               :: (Monad      m) => StateT Int m  ()
-    liftT $ putStrLn "Tock!" :: (MonadTrans t) => t          IO ()
+    (|*|) tick               :: (Monad      m) => StateT Int m  ()  -- (|*|) is the level-1 trans-cover function, analogous for (*:)
+    liftT $ putStrLn "Tock!" :: (MonadTrans t) => t          IO ()  -- 'liftT' is the level-1 trans-lift function, alias to 'lift'
 
 -- λ> runStateT tock 0
 -- Tock!
 -- ((),1)
 
-save    :: StateT Int (Writer [Int]) ()
+save :: StateT Int (Writer [Int]) ()
 save = do
     n <- get
     liftT $ tell [n]
 
-program ::               StateT Int (IdentityT2 IO (Writer [Int])) ()
+program ::               StateT Int (IdentityT2 IO (Writer [Int])) () -- StateT-IdentityT2-IO-Writer monad, a level-2 monad-transform
 program = replicateM_ 4 $ do
-    ((|-*|).liftT) |>| tock
+    ((|-*|).liftT) |>| tock                                           -- (|-*|) is a level-2 trans-cover function, analogous for (-*)
         :: (Monad2 m) => StateT Int (IdentityT2 IO m             ) ()
-    ((|*-|).liftT) |>| save
+    ((|*-|).liftT) |>| save                                           -- (|*-|) is a level-2 trans-cover function, analogous for (*-)
         :: (Monad  m) => StateT Int (IdentityT2 m  (Writer [Int])) ()
 
 -- λ> execWriter |$> runIdentityT2 (runStateT program 0)
@@ -416,14 +338,14 @@
 
 Work well likewise.
 
-### [Monad-Morph](https://hackage.haskell.org/package/deepcontrol-0.4.1.1/docs/DeepControl-Monad-Morph.html)
+### [Monad-Morph](https://hackage.haskell.org/package/deepcontrol-0.4.2.0/docs/DeepControl-Monad-Morph.html)
 
 Here is a monad-morph example, a level-2 monad-morph.
 
 ```haskell
 import DeepControl.Monad.Morph
-import DeepControl.Monad.Trans.State
 import DeepControl.Monad.Trans.Writer
+import Control.Trans.State
 
 -- i.e. :: StateT Int Identity ()
 tick    :: State Int ()
@@ -431,7 +353,7 @@
 
 tock                        ::                   StateT Int IO ()
 tock = do
-    generalize |>| tick     :: (Monad      m) => StateT Int m  ()
+    generalize |>| tick     :: (Monad      m) => StateT Int m  ()  -- (|>|) is the level-1 trans-map function, analogous for (|$>)
     lift $ putStrLn "Tock!" :: (MonadTrans t) => t          IO ()
 
 -- λ> runStateT tock 0
@@ -448,7 +370,7 @@
 program = replicateM_ 4 $ do
     lift |>| tock
         :: (MonadTrans t) => StateT Int (t             IO) ()
-    generalize |>>| save
+    generalize |>>| save                                        -- (|>>|) is the level-2 trans-map function, analogous for (|$>>)
         :: (Monad      m) => StateT Int (WriterT [Int] m ) ()
 
 -- λ> execWriterT (runStateT program 0)
@@ -459,6 +381,8 @@
 -- [1,2,3,4]
 ```
 
-### [Commutative](https://hackage.haskell.org/package/deepcontrol-0.4.1.1/docs/DeepControl-Commutative.html)
+#### Level-3, Level-4 and Level-5
 
-### [Arrow](https://hackage.haskell.org/package/deepcontrol-0.4.1.1/docs/DeepControl-Arrow.html)
+Work well likewise.
+
+### [Arrow](https://hackage.haskell.org/package/deepcontrol-0.4.2.0/docs/DeepControl-Arrow.html)
diff --git a/deepcontrol.cabal b/deepcontrol.cabal
--- a/deepcontrol.cabal
+++ b/deepcontrol.cabal
@@ -1,5 +1,5 @@
 name:                deepcontrol
-version:             0.4.1.1
+version:             0.4.2.0
 synopsis:            Provide more deeper level style of programming than the usual Control.xxx modules express
 description:         This module enables more deeper level style of programming than the usual Control.xxx modules express, especially for Applicative and Monad.
 license:             BSD3
@@ -31,9 +31,6 @@
                      , DeepControl.Monad.Trans.Identity
                      , DeepControl.Monad.Trans.Except
                      , DeepControl.Monad.Trans.Writer
-                     , DeepControl.Monad.Trans.Reader
-                     , DeepControl.Monad.Trans.State
-                     , DeepControl.Monad.Trans.RWS
   -- other-modules:       
   other-extensions:    MultiParamTypeClasses
                      , FlexibleInstances
diff --git a/test/unit_Monad-Level1.hs b/test/unit_Monad-Level1.hs
--- a/test/unit_Monad-Level1.hs
+++ b/test/unit_Monad-Level1.hs
@@ -3,9 +3,9 @@
 
 import DeepControl.Applicative ((|$>))
 import DeepControl.Monad ((>-))
-import DeepControl.Monad.Trans.RWS
 import DeepControl.Monad.Trans.Except
 
+import Control.Monad.RWS
 import qualified Data.Map as M
 
 ------------------------------------------------
diff --git a/test/unit_Monad-Level2.hs b/test/unit_Monad-Level2.hs
--- a/test/unit_Monad-Level2.hs
+++ b/test/unit_Monad-Level2.hs
@@ -7,8 +7,8 @@
 import DeepControl.Monad.Trans
 import DeepControl.Monad.Trans.Except
 import DeepControl.Monad.Trans.Identity
-import DeepControl.Monad.Trans.State
 
+import Control.Monad.State
 import Control.Monad.Trans.Maybe
 
 -----------------------------------------------
diff --git a/test/unit_Monad.hs b/test/unit_Monad.hs
--- a/test/unit_Monad.hs
+++ b/test/unit_Monad.hs
@@ -3,9 +3,8 @@
 import DeepControl.Applicative
 import DeepControl.Monad
 import DeepControl.Monad.Trans.Writer
-import DeepControl.Monad.Trans.Reader
 import DeepControl.Monad.Trans.Identity
-
+import Control.Monad.Reader
 import Safe
 
 main :: IO ()
diff --git a/test/unit_MonadMorph.hs b/test/unit_MonadMorph.hs
--- a/test/unit_MonadMorph.hs
+++ b/test/unit_MonadMorph.hs
@@ -1,8 +1,8 @@
 import Test.HUnit hiding (State)
 
 import DeepControl.Monad.Morph
-import DeepControl.Monad.Trans.State
-import DeepControl.Monad.Trans.Writer
+import Control.Monad.Writer
+import Control.Monad.State
 
 -- i.e. :: StateT Int Identity ()
 tick    :: State Int ()
diff --git a/test/unit_MonadTrans-2.hs b/test/unit_MonadTrans-2.hs
--- a/test/unit_MonadTrans-2.hs
+++ b/test/unit_MonadTrans-2.hs
@@ -6,7 +6,7 @@
 import DeepControl.Monad.Morph ((|>|))
 import DeepControl.Monad.Trans (liftTT2, transfold2, untransfold2)
 import DeepControl.Monad.Trans.Identity
-import DeepControl.Monad.Trans.Reader
+import Control.Monad.Reader
 import Control.Monad.Trans.Maybe
 
 import System.Timeout (timeout)
diff --git a/test/unit_MonadTrans.hs b/test/unit_MonadTrans.hs
--- a/test/unit_MonadTrans.hs
+++ b/test/unit_MonadTrans.hs
@@ -4,9 +4,9 @@
 import DeepControl.Monad (Monad2)
 import DeepControl.Monad.Morph ((|>|))
 import DeepControl.Monad.Trans (liftT, (|*|), (|-*|), (|*-|))
-import DeepControl.Monad.Trans.Writer
 import DeepControl.Monad.Trans.Identity
-import DeepControl.Monad.Trans.State
+import DeepControl.Monad.Trans.Writer
+import Control.Monad.State
 
 tick :: State Int ()
 tick = modify (+1)
