--- a/monad→monoidal.agda	Sat Dec 02 09:18:20 2017 +0900
+++ b/monad→monoidal.agda	Mon Dec 04 12:36:43 2017 +0900
@@ -125,7 +125,7 @@
           left {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k h ) eq 
           ≡cong = Relation.Binary.PropositionalEquality.cong
           identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a )  <*> u ≡ u
-          identity {a} {u} =  Relation.Binary.PropositionalEquality.cong ( λ h → h u ) ( begin
+          identity {a} {u} =  ≡cong ( λ h → h u ) ( begin
                  (  λ u →  pure ( id1 Sets a )  <*> u )
              ≈⟨⟩
                  ( λ u → μ  a (FMap F (λ k → FMap F k u) (η (a → a) (λ x → x)))) 
@@ -148,7 +148,7 @@
                   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} = Relation.Binary.PropositionalEquality.cong ( λ h → h w ) ( begin 
+          composition {a} {b} {c} {u} {v} {w} = ≡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)
@@ -161,7 +161,28 @@
              where
                   open ≈-Reasoning Sets
           homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a }  → pure f <*> pure x ≡ pure (f x)
-          homomorphism = {!!}
+          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)) ))
+             ≈⟨ {!!} ⟩
+                 ( λ x → η  b (f x) )
+             ≈⟨⟩
+                 ( λ x →  pure (f x ))
+             ∎ )
+             where
+                  open ≈-Reasoning Sets
           interchange : { a b : Obj Sets } { u : FObj F ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u
-          interchange = {!!}
+          interchange {a} {b} {u} {x} =  ≡cong ( λ h → h x ) ( begin
+                 ( λ x →  u <*> pure x )
+             ≈⟨⟩
+                 ( λ x → μ  b (FMap F (λ k → FMap F k (η  a x)) u)) 
+             ≈⟨ {!!} ⟩
+                 ( λ x → μ  b (FMap F (λ k → FMap F k u) (η  ((f : a → b) → b) (λ f → f x))) )
+             ≈⟨⟩
+                 ( λ x →   pure (λ f → f x) <*> u )
+             ∎ )
+             where
+                  open ≈-Reasoning Sets
 
+