-A natural transformation t assigns to each type C1 in <b>C</b> a morphism t[C1]: C1→M(C1) such that, for every f:C1→C2:
- t[C2] ∘ f = M(f) ∘ t[C1]
+<pre>
+ (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 F(G'('t)) -> M(G'('t))
+
+ fun b -> (unit G') =<< gamma b = gamma
+
+ (unit G') =<< gamma b = gamma b
+
+ Let return be a polymorphic function mapping arguments of any
+ type 't to M('t). In particular, it maps arguments c of type
+ G'('t) to the monadic value (unit G') c, of type M(G'('t)).
+
+ (iii.1'') return =<< gamma b = gamma b
+</pre>
+
+<pre>
+ (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
+
+ As above, return will map 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>