--- a/monoid-monad.agda	Sun Sep 29 13:36:42 2013 +0900
+++ b/monoid-monad.agda	Sun Sep 29 14:01:07 2013 +0900
@@ -111,7 +111,7 @@
 -- Multi Arguments Functional Extensionality
 extensionality30 : {f g : Carrier M → Carrier M → Carrier M → Carrier M } → 
                (∀ x y z  → f x y z ≡ g x y z )  → ( f ≡ g ) 
-extensionality30 eq = extensionality ( \x -> extensionality ( \y -> extensionality (eq x y) ) )
+extensionality30 eq = extensionality ( λ x → extensionality ( λ y → extensionality (eq x y) ) )
 
 Lemma-MM9  : ( λ(x : Carrier M) → ( M ∙ ε M ) x )  ≡ ( λ(x : Carrier M) → x ) 
 Lemma-MM9  = extensionality Lemma-MM34
@@ -171,13 +171,13 @@
                 ∎
 
 
-F  : (m : Carrier M) -> { a b : Obj A } -> ( f : a -> b ) -> Hom A a ( FObj T b )
-F m {a} {b} f =  \(x : a ) -> ( m , ( f x) )
+F  : (m : Carrier M) → { a b : Obj A } → ( f : a → b ) → Hom A a ( FObj T b )
+F m {a} {b} f =  λ (x : a ) → ( m , ( f x) )
 
 postulate m m' : Carrier M
 postulate a b c' : Obj A 
-postulate f :  b -> c'
-postulate g :  a -> b
+postulate f :  b → c'
+postulate g :  a → b
 
 Lemma-MM12 =  Monad.join MonoidMonad (F m f) (F m' g)