--- a/monad→monoidal.agda	Wed Nov 29 01:13:13 2017 +0900
+++ b/monad→monoidal.agda	Thu Nov 30 11:06:56 2017 +0900
@@ -92,7 +92,6 @@
           idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x
           idlφ = {!!}
 
-
 Monad→Applicative : {l : Level } (m : Monad (Sets {l} ) ) → Applicative ( Monad.T m )
 Monad→Applicative monad = record {
          pure = pure
@@ -125,22 +124,31 @@
           left : {n : Level} { a b : Set n} → { x y : a → b } { h : a }  → ( x ≡ y ) → x h ≡ y h
           left {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k h ) eq 
           identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a )  <*> u ≡ u
-          identity {a} {u} = {!!}
+          identity {a} {u} =  Relation.Binary.PropositionalEquality.cong ( λ h → h u ) ( begin
+                 (  λ u →  pure ( id1 Sets a )  <*> u )
+             ≈⟨⟩
+                 ( λ u → μ  a (FMap F (λ k → FMap F k u) (η (a → a) (λ x → x)))) 
+             ≈⟨⟩
+                 ( λ h → μ  a (FMap F h (η (a → a) (λ x → x) )))  o (  λ u k →  FMap F k u )
+             ≈⟨ {!!} ⟩
+                 ( λ u →  u )
+             ∎ ) 
+             where
+                  open ≈-Reasoning Sets hiding ( _o_ )
           composition : { a b c : Obj Sets } { u : FObj F ( b → c ) } { v : FObj F (a → b ) } { w : FObj F a }
               → (( pure _・_ <*> u ) <*> v ) <*> w  ≡ u  <*> (v  <*> w)
-          composition {a} {b} {c} {u} {v} {w} = begin
-                 (( pure _・_ <*> u ) <*> v ) <*> w
-             ≡⟨⟩ 
-                μ  c (FMap F (λ k → FMap F k w) (μ  (a → c) (FMap F (λ k → FMap F k v) (μ ((a → b) → a → c)
-                    (FMap F (λ k → FMap F k u) (η ((b → c) → (a → b) → a → c) (λ f g x → f (g x))))))))
-             ≡⟨ {!!} ⟩ 
-                μ  c (FMap F (λ k → FMap F k (μ b (FMap F (λ k₁ → FMap F k₁ w) v))) u)
-             ≡⟨⟩ 
-                 u  <*> (v  <*> w)
-             ∎ 
+          composition {a} {b} {c} {u} {v} {w} = Relation.Binary.PropositionalEquality.cong ( λ h → h w ) ( begin 
+                 ( λ w →  (( pure _・_ <*> u ) <*> v ) <*> w  )
+             ≈⟨⟩ 
+                 ( λ w → μ c (FMap F (λ k → FMap F k w) (μ (a → c) (FMap F (λ k → FMap F k v)
+                   (μ ((a → b) → a → c) (FMap F (λ k → FMap F k u) (η ((b → c) → (a → b) → a → c) (λ f g x → f (g x)))))))))
+             ≈⟨ {!!} ⟩
+                 ( λ w → μ c (FMap F (λ k → FMap F k (μ b (FMap F (λ h → FMap F h w) v))) u) )
+             ≈⟨⟩ 
+                 ( λ w →  u <*> (v <*> w) )
+             ∎ ) 
              where
-                  open Relation.Binary.PropositionalEquality
-                  open Relation.Binary.PropositionalEquality.≡-Reasoning
+                  open ≈-Reasoning Sets
           homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a }  → pure f <*> pure x ≡ pure (f x)
           homomorphism = {!!}
           interchange : { a b : Obj Sets } { u : FObj F ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u