# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1512981209 -32400
# Node ID 74d197dd8a682e42b1be0395239a62708e33a318
# Parent  a4074765abf8d8ab597c936527aba6a7c5eb020a
composition connected

diff -r a4074765abf8 -r 74d197dd8a68 monad→monoidal.agda
--- a/monad→monoidal.agda	Mon Dec 11 15:58:52 2017 +0900
+++ b/monad→monoidal.agda	Mon Dec 11 17:33:29 2017 +0900
@@ -351,16 +351,30 @@
                  ( λ w → ( μ c o (μ (FObj F c)  o ( FMap F (FMap F (λ k → FMap F k w)  o ((λ k → FMap F k v) o (λ f g x → f (g x)) )))))  u )
              ≈⟨⟩
                  ( λ w → (( μ c o μ (FObj F c) ) o ( FMap F (FMap F (λ k → FMap F k w)  o ((λ k → FMap F k v) o (λ f g x → f (g x)) ))    ))  u )
-             ≈⟨ {!!} ⟩
+             ≈⟨ {!!} ⟩  -- Monad assoc
                  ( λ w → (( μ c o (FMap F ( μ c )) ) o ( FMap F (FMap F (λ k → FMap F k w)  o ((λ k → FMap F k v) o (λ f g x → f (g x)) ))    ))  u )
              ≈⟨⟩
                  ( λ w → ( μ c o (FMap F ( μ c ) o ( FMap F (FMap F (λ k → FMap F k w)  o ((λ k → FMap F k v) o (λ f g x → f (g x)) )) )))    u )
              ≈⟨ {!!} ⟩
                  ( λ w → ( μ c o (FMap F ( μ c  o (FMap F (λ k → FMap F k w)  o ((λ k → FMap F k v) o (λ f g x → f (g x)) )) )))   u )
-             ≈⟨ {!!} ⟩
-                 ( λ w → ( μ c o (FMap F ( (λ x → ( μ c  o (FMap F (λ k → FMap F k w)  o (FMap F (λ g x₁ → x (g x₁)) ) )) v )))) u )
+             ≈⟨⟩
+                 ( λ w → ( μ c o (FMap F (λ x →  ( μ c  o (FMap F (λ k → FMap F k w)  o (FMap F (λ g x₁ → x (g x₁))))) v ))) u )
+             ≈⟨ {!!} ⟩ 
+                 ( λ w → ( μ c o (FMap F (λ k →  ( μ c  o (FMap F ((λ x → FMap F x w)  o (λ g x₁ → k (g x₁))))) v ))) u )
+             ≈⟨⟩ 
+                 ( λ w → ( μ c o (FMap F (λ k →  ( μ c  o (FMap F ((λ x → (FMap F ( k o  x ) w))))            ) v ))) u ) 
              ≈⟨ {!!} ⟩ 
-                 ( λ w → ( μ c o (FMap F (λ k → ( FMap F k o ( μ b  o FMap F  (λ h → FMap F h w))) v ))  ) u ) 
+                 ( λ w → ( μ c o (FMap F (λ k →  ( μ c  o (FMap F ((λ x → (FMap F k  o  FMap F x ) w)))       ) v ))) u ) 
+             ≈⟨⟩ 
+                 ( λ w → ( μ c o (FMap F (λ k →  ( μ c  o (FMap F (FMap F k  o (λ h → FMap F h w)))           ) v ))) u ) 
+             ≈⟨ {!!} ⟩ 
+                 ( λ w → ( μ c o (FMap F (λ k →  (( μ c o ( FMap F (FMap F k ) o FMap F  (λ h → FMap F h w)))         ) v ))) u ) 
+             ≈⟨⟩ 
+                 ( λ w → ( μ c o (FMap F (λ k →  ((( μ c o FMap F (FMap F k )) o FMap F  (λ h → FMap F h w))          ) v ))) u ) 
+             ≈⟨ {!!} ⟩ 
+                 ( λ w → ( μ c o (FMap F (λ k →  ((( FMap F k o  μ b ) o FMap F  (λ h → FMap F h w))          ) v ))) u ) 
+             ≈⟨⟩ 
+                 ( λ w → ( μ c o (FMap F (λ k →  ( FMap F k o ( μ b  o FMap F  (λ h → FMap F h w))            ) v ))) u ) 
              ≈⟨⟩ 
                  ( λ w → μ c (FMap F (λ k → FMap F k (μ b (FMap F (λ h → FMap F h w) v))) u) )
              ≈⟨⟩