--- a/monad→monoidal.agda	Thu Nov 30 11:06:56 2017 +0900
+++ b/monad→monoidal.agda	Sat Dec 02 00:30:44 2017 +0900
@@ -60,7 +60,7 @@
                   μ (Σ c (λ v → d)) (FMap F (λ x₁ → FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) (FMap F (λ g₁ → x₁ , g₁) y)) x)
              ≡⟨⟩ 
                   (μ (Σ c (λ v → d)) ・ (FMap F (λ x₁ → FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) (FMap F (λ g₁ → x₁ , g₁) y)))) x
-             ≡⟨ {!!} ⟩ 
+             ≡⟨ sym (  ≡-cong ( λ h → (μ (Σ c (λ v → d)) ・ (FMap F (λ x₁ → ( h x₁ y )))) x ) ( extensionality Sets ( λ x → IsFunctor.distr ( Functor.isFunctor F )   )))  ⟩ 
                   (μ (Σ c (λ v → d)) ・ (FMap F (λ x₁ → FMap F ((λ xy → f (proj₁ xy) , g (proj₂ xy)) ・  (λ g₁ → x₁ , g₁) ) y))) x
              ≡⟨⟩ 
                  μ  (Σ c (λ v → d)) (FMap F (λ x₁ → FMap F (λ x₂ → f x₁ , g x₂) y) x)
@@ -70,13 +70,13 @@
                 μ  (Σ c (λ x₁ → d)) (FMap F (λ x₁ → FMap F (λ k → f x₁ , g k) y) x)
              ≡⟨⟩ 
                 μ  (Σ c (λ x₁ → d)) (FMap F ((λ f₁ → FMap F (λ k → f₁ , g k) y) ・ f) x)
-             ≡⟨ {!!} ⟩ 
+             ≡⟨  ≡-cong ( λ h → μ  (Σ c (λ x₁ → d)) (h x)) ( IsFunctor.distr ( Functor.isFunctor F ))  ⟩ 
                 μ  (Σ c (λ x₁ → d)) (((FMap F (λ f₁ → FMap F (λ k → f₁ , g k) y)) ・ (FMap F f)) x)
              ≡⟨⟩ 
                 μ  (Σ c (λ x₁ → d)) (FMap F (λ f₁ → FMap F (λ k → f₁ , g k) y) (FMap F f x))
              ≡⟨⟩ 
                   μ  (Σ c (λ x₁ → d)) (FMap F (λ f₁ → FMap F (λ k → ((λ g₁ → f₁ , g₁) (g k))) y) (FMap F f x))
-             ≡⟨ {!!}  ⟩ 
+             ≡⟨  ≡-cong ( λ h →  μ  (Σ c (λ x₁ → d)) (FMap F (λ f₁ → h f₁ y ) (FMap F f x ))) ( extensionality Sets ( λ x →  (IsFunctor.distr ( Functor.isFunctor F )  ) )) ⟩ 
                   μ  (Σ c (λ x₁ → d)) (FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) (FMap F g y)) (FMap F f x))
              ≡⟨⟩
                   φ (FMap F f x , FMap F g y)
@@ -123,14 +123,25 @@
           id x = x
           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 
+          ≡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
                  (  λ 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 → μ a ((FMap F (λ k → FMap F k u) o η (a → a)) (id1 Sets a ))) 
+             ≈⟨  ≡cong ( λ h → λ u → μ a (h u (id1 Sets a) ) ) ( extensionality Sets ( λ x → (IsNTrans.commute (NTrans.isNTrans  (Monad.η monad ) )))) ⟩
+                 (λ u → μ a ((η (FObj F a) o FMap F (id1 Sets a)) u ) )
+             ≈⟨ ≡cong ( λ h →  (λ u → μ a ( ( η (FObj F a) o  h)  u ))) (IsFunctor.identity (Functor.isFunctor F ))   ⟩
+                 (λ u → μ a ((η (FObj F a) o id1 Sets (FObj F a)) u ) )
+             ≈⟨ ≡cong ( λ h →  (λ u → μ a ( h  u ))) idR ⟩
+                 (λ u → μ a (η (FObj F a) u))
+             ≈⟨⟩
+                  μ  a o η  (FObj F a) 
+             ≈⟨ IsMonad.unity1 (Monad.isMonad monad )   ⟩
+                  id1 Sets (FObj F a) 
+             ≈⟨⟩
                  ( λ u →  u )
              ∎ ) 
              where