# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1512173900 -32400
# Node ID c1362961132a19d1731e64918c671f9ef2352adf
# Parent  84147ef7cada22a20597e1e408fa933c6395d9e9
...

diff -r 84147ef7cada -r c1362961132a monad→monoidal.agda
--- a/monad→monoidal.agda	Sat Dec 02 00:30:44 2017 +0900
+++ b/monad→monoidal.agda	Sat Dec 02 09:18:20 2017 +0900
@@ -131,16 +131,16 @@
                  ( λ u → μ  a (FMap F (λ k → FMap F k u) (η (a → a) (λ x → x)))) 
              ≈⟨⟩
                  (λ u → μ a ((FMap F (λ k → FMap F k u) o η (a → a)) (id1 Sets a ))) 
-             ≈⟨  ≡cong ( λ h → λ u → μ a (h u (id1 Sets a) ) ) ( extensionality Sets ( λ x → (IsNTrans.commute (NTrans.isNTrans  (Monad.η monad ) )))) ⟩
-                 (λ u → μ a ((η (FObj F a) o FMap F (id1 Sets a)) u ) )
-             ≈⟨ ≡cong ( λ h →  (λ u → μ a ( ( η (FObj F a) o  h)  u ))) (IsFunctor.identity (Functor.isFunctor F ))   ⟩
-                 (λ u → μ a ((η (FObj F a) o id1 Sets (FObj F a)) u ) )
-             ≈⟨ ≡cong ( λ h →  (λ u → μ a ( h  u ))) idR ⟩
-                 (λ u → μ a (η (FObj F a) u))
+             ≈⟨ ≡cong ( λ h → λ u → μ a (h u (id1 Sets a) ) ) ( extensionality Sets ( λ x → (IsNTrans.commute (NTrans.isNTrans  (Monad.η monad ) )))) ⟩
+                 (λ u → μ a ( (η (FObj F a) o FMap F (  (id1 Sets a )) ) u )  ) 
              ≈⟨⟩
-                  μ  a o η  (FObj F a) 
+                 μ a o (η (FObj F a) o FMap F (id1 Sets a))  
+             ≈⟨ ≡cong ( λ h →  (λ u → μ a ( ( η (FObj F a) o  h)  u ))) (IsFunctor.identity (Functor.isFunctor F ))   ⟩ -- cdr cdr
+                 μ a o (η (FObj F a) o id1 Sets (FObj F a))  
+             ≈⟨ ≡cong ( λ h →  (λ u → μ a ( h  u ))) idR ⟩  -- cdr idR
+                 μ  a o η  (FObj F a) 
              ≈⟨ IsMonad.unity1 (Monad.isMonad monad )   ⟩
-                  id1 Sets (FObj F a) 
+                 id1 Sets (FObj F a) 
              ≈⟨⟩
                  ( λ u →  u )
              ∎ )