+ (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`