+Now where `gamma` is another function of type <code>F'('t) -> M(G'('t))</code>, we define:
+
+<pre>
+ gamma =<< phi a =def. ((join G') -v- (M gamma)) (phi a)
+ = ((join G') -v- (M gamma) -v- phi) a
+ = (gamma <=< phi) a
+</pre>
+
+Hence:
+
+<pre>
+ gamma <=< phi = (fun a -> gamma =<< phi a)
+</pre>
+
+`gamma =<< phi a` is called the operation of "binding" the function gamma to the monadic value `phi a`, and is usually written as `phi a >>= gamma`.
+
+With these definitions, our monadic laws become:
+
+
+<pre>
+ Where phi is a polymorphic function of type F('t) -> M(F'('t))
+ gamma is a polymorphic function of type G('t) -> M(G'('t))
+ rho is a polymorphic function of type R('t) -> M(R'('t))
+ and F' = G and G' = R,
+ and a ranges over values of type F('t),
+ and b ranges over values of type G('t),
+ and c 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))
+</pre>
+
+<pre>
+ (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)
+</pre>
+
+<pre>
+ (iii.1) (unit G') <=< γ = γ
+ whenever γ is a natural transformation from some FG' to MG'
+ ==>
+ (unit G') <=< gamma = gamma
+ whenever 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)
+ whenever γ is a natural transformation from G to some MR'G
+ ==>
+ gamma = gamma <=< (unit G)
+ whenever 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>