# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1513001305 -32400
# Node ID 96afaa736186f7a55ccf65b95f68abf83daa66ba
# Parent  e7c673eba848815abc6c479c7335b554c216de98
connected interchange

diff -r e7c673eba848 -r 96afaa736186 monad→monoidal.agda
--- a/monad→monoidal.agda	Mon Dec 11 22:03:32 2017 +0900
+++ b/monad→monoidal.agda	Mon Dec 11 23:08:25 2017 +0900
@@ -421,13 +421,11 @@
              ≈⟨ {!!} ⟩
                  ( λ x → (μ b o (FMap F (λ k → (η b o k ) x))) u )
              ≈⟨ {!!} ⟩
-                 ( λ x → (μ b o ( η (FObj F b) o  FMap F ( {!!} ))) u )
-             ≈⟨ {!!} ⟩
-                 ( λ x → (μ b o ((FMap F (FMap F  (λ f → f x) )) o η (FObj F (a → b) ))) u )
+                 ( λ x → (μ b o ( FMap F ( FMap F   (λ f → f x) )   o FMap F ( η (a → b) ))) u )
              ≈⟨ {!!} ⟩
-                 ( λ x → (((FMap F  (λ f → f x)  o μ (a → b)) o η (FObj F (a → b)))) u )
-             ≈⟨⟩
-                 ( λ x → ((FMap F  (λ f → f x) o (μ (a → b) o η (FObj F (a → b))))) u )
+                 ( λ x → ( (μ b o (FMap F ( FMap F   (λ f → f x) )) )  o FMap F ( η (a → b) )) u )
+             ≈⟨ {!!} ⟩
+                 ( λ x → ((FMap F  (λ f → f x) o (μ (a → b) o FMap F ( η (a → b) )))) u )
              ≈⟨ {!!} ⟩
                  ( λ x → ((FMap F (λ f → f x) o id1 Sets (FObj F (a → b)))) u )
              ≈⟨ {!!} ⟩