# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1512883811 -32400
# Node ID a83145326258ddfcb9eeb3b8c23cc9d6571ed9fe
# Parent  37bffde965b3f94e3fc836c38843bac4fcfd09c0
yellow on idrφ

diff -r 37bffde965b3 -r a83145326258 monad→monoidal.agda
--- a/monad→monoidal.agda	Sun Dec 10 11:28:03 2017 +0900
+++ b/monad→monoidal.agda	Sun Dec 10 14:30:11 2017 +0900
@@ -99,21 +99,34 @@
                   FMap F proj₁ o  (μ (a * One ) o FMap F (λ f → ( FMap F (λ g → f , g) ((η One) OneObj))))
              ≈⟨⟩
                   FMap F proj₁ o  (μ (a * One ) o FMap F (λ f → ( FMap F (λ g → f , g) o η One ) OneObj ))
-             ≈⟨ {!!} ⟩
-                  FMap F proj₁ o ( μ (a * One ) o  ( η (FObj F (a * One ) ) o FMap F ((λ g → (λ f → ( f , g ) )) OneObj )    ) )
+             ≈⟨ cdr ( cdr ( fcong F  ( begin
+                   (λ f → ( FMap F (λ g → f , g) o η One ) OneObj )
+                 ≈⟨  monoidal.≡-cong ( λ h →  λ f → (h f) OneObj ) (extensionality Sets (λ f → (
+                      begin
+                         FMap F (λ g → f , g) o η One 
+                      ≈⟨ nat ( Monad.η monad ) ⟩
+                          η  ( a * One) o FMap identityFunctor (λ g → f , g) 
+                      ≈⟨⟩
+                         η (a * One) o ( λ g → ( f , g ) )
+                      ∎   
+                    ))) ⟩
+                   (λ f → ( η (a * One) o ( λ g → ( f , g ) ) ) OneObj )
+                 ≈⟨⟩
+                     η (a * One  ) o ( λ f → ( f , OneObj  ) )
+                 ∎
+                ))) ⟩
+                  FMap F proj₁ o  (μ (a * One ) o FMap F ( η (a * One  ) o ( λ f → ( f , OneObj  ))))
+             ≈⟨ cdr ( cdr ( distr F )) ⟩
+                  FMap F proj₁ o  (μ (a * One ) o ( FMap F ( η (a * One  )) o FMap F ( λ f → ( f , OneObj  ))))
+             ≈⟨ cdr assoc ⟩
+                  FMap F proj₁ o  ( ( μ (a * One ) o  FMap F ( η (a * One  ))) o FMap F ( λ f → ( f , OneObj  )))
+             ≈⟨ cdr  ( car ( IsMonad.unity2 (Monad.isMonad monad )))   ⟩
+                  FMap F proj₁ o  ( id1 Sets (FObj F (a * One)) o FMap F ( λ f → ( f , OneObj  )))
+             ≈⟨ cdr idL ⟩
+                  FMap F proj₁ o   FMap F ( λ f → ( f , OneObj  ))
+             ≈↑⟨ distr F  ⟩
+                  FMap F ( proj₁ o   ( λ f → ( f , OneObj  )))
              ≈⟨⟩
-                  FMap F proj₁ o ( μ (a * One ) o  ( η (FObj F (a * One ) ) o FMap F (λ f → ( f , OneObj ) )    ) )
-             ≈⟨ cdr ( cdr ( nat( Monad.η monad ) )) ⟩
-                  FMap F proj₁ o (( μ ( a  * One ) o FMap F  (FMap F (λ f → ( f , OneObj ) ) )) o  η (FObj F a )) 
-             ≈⟨ cdr ( car (nat ( Monad.μ monad )))   ⟩
-                  FMap F proj₁ o (( FMap F (λ f → ( f , OneObj )) o μ a ) o  η (FObj F a )) 
-             ≈⟨ cdr assoc ⟩
-                  FMap F proj₁ o ( FMap F (λ f → ( f , OneObj ))  o ( μ a  o  η (FObj F a ))) 
-             ≈⟨ cdr  ( cdr ( IsMonad.unity2 (Monad.isMonad monad )))   ⟩
-                  FMap F proj₁ o ( FMap F (λ f → ( f , OneObj ))  o id1 Sets (FObj F a ) ) 
-             ≈⟨ cdr idR ⟩
-                  FMap F proj₁  o FMap F  (λ z → z ,  λ f → ( f , OneObj )  )
-             ≈↑⟨ distr F  ⟩
                   FMap F (id1 Sets a )
              ≈⟨ IsFunctor.identity ( Functor.isFunctor F ) ⟩
                  id1 Sets (FObj F a)
@@ -198,19 +211,21 @@
                  ( λ w →  u <*> (v <*> w) )
              ∎ ) 
              where
-                  open ≈-Reasoning Sets
+                  open ≈-Reasoning Sets hiding ( _o_ )
           homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a }  → pure f <*> pure x ≡ pure (f x)
           homomorphism {a} {b} {f} {x} = ≡cong ( λ h → h x ) ( begin
                  ( λ x →  pure f <*> pure x )
              ≈⟨⟩
                  ( λ x → μ  b (FMap F (λ k → FMap F k (η  a x)) ((η  (a → b) f)) ))
              ≈⟨ {!!} ⟩
+                 η  b o  f 
+             ≈⟨⟩
                  ( λ x → η  b (f x) )
              ≈⟨⟩
                  ( λ x →  pure (f x ))
              ∎ )
              where
-                  open ≈-Reasoning Sets
+                  open ≈-Reasoning Sets hiding ( _o_ )
           interchange : { a b : Obj Sets } { u : FObj F ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u
           interchange {a} {b} {u} {x} =  ≡cong ( λ h → h x ) ( begin
                  ( λ x →  u <*> pure x )
@@ -222,6 +237,6 @@
                  ( λ x →   pure (λ f → f x) <*> u )
              ∎ )
              where
-                  open ≈-Reasoning Sets
+                  open ≈-Reasoning Sets hiding ( _o_ )