--- a/list-monoid-cat.agda	Sun Sep 29 13:36:42 2013 +0900
+++ b/list-monoid-cat.agda	Sun Sep 29 14:01:07 2013 +0900
@@ -8,11 +8,11 @@
 infixr 40 _::_
 data  List  (A : Set ) : Set  where
    [] : List A
-   _::_ : A -> List A -> List A
+   _::_ : A → List A → List A
 
 
 infixl 30 _++_
-_++_ :   {A : Set } -> List A -> List A -> List A
+_++_ :   {A : Set } → List A → List A → List A
 []        ++ ys = ys
 (x :: xs) ++ ys = x :: (xs ++ ys)
 
@@ -24,37 +24,37 @@
 
 ≡-cong = Relation.Binary.PropositionalEquality.cong 
 
-isListCategory : (A : Set) -> IsCategory ListObj (\a b -> List A) _≡_  _++_  []
+isListCategory : (A : Set) → IsCategory ListObj (λ a b → List A) _≡_  _++_  []
 isListCategory  A = record  { isEquivalence =  isEquivalence1 {A}
                     ; identityL =   list-id-l
                     ; identityR =   list-id-r
                     ; o-resp-≈ =    o-resp-≈ {A}
-                    ; associative = \{a} {b} {c} {d} {x} {y} {z} -> list-assoc {A} {x} {y} {z}
+                    ; associative = λ {a} {b} {c} {d} {x} {y} {z} → list-assoc {A} {x} {y} {z}
                     }
      where
-        list-id-l : { A : Set } -> { x : List A } ->  [] ++ x ≡ x
+        list-id-l : { A : Set } → { x : List A } →  [] ++ x ≡ x
         list-id-l {_} {_} = refl
-        list-id-r : { A : Set } -> { x : List A } ->  x ++ [] ≡ x
+        list-id-r : { A : Set } → { x : List A } →  x ++ [] ≡ x
         list-id-r {_} {[]} =   refl
-        list-id-r {A} {x :: xs} =  ≡-cong ( \y -> x :: y ) ( list-id-r {A} {xs} ) 
-        list-assoc : {A : Set} -> { xs ys zs : List A } ->
+        list-id-r {A} {x :: xs} =  ≡-cong ( λ y → x :: y ) ( list-id-r {A} {xs} ) 
+        list-assoc : {A : Set} → { xs ys zs : List A } →
               ( xs ++ ( ys ++ zs ) ) ≡ ( ( xs ++ ys ) ++ zs )
         list-assoc  {_} {[]} {_} {_} = refl
-        list-assoc  {A} {x :: xs}  {ys} {zs} = ≡-cong  ( \y  -> x :: y ) 
+        list-assoc  {A} {x :: xs}  {ys} {zs} = ≡-cong  ( λ y  → x :: y ) 
                  ( list-assoc {A} {xs} {ys} {zs} )
-        o-resp-≈ :  {A : Set} ->  {f g : List A } → {h i : List A } → 
+        o-resp-≈ :  {A : Set} →  {f g : List A } → {h i : List A } → 
                           f ≡  g → h ≡  i → (h ++ f) ≡  (i ++ g)
         o-resp-≈  {A} refl refl = refl
-        isEquivalence1 : {A : Set} -> IsEquivalence {_} {_} {List A }  _≡_ 
+        isEquivalence1 : {A : Set} → IsEquivalence {_} {_} {List A }  _≡_ 
         isEquivalence1 {A} =      -- this is the same function as A's equivalence but has different types
            record { refl  = refl
              ; sym   = sym
              ; trans = trans
              } 
-ListCategory : (A : Set) -> Category _ _ _
+ListCategory : (A : Set) → Category _ _ _
 ListCategory A =
   record { Obj = ListObj
-         ; Hom = \a b -> List  A
+         ; Hom = λ a b → List  A
          ; _o_ = _++_ 
          ; _≈_ = _≡_
          ; Id  =  []
@@ -78,27 +78,27 @@
 open ≡-Monoid 
 open import Data.Product
 
-isMonoidCategory : (M :  ≡-Monoid c) -> IsCategory MonoidObj (\a b -> Carrier M ) _≡_  (_∙_  M) (ε M)
+isMonoidCategory : (M :  ≡-Monoid c) → IsCategory MonoidObj (λ a b → Carrier M ) _≡_  (_∙_  M) (ε M)
 isMonoidCategory  M = record  { isEquivalence =  isEquivalence1 {M}
-                    ; identityL =   \{_} {_} {x} -> (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x )
-                    ; identityR =   \{_} {_} {x} -> (( proj₂ ( IsMonoid.identity ( isMonoid M )) ) x )
-                    ; associative = \{a} {b} {c} {d} {x} {y} {z} -> sym ( (IsMonoid.assoc ( isMonoid M )) x y z )
+                    ; identityL =   λ {_} {_} {x} → (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x )
+                    ; identityR =   λ {_} {_} {x} → (( proj₂ ( IsMonoid.identity ( isMonoid M )) ) x )
+                    ; associative = λ {a} {b} {c} {d} {x} {y} {z} → sym ( (IsMonoid.assoc ( isMonoid M )) x y z )
                     ; o-resp-≈ =    o-resp-≈ {M}
                     }
      where
-        o-resp-≈ :  {M :  ≡-Monoid c} ->  {f g : Carrier M } → {h i : Carrier M } → 
+        o-resp-≈ :  {M :  ≡-Monoid c} →  {f g : Carrier M } → {h i : Carrier M } → 
                           f ≡  g → h ≡  i → (_∙_ M  h f) ≡  (_∙_ M i g)
         o-resp-≈  {A} refl refl = refl
-        isEquivalence1 : {M :  ≡-Monoid c} -> IsEquivalence {_} {_} {Carrier M }  _≡_ 
+        isEquivalence1 : {M :  ≡-Monoid c} → IsEquivalence {_} {_} {Carrier M }  _≡_ 
         isEquivalence1 {A} =      -- this is the same function as A's equivalence but has different types
            record { refl  = refl
              ; sym   = sym
              ; trans = trans
              } 
-MonoidCategory : (M : ≡-Monoid c) -> Category _ _ _
+MonoidCategory : (M : ≡-Monoid c) → Category _ _ _
 MonoidCategory M =
   record { Obj = MonoidObj
-         ; Hom = \a b -> Carrier M 
+         ; Hom = λ a b → Carrier M 
          ; _o_ = _∙_  M
          ; _≈_ = _≡_
          ; Id  =  ε M