Signed-off-by: Jim Pryor <profjim@jimpryor.net>
==>
(unit G') is a transformation from G' to MG', so:
(unit G') <=< γ becomes: ((join G') (M unit G') γ)
==>
(unit G') is a transformation from G' to MG', so:
(unit G') <=< γ becomes: ((join G') (M unit G') γ)
- which is: ((join G') (M unit G') γ)
substituting in (iii.1), we get:
((join G') (M unit G') γ) = γ
substituting in (iii.1), we get:
((join G') (M unit G') γ) = γ
(iii.2) γ = γ <=< (unit G)
when γ is a natural transformation from G to some MR'G
==>
(iii.2) γ = γ <=< (unit G)
when γ is a natural transformation from G to some MR'G
==>
- unit <=< γ becomes: (join R'G) (M γ) unit
+ unit <=< γ becomes: ((join R'G) (M γ) unit)
substituting in (iii.2), we get:
γ = ((join R'G) (M γ) (unit G))
substituting in (iii.2), we get:
γ = ((join R'G) (M γ) (unit G))
Collecting the results, our monad laws turn out in this format to be:
Collecting the results, our monad laws turn out in this format to be:
-</pre>
- when φ a transformation from F to MF', γ a transformation from F' to MG', ρ a transformation from G' to MR' are all in T:
+<pre>
+ 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') ((join G') (M γ) φ) etc also in T
(i') ((join G') (M γ) φ) etc also in T