# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1513003421 -32400
# Node ID 37ddc82288326f5b0e5d10eac6379056cbe06e38
# Parent  96afaa736186f7a55ccf65b95f68abf83daa66ba
monad to applicative done.

diff -r 96afaa736186 -r 37ddc8228832 monad→monoidal.agda
--- a/monad→monoidal.agda	Mon Dec 11 23:08:25 2017 +0900
+++ b/monad→monoidal.agda	Mon Dec 11 23:43:41 2017 +0900
@@ -418,27 +418,31 @@
                  ( λ x → μ  b (FMap F (λ k → FMap F k (η  a x)) u)) 
              ≈⟨⟩
                  ( λ x → (μ b o (FMap F (λ k → (FMap F k o η  a) x))) u )
-             ≈⟨ {!!} ⟩
-                 ( λ x → (μ b o (FMap F (λ k → (η b o k ) x))) u )
-             ≈⟨ {!!} ⟩
+             ≈⟨  extensionality Sets ( λ x → ≡cong ( λ h → ( μ b o h) u ) (fcong F (  extensionality Sets ( λ k →  ≡cong ( λ h → h x ) ( nat ( Monad.η monad ))))))  ⟩
+                 ( λ x → (μ b o FMap F (λ k → (η b o k ) x)) u )
+             ≈⟨⟩
+                  (λ x → (μ b o FMap F ( η b o (λ f → f x) )) u) 
+             ≈↑⟨  extensionality Sets ( λ x → ≡cong ( λ h → ( μ b o h) u ) ( fcong F (nat ( Monad.η monad ) )))  ⟩
+                  (λ x → (μ b o FMap F ( FMap F (λ f → f x) o η (a → b) )) u) 
+             ≈⟨  extensionality Sets ( λ x → ≡cong ( λ h → ( μ b o h) u ) ( distr F ) ) ⟩
                  ( λ x → (μ b o ( FMap F ( FMap F   (λ f → f x) )   o FMap F ( η (a → b) ))) u )
-             ≈⟨ {!!} ⟩
+             ≈⟨⟩
                  ( λ x → ( (μ b o (FMap F ( FMap F   (λ f → f x) )) )  o FMap F ( η (a → b) )) u )
-             ≈⟨ {!!} ⟩
+             ≈↑⟨ extensionality Sets ( λ x → ≡cong ( λ h → ( h  o FMap F ( η (a → b) )) u ) ( nat ( Monad.μ monad )))  ⟩
                  ( λ x → ((FMap F  (λ f → f x) o (μ (a → b) o FMap F ( η (a → b) )))) u )
-             ≈⟨ {!!} ⟩
+             ≈⟨ extensionality Sets ( λ x → ≡cong ( λ h → (FMap F  (λ f → f x) o h ) u ) ( IsMonad.unity2 ( Monad.isMonad monad ) ))  ⟩
                  ( λ x → ((FMap F (λ f → f x) o id1 Sets (FObj F (a → b)))) u )
-             ≈⟨ {!!} ⟩
+             ≈⟨ extensionality Sets ( λ x → ≡cong ( λ h → h u ) ( idR {_} {_} {FMap F (λ f → f x)} ))  ⟩
                  ( λ x → ( FMap F (λ f → f x) ) u )
-             ≈⟨ {!!} ⟩
+             ≈↑⟨ extensionality Sets ( λ x → ≡cong ( λ h → h u ) ( idL {_} {_} { FMap F (λ f → f x) }) )  ⟩
                  ( λ x → (id1 Sets (FObj F b ) o  FMap F (λ f → f x) ) u )
-             ≈⟨ {!!} ⟩
+             ≈↑⟨ extensionality Sets ( λ x → ≡cong ( λ h → (h  o  FMap F (λ f → f x)  ) u ) ( IsMonad.unity1 ( Monad.isMonad monad ) ))  ⟩
                  ( λ x → (( μ b o  η (FObj F b )) o  FMap F (λ f → f x) ) u )
              ≈⟨⟩
                  ( λ x → ( μ b o ( η (FObj F b ) o  FMap F (λ f → f x)))  u )
              ≈⟨⟩
                  ( λ x → ( μ b o ( η (FObj F b ) o  (λ k → FMap F k u)   )) (λ f → f x) )
-             ≈⟨ {!!} ⟩
+             ≈↑⟨ extensionality Sets ( λ x → ≡cong ( λ h → ( μ b o h ) (λ f → f x) ) ( nat ( Monad.η monad )))  ⟩
                  ( λ x → ( μ b o ((FMap F (λ k → FMap F k u) ) o η ((f : a → b) → b))) (λ f → f x) )
              ≈⟨⟩
                  ( λ x → (( μ b o (FMap F (λ k → FMap F k u) )) o η ((f : a → b) → b)) (λ f → f x) )