# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1512723093 -32400
# Node ID c8e9786c273ad5c99ca330796e34e79be0e5d39f
# Parent  e33e9ae1514b2bce6a8556838e4d16ea2914e7cb
...

diff -r e33e9ae1514b -r c8e9786c273a monad→monoidal.agda
--- a/monad→monoidal.agda	Tue Dec 05 17:04:03 2017 +0900
+++ b/monad→monoidal.agda	Fri Dec 08 17:51:33 2017 +0900
@@ -91,21 +91,32 @@
              → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c))
           assocφ = {!!}
           idrφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡ x
-          idrφ {a} {x} = begin
-                  FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit))
-             ≡⟨⟩
-                  FMap F proj₁ (μ  (a * One) (FMap F (λ f → FMap F (λ g → f , g) (η  One OneObj)) x))
-             ≡⟨ {!!} ⟩
-                 FMap F proj₁ (μ  (a * One) (FMap F (λ f → η ( a * One ) (f , OneObj ) ) x )  ) 
-             ≡⟨ {!!} ⟩
-                 FMap F proj₁ ( FMap F (λ f → {!!}) ( μ {!!} (η {!!} x ) )  )
-             ≡⟨ {!!} ⟩
-                 id1 Sets {!!} x
-             ≡⟨ {!!} ⟩
-                  x
-             ∎ where
-                  open Relation.Binary.PropositionalEquality
-                  open Relation.Binary.PropositionalEquality.≡-Reasoning
+          idrφ {a} {x} =  monoidal.≡-cong ( λ h → h x ) ( begin
+                  ( λ x → FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) )
+             ≈⟨⟩
+                  ( λ x → FMap F proj₁ (μ (a * One) (FMap F (λ f → FMap F (λ g → f , g) (η  One OneObj)) x)) )
+             ≈⟨⟩
+                  ( λ x → FMap F proj₁      ((μ (a * One)  o  (FMap F (λ f → FMap F (λ g → f , g) (η  One OneObj)))) x)) 
+             ≈⟨⟩
+                  ( λ x → ( FMap F proj₁ o ( (μ (a * One ) o  λ y → FMap F (λ f →  FMap F ( λ g → ( f , g )) y )  x ) o η One )) OneObj )
+             ≈⟨ {!!} ⟩
+                  ( λ x → ( FMap F proj₁ o (( μ ( a  * One ) o FMap F {!!} ) o  η (FObj F a ))) x )
+             ≈⟨⟩
+                  FMap F proj₁ o (( μ ( a  * One ) o FMap F {!!} ) o  η (FObj F a )) 
+             ≈⟨ cdr ( car (nat ( Monad.μ monad )))   ⟩
+                  FMap F proj₁ o (( FMap F {!!} o μ a ) o  η (FObj F a )) 
+             ≈⟨ cdr assoc ⟩
+                  FMap F proj₁ o ( FMap F {!!} o ( μ a  o  η (FObj F a ))) 
+             ≈⟨ {!!} ⟩
+                  FMap F proj₁ o ( FMap F {!!} o id1 Sets (FObj F a ) ) 
+             ≈⟨ cdr idR ⟩
+                  FMap F proj₁  o FMap F  (λ z → z , {!!} )
+             ≈↑⟨ distr F  ⟩
+                  FMap F (id1 Sets a )
+             ≈⟨ IsFunctor.identity ( Functor.isFunctor F ) ⟩
+                 id1 Sets (FObj F a)
+             ∎ ) where
+                  open ≈-Reasoning Sets hiding ( _o_ )
           idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x
           idlφ = {!!}