+<pre>
+ Where phi is a polymorphic function from type F('t) -> M F'('t)
+ and gamma is a polymorphic function from type G('t) -> M G' ('t)
+ and rho is a polymorphic function from type R('t) -> M R' ('t)
+ and F' = G and G' = R,
+ and a ranges over values of type F('t) for some type 't,
+ and b ranges over values of type G('t):
+
+ (i) γ <=< φ is defined,
+ and is a natural transformation from F to MG'
+ ==>
+ (i'') fun a -> gamma =<< phi a is defined,
+ and is a function from type F('t) -> M G' ('t)
+
+
+
+ (ii) (ρ <=< γ) <=< φ = ρ <=< (γ <=< φ)
+ ==>
+ (fun a -> (rho <=< gamma) =<< phi a) = (fun a -> rho =<< (gamma <=< phi) a)
+ (fun a -> (fun b -> rho =<< gamma b) =<< phi a) = (fun a -> rho =<< (gamma =<< phi a))
+
+ (ii'') (fun b -> rho =<< gamma b) =<< phi a = rho =<< (gamma =<< phi a)
+
+
+
+ (iii.1) (unit G') <=< γ = γ
+ when γ is a natural transformation from some FG' to MG'
+
+ (unit G') <=< gamma = gamma
+ when gamma is a function of type FQ'('t) -> M G'('t)
+
+ fun b -> (unit G') =<< gamma b = gamma
+
+ (unit G') =<< gamma b = gamma b
+
+ As below, return will map arguments c of type G'('t)
+ to the monadic value (unit G') b, of type M G'('t).
+
+ (iii.1'') return =<< gamma b = gamma b
+
+
+
+ (iii.2) γ = γ <=< (unit G)
+ when γ is a natural transformation from G to some MR'G
+ ==>
+ gamma = gamma <=< (unit G)
+ when gamma is a function of type G('t) -> M R' G('t)
+
+ gamma = fun b -> gamma =<< ((unit G) b)
+
+ Let return be a polymorphic function mapping arguments
+ of any type 't to M('t). In particular, it maps arguments
+ b of type G('t) to the monadic value (unit G) b, of
+ type M G('t).
+
+ gamma = fun b -> gamma =<< return b
+
+ (iii.2'') gamma b = gamma =<< return b
+</pre>
+
+Summarizing (ii''), (iii.1''), (iii.2''), these are the monadic laws as usually stated in the functional programming literature:
+
+* `fun b -> rho =<< gamma b) =<< phi a = rho =<< (gamma =<< phi a)`
+
+ Usually written reversed, and with a monadic variable `u` standing in
+ for `phi a`:
+
+ `u >>= (fun b -> gamma b >>= rho) = (u >>= gamma) >>= rho`
+
+* `return =<< gamma b = gamma b`