Finally, we substitute <code>((join G') -v- (M γ) -v- φ)</code> for <code>γ <=< φ</code> in the monad laws. For simplicity, I'll omit the "-v-".
<pre>
- for all φ,γ,ρ in T, where φ is a transformation from F to MF', γ is a transformation from G to MG', R is a transformation from R to MR', and F'=G and G'=R:
+ For all ρ, γ, φ in T,
+ where φ is a transformation from F to MF',
+ γ is a transformation from G to MG',
+ ρ is a transformation from R to MR',
+ and F'=G and G'=R:
- (i) γ <=< φ etc are also in T
+ (i) γ <=< φ etc are also in T
==>
- (i') ((join G') (M γ) φ) etc are also in T
+ (i') ((join G') (M γ) φ) etc are also in T
- (ii) (ρ <=< γ) <=< φ = ρ <=< (γ <=< φ)
+
+ (ii) (ρ <=< γ) <=< φ = ρ <=< (γ <=< φ)
==>
(ρ <=< γ) is a transformation from G to MR', so:
(ρ <=< γ) <=< φ becomes: (join R') (M (ρ <=< γ)) φ
substituting in (ii), and helping ourselves to associativity on the rhs, we get:
((join R') (M ((join R') (M ρ) γ)) φ) = ((join R') (M ρ) (join G') (M γ) φ)
- ---------------------
+
which by the distributivity of functors over composition, and helping ourselves to associativity on the lhs, yields:
- ------------------------
+
((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (M ρ) (join G') (M γ) φ)
- ---------------
+
which by lemma 1, with ρ a transformation from G' to MR', yields:
- -----------------
+
((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (join MR') (MM ρ) (M γ) φ)
which will be true for all ρ,γ,φ just in case:
which will in turn be true just in case:
- (ii') (join (M join)) = (join (join M))
+ (ii') (join (M join)) = (join (join M))
+
+ (iii.1) (unit G') <=< γ = γ
+ when γ is a natural transformation from some FG' to MG'
(iii.1) (unit F') <=< φ = φ
==>
(unit F') is a transformation from F' to MF', so:
(iii.1') (join (M unit) = the identity transformation
+
+
+ (iii.2) γ = γ <=< (unit G)
+ when γ is a natural transformation from G to some MR'G
(iii.2) φ = φ <=< (unit F)
==>
φ is a transformation from F to MF', so: