--- a/monad→monoidal.agda	Sat Dec 09 11:51:30 2017 +0900
+++ b/monad→monoidal.agda	Sun Dec 10 11:28:03 2017 +0900
@@ -96,15 +96,9 @@
              ≈⟨⟩
                   ( λ 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)) 
+                  FMap F proj₁ o  (μ (a * One ) o FMap F (λ f → ( FMap F (λ g → f , g) ((η One) OneObj))))
              ≈⟨⟩
-                  ( λ 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  (( λ 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 η One ) )) OneObj )
-             ≈⟨ {!!} ⟩
-                  ( λ x → ( FMap F proj₁ o ( μ (a * One ) o  ( η (FObj F (a * One ) ) o FMap F (λ f → ( f , OneObj ) )) )) x )
+                  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 )    ) )
              ≈⟨⟩
@@ -126,7 +120,16 @@
              ∎ ) where
                   open ≈-Reasoning Sets hiding ( _o_ )
           idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x
-          idlφ = {!!}
+          idlφ {a} {x} =  monoidal.≡-cong ( λ h → h x ) ( begin
+                 ( λ x → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) )
+             ≈⟨⟩
+                 ( λ x → FMap F proj₂ (μ (One * a ) (FMap F (λ f → FMap F (λ g → f , g) x) (η  One OneObj))))
+             ≈⟨ {!!} ⟩
+                  FMap F (id1 Sets a )
+             ≈⟨ IsFunctor.identity ( Functor.isFunctor F ) ⟩
+                 id1 Sets (FObj F a)
+             ∎ ) where
+                  open ≈-Reasoning Sets hiding ( _o_ )
 
 Monad→Applicative : {l : Level } (m : Monad (Sets {l} ) ) → Applicative ( Monad.T m )
 Monad→Applicative monad = record {