# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1512960304 -32400
# Node ID 03f09d7dfffdd1b56e82d8ce6eab4da40533c3fb
# Parent  a1c3d82be8c8e9cb233ae95aa91500b2b1387101
...

diff -r a1c3d82be8c8 -r 03f09d7dfffd monad→monoidal.agda
--- a/monad→monoidal.agda	Mon Dec 11 11:01:23 2017 +0900
+++ b/monad→monoidal.agda	Mon Dec 11 11:45:04 2017 +0900
@@ -319,8 +319,30 @@
                  ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F (λ k → FMap F k v)  o (
                         μ ((a → b) → a → c)  o  (FMap F (λ k → FMap F k u)  o η ((b → c) → (a → b) → a → c))
                      ) ) ) ) ) (λ f g x → f (g x))  )
+             ≈⟨ {!!} ⟩ -- nat η
+                 ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F (λ k → FMap F k v)  o (
+                        μ ((a → b) → a → c)  o  (η (FObj F ((a → b) → a → c)) o (λ k → FMap F k u)   )
+                     ) ) ) ) ) (λ f g x → f (g x))  )
+             ≈⟨ {!!} ⟩ -- assoc
+                 ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F (λ k → FMap F k v)  o (
+                        ( μ ((a → b) → a → c)  o  η (FObj F ((a → b) → a → c)) ) o (λ k → FMap F k u)   
+                     ) ) ) ) ) (λ f g x → f (g x))  )
+             ≈⟨ {!!} ⟩ 
+                 ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F (λ k → FMap F k v)  o (
+                        id1 Sets (FObj (Monad.T monad) ((a → b) → a → c))  o (λ k → FMap F k u)   
+                     ) ) ) ) ) (λ f g x → f (g x))  )
+             ≈⟨ {!!} ⟩ -- idR
+                 ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F (λ k → FMap F k v)  o (
+                         λ k → FMap F k u   
+                     ) ) ) ) ) (λ f g x → f (g x))  )
+             ≈⟨⟩ 
+                 ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o (  λ j → ( FMap F (λ k → FMap F k v)  o  FMap F j ) u ))))  (λ f g x → f (g x))  )
              ≈⟨ {!!} ⟩
-                 ( λ 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 w) o ( μ (a → c) o (  λ j → ( FMap F (( λ k → FMap F k v)  o   j ) u )))))  (λ f g x → f (g x))  )
+             ≈⟨⟩
+                 ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F ((λ k → FMap F k v) o (λ f g x → f (g x)) ))   ))) 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) )
              ≈⟨⟩