((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 γ) φ)
+ ((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 γ) φ)
+ ((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (join MR') (MM ρ) (M γ) φ)
- which will be true for all ρ,γ,φ just in case:
+ which will be true for all ρ,γ,φ only when:
((join R') (M join R')) = ((join R') (join MR')), for any R'.
- which will in turn be true just in case:
-
+ which will in turn be true when:
(ii') (join (M join)) = (join (join M))