--- a/monoid-monad.agda	Thu Aug 15 03:34:00 2013 +0900
+++ b/monoid-monad.agda	Thu Aug 15 04:46:22 2013 +0900
@@ -94,20 +94,21 @@
 Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b}  {x :  Σ A B } →  (((proj₁ x) , proj₂ x ) ≡ x )
 Lemma-MM33 =  _≡_.refl
 
-Lemma-MM34 : { x : Carrier Mono  } -> ( (Mono ∙ ε Mono) x ≡ x  )
-Lemma-MM34  {x} = ( proj₁ ( IsMonoid.identity ( isMonoid Mono )) ) x
+Lemma-MM34 : ∀{ x : Carrier Mono  } -> ( (Mono ∙ ε Mono) x ≡ x  )
+Lemma-MM34  {x} = (( proj₁ ( IsMonoid.identity ( isMonoid Mono )) ) x )
 
-Lemma-MM35 : { x : Carrier Mono  } -> ((Mono ∙ x) (ε Mono))  ≡ x
+Lemma-MM35 : ∀{ x : Carrier Mono  } -> ((Mono ∙ x) (ε Mono))  ≡ x
 Lemma-MM35  {x} = ( proj₂  ( IsMonoid.identity ( isMonoid Mono )) ) x
 
-Lemma-MM36 : { x y z : Carrier Mono } -> ((Mono ∙ (Mono ∙ x) y) z)  ≡ (_∙_ Mono  x (_∙_ Mono y z ) )
+Lemma-MM36 : ∀{ x y z : Carrier Mono } -> ((Mono ∙ (Mono ∙ x) y) z)  ≡ (_∙_ Mono  x (_∙_ Mono y z ) )
 Lemma-MM36  {x} {y} {z} = ( IsMonoid.assoc ( isMonoid Mono ))  x y z
 
 -- We cannot prove this ...
 -- Lemma-MM38 :  ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x)  -> (( λ x -> f x)  ≡ (λ x -> g x) )
 -- Lemma-MM38 {x} {f} {g} eq  = {!!}
 
-postulate Lemma-MM39 :  ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x)  -> ( f ≡ g ) 
+-- Functional Extensionarity 
+postulate Lemma-MM39 : {x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x)  -> ( f ≡ g ) 
 
 postulate Lemma-MM40 :  ∀{x y z : Carrier Mono } {f g : Carrier Mono -> Carrier Mono -> Carrier Mono -> Carrier Mono } -> 
                (f x y z ≡ g x y z )  -> ( f ≡ g ) 
@@ -130,14 +131,14 @@
        }  
    } where
        A = Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ } 
-       Lemma-MM3 :  {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
+       Lemma-MM3 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
        Lemma-MM3 {a} = let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in
                 begin
                      TMap μ a o TMap η ( FObj T a )
                 ≈⟨⟩
                     ( λ x → ((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ))
-                ≈⟨  cong ( \f -> ( \x ->  ( ( f (proj₁ x) ) , proj₂ x ))) ( Lemma-MM9 )  ⟩
-                    ( λ x → (proj₁ x) , proj₂ x )
+                ≈⟨  cong ( \f -> ( \(x : FObj T a ) ->  ( ( f (proj₁ x) ) , proj₂ x ))) ( Lemma-MM9 )  ⟩
+                    ( λ (x : FObj T a) → (proj₁ x) , proj₂ x )
                 ≈⟨⟩
                     ( λ x → x )
                 ≈⟨⟩