Mercurial > hg > Members > kono > Proof > category

changeset 300:d6a6dd305da2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
arrow and lambda fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 29 Sep 2013 14:01:07 +0900
parents 8c72f5284bc8
children 93cf0a6c21fe
files CatExponetial.agda cat-utility.agda comparison-em.agda comparison-functor-conv.agda comparison-functor.agda em-category.agda equalizer.agda kleisli.agda level-ex.agda list-level.agda list-monoid-cat.agda list-nat.agda list-nat0.agda monoid-monad.agda pullback.agda record-ex.agda universal-mapping.agda yoneda.agda
diffstat 18 files changed, 263 insertions(+), 263 deletions(-) [+]
line wrap: on
line diff
--- a/CatExponetial.agda	Sun Sep 29 13:36:42 2013 +0900
+++ b/CatExponetial.agda	Sun Sep 29 14:01:07 2013 +0900
@@ -24,7 +24,7 @@
 
 open NTrans 
 Cid : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ' ) {a : CObj A B } → CHom A B a a
-Cid {c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} A B {a} = record { TMap = \x -> id1 B (FObj a x) ; isNTrans = isNTrans1 {a} } where
+Cid {c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} A B {a} = record { TMap = λ x → id1 B (FObj a x) ; isNTrans = isNTrans1 {a} } where
    commute : {a : CObj A B } {a₁ b : Obj A} {f : Hom A a₁ b} →
         B [ B [ FMap a f o id1 B (FObj a a₁) ] ≈
         B [ id1 B (FObj a b) o FMap a f ] ]
@@ -35,8 +35,8 @@
              ≈↑⟨ idL ⟩
                  id1 B (FObj a b) o FMap a f
              ∎
-   isNTrans1 : {a : CObj A B } → IsNTrans A B a a (\x -> id1 B (FObj a x))
-   isNTrans1 {a} = record { commute = \{a₁ b f} -> commute {a} {a₁} {b} {f} }
+   isNTrans1 : {a : CObj A B } → IsNTrans A B a a (λ x → id1 B (FObj a x))
+   isNTrans1 {a} = record { commute = λ {a₁ b f} → commute {a} {a₁} {b} {f} }
 
 _+_ :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ' }  {a b c : CObj A B } 
      → CHom A B b c → CHom A B a b → CHom A B a c
@@ -71,8 +71,8 @@
 isB^A :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ' ) → IsCategory (CObj A B) (CHom A B) _==_ _+_ (Cid A B)
 isB^A  {c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} A B =
   record  { isEquivalence =  record {refl = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory B )); 
-                  sym = \{i j} → sym1 {_} {_} {i} {j} ;
-                  trans = \{i j k} → trans1 {_} {_} {i} {j} {k} }  
+                  sym = λ {i j} → sym1 {_} {_} {i} {j} ;
+                  trans = λ {i j k} → trans1 {_} {_} {i} {j} {k} }  
         ; identityL = IsCategory.identityL ( Category.isCategory B )
         ; identityR = IsCategory.identityR ( Category.isCategory B )
         ; o-resp-≈ =  λ{a b c f g h i } → o-resp-≈1      {a} {b} {c} {f} {g} {h} {i}
--- a/cat-utility.agda	Sun Sep 29 13:36:42 2013 +0900
+++ b/cat-utility.agda	Sun Sep 29 14:01:07 2013 +0900
@@ -106,9 +106,9 @@
 
 
         Functor*Nat :  {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'')
-            (F : Functor B C) -> { G H : Functor A B } -> ( n : NTrans A B G H ) -> NTrans A C (F ○  G) (F ○ H)
+            (F : Functor B C) → { G H : Functor A B } → ( n : NTrans A B G H ) → NTrans A C (F ○  G) (F ○ H)
         Functor*Nat A {B} C F {G} {H} n = record {
-               TMap  = \a -> FMap F (TMap n a)
+               TMap  = λ a → FMap F (TMap n a)
                ; isNTrans = record {
                     commute = commute
                }
@@ -127,9 +127,9 @@
                     ∎
 
         Nat*Functor :  {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'')
-            { G H : Functor B C } -> ( n : NTrans B C G H ) -> (F : Functor A B) -> NTrans A C (G ○  F) (H ○ F)
+            { G H : Functor B C } → ( n : NTrans B C G H ) → (F : Functor A B) → NTrans A C (G ○  F) (H ○ F)
         Nat*Functor A {B} C {G} {H} n F = record {
-               TMap  = \a -> TMap n (FObj F a)
+               TMap  = λ a → TMap n (FObj F a)
                ; isNTrans = record {
                     commute = commute
                }
@@ -156,9 +156,9 @@
                         : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
                    field
                       T=UF  :  T ≃  (UR ○ FR) 
-                      μ=UεF : {x : Obj A } -> A [ TMap μR x ≈ FMap UR ( TMap εR ( FObj FR x ) ) ]
-                      -- ηR=η  : {x : Obj A } -> A [ TMap ηR x  ≈  TMap η x ] -- We need T -> UR FR conversion
-                      -- μR=μ  : {x : Obj A } -> A [ TMap μR x  ≈  TMap μ x ]
+                      μ=UεF : {x : Obj A } → A [ TMap μR x ≈ FMap UR ( TMap εR ( FObj FR x ) ) ]
+                      -- ηR=η  : {x : Obj A } → A [ TMap ηR x  ≈  TMap η x ] -- We need T → UR FR conversion
+                      -- μR=μ  : {x : Obj A } → A [ TMap μR x  ≈  TMap μ x ]
 
 
         record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  {c a b : Obj A} (e : Hom A c a) (f g : Hom A a b)  : Set  (ℓ ⊔ (c₁ ⊔ c₂)) where
@@ -178,7 +178,7 @@
         --        f       |        g
         --                |f×g
         --                v
-        --    a <-------- ab ----------> b
+        --    a <-------- ab ---------→ b
         --         π1            π2
 
 
@@ -201,11 +201,11 @@
 
         -- Pullback
         --         f
-        --     a -------> c
+        --     a ------→ c
         --     ^          ^                 
         --  π1 |          |g
         --     |          |
-        --    ab -------> b
+        --    ab ------→ b
         --     ^   π2
         --     |
         --     d   
--- a/comparison-em.agda	Sun Sep 29 13:36:42 2013 +0900
+++ b/comparison-em.agda	Sun Sep 29 14:01:07 2013 +0900
@@ -47,11 +47,11 @@
 open MResolution
 open Eilenberg-Moore-Hom
 
-emkobj : Obj B -> EMObj
+emkobj : Obj B → EMObj
 emkobj b = record { 
      a = FObj U^K b ; phi = FMap U^K (TMap ε^K b) ; isAlgebra = record { identity = identity1 b; eval = eval1 b }
   } where
-      identity1 :  (b : Obj B) -> A [ A [ (FMap U^K (TMap ε^K b))  o TMap η^K (FObj U^K b) ] ≈ id1 A (FObj U^K b) ]
+      identity1 :  (b : Obj B) → A [ A [ (FMap U^K (TMap ε^K b))  o TMap η^K (FObj U^K b) ] ≈ id1 A (FObj U^K b) ]
       identity1 b =  let open ≈-Reasoning (A) in
            begin
                 (FMap U^K (TMap ε^K b))  o TMap η^K (FObj U^K b)
@@ -59,7 +59,7 @@
                 id1 A (FObj U^K b)
            ∎
 
-      eval1 :  (b : Obj B) -> A [ A [ (FMap U^K (TMap ε^K b))  o TMap μ^K' (FObj U^K b) ] ≈ A [ (FMap U^K (TMap ε^K b)) o FMap T^K (FMap U^K (TMap ε^K b)) ] ]
+      eval1 :  (b : Obj B) → A [ A [ (FMap U^K (TMap ε^K b))  o TMap μ^K' (FObj U^K b) ] ≈ A [ (FMap U^K (TMap ε^K b)) o FMap T^K (FMap U^K (TMap ε^K b)) ] ]
       eval1 b = let open ≈-Reasoning (A) in
            begin
                 (FMap U^K (TMap ε^K b)) o TMap μ^K' (FObj U^K b) 
@@ -77,10 +77,10 @@
 
 
 open EMObj
-emkmap : {a b : Obj B} (f : Hom B a b) -> EMHom (emkobj a) (emkobj b)
+emkmap : {a b : Obj B} (f : Hom B a b) → EMHom (emkobj a) (emkobj b)
 emkmap {a} {b} f = record { EMap = FMap U^K f ; homomorphism = homomorphism1 a b f
   } where
-      homomorphism1 : (a b : Obj B) (f : Hom B a b) -> A [ A [ (φ (emkobj b))  o FMap T^K (FMap U^K f) ]  ≈ A [ (FMap U^K f) o (φ (emkobj a)) ] ]
+      homomorphism1 : (a b : Obj B) (f : Hom B a b) → A [ A [ (φ (emkobj b))  o FMap T^K (FMap U^K f) ]  ≈ A [ (FMap U^K f) o (φ (emkobj a)) ] ]
       homomorphism1 a b f = let open ≈-Reasoning (A) in
            begin
                 (φ (emkobj b))  o FMap T^K (FMap U^K f)
@@ -118,7 +118,7 @@
            ≈⟨⟩
               EMap (EM-id {emkobj a})
            ∎
-         ≈-cong : {a b : Obj B} -> {f g : Hom B a b} → B [ f ≈ g ] →  emkmap f ≗ emkmap g 
+         ≈-cong : {a b : Obj B} → {f g : Hom B a b} → B [ f ≈ g ] →  emkmap f ≗ emkmap g 
          ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (A) in
            begin
                EMap (emkmap f)
@@ -133,7 +133,7 @@
               EMap (emkmap g ∙ emkmap f)
            ∎
 
-Lemma-EM20 : { a b : Obj B} { f : Hom B a b } -> A [ FMap U^T ( FMap K^T f)  ≈ FMap U^K f ]
+Lemma-EM20 : { a b : Obj B} { f : Hom B a b } → A [ FMap U^T ( FMap K^T f)  ≈ FMap U^K f ]
 Lemma-EM20 {a} {b} {f}  =  let open ≈-Reasoning (A) in 
            begin
                FMap U^T ( FMap K^T f) 
@@ -141,9 +141,9 @@
                FMap U^K f 
            ∎
 
--- Lemma-EM21 : { a : Obj B}  -> FObj U^T ( FObj K^T a)  = FObj U^K a 
+-- Lemma-EM21 : { a : Obj B}  → FObj U^T ( FObj K^T a)  = FObj U^K a 
 
-Lemma-EM22 : { a b : Obj A} { f : Hom A a b } ->  A [ EMap ( FMap K^T ( FMap F^K f) ) ≈ EMap ( FMap F^T f  ) ]
+Lemma-EM22 : { a b : Obj A} { f : Hom A a b } →  A [ EMap ( FMap K^T ( FMap F^K f) ) ≈ EMap ( FMap F^T f  ) ]
 Lemma-EM22  {a} {b} {f} =  let open ≈-Reasoning (A) in 
            begin
                 EMap ( FMap K^T ( FMap F^K f) )
@@ -154,12 +154,12 @@
            ∎
  
 
--- Lemma-EM23 : { a b : Obj A}  ->  ( FObj K^T ( FObj F^K f) ) = ( FObj F^T f  ) 
+-- Lemma-EM23 : { a b : Obj A}  →  ( FObj K^T ( FObj F^K f) ) = ( FObj F^T f  ) 
 
--- Lemma-EM24 :  {a : Obj A } {b : Obj B} -> A [ TMap η^K (FObj U^K b) ≈ TMap η^K a ]
+-- Lemma-EM24 :  {a : Obj A } {b : Obj B} → A [ TMap η^K (FObj U^K b) ≈ TMap η^K a ]
 -- Lemma-EM24 = ?
 
-Lemma-EM26 : {b : Obj B} -> A [ EMap (TMap ε^T ( FObj K^T b)) ≈ FMap U^K ( TMap ε^K b) ]
+Lemma-EM26 : {b : Obj B} → A [ EMap (TMap ε^T ( FObj K^T b)) ≈ FMap U^K ( TMap ε^K b) ]
 Lemma-EM26  {b} =  let open ≈-Reasoning (A) in 
            begin
                  EMap (TMap ε^T ( FObj K^T b))
--- a/comparison-functor-conv.agda	Sun Sep 29 13:36:42 2013 +0900
+++ b/comparison-functor-conv.agda	Sun Sep 29 14:01:07 2013 +0900
@@ -55,29 +55,29 @@
 
 open KleisliHom
 
-RHom  = \(a b : Obj A) -> KleisliHom {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } a b
-TtoK : (a b : Obj A) -> (KHom a b) ->  {g h : Hom A  (FObj T b) (FObj ( U_K ○ F_K) b) } ->
-      ([ A ] g ~ h) -> Hom A a (FObj ( U_K ○ F_K ) b)  
+RHom  = λ (a b : Obj A) → KleisliHom {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } a b
+TtoK : (a b : Obj A) → (KHom a b) →  {g h : Hom A  (FObj T b) (FObj ( U_K ○ F_K) b) } →
+      ([ A ] g ~ h) → Hom A a (FObj ( U_K ○ F_K ) b)  
 TtoK  _ _ f {g} (Category.Cat.refl _) = A [ g o (KMap f) ]
-TKMap : {a b : Obj A} -> (f : KHom a b) -> Hom A a (FObj ( U_K ○ F_K ) b) 
+TKMap : {a b : Obj A} → (f : KHom a b) → Hom A a (FObj ( U_K ○ F_K ) b) 
 TKMap  {a} {b} f = TtoK a b f {_} {_} ((hoge (T=UF RK)) (id1 A b)) 
 
-KtoT : (a b : Obj A) -> (RHom a b) -> {g h : Hom A  (FObj ( U_K ○ F_K ) b) (FObj  T b) } ->
-      ([ A ] g ~ h) -> Hom A a (FObj T b)  
+KtoT : (a b : Obj A) → (RHom a b) → {g h : Hom A  (FObj ( U_K ○ F_K ) b) (FObj  T b) } →
+      ([ A ] g ~ h) → Hom A a (FObj T b)  
 KtoT  _ _ f {g} {h} (Category.Cat.refl eq) = A [ g o (KMap f) ]
-KTMap : {a b : Obj A} -> (f : RHom a b) -> Hom A a (FObj T b) 
+KTMap : {a b : Obj A} → (f : RHom a b) → Hom A a (FObj T b) 
 KTMap {a} {b} f = KtoT a b f {_} {_}  (( ≃-sym (T=UF RK)) (id1 A b))
 
-TKMap-cong : {a b : Obj A} {f g : KHom a b} -> A [ KMap f ≈ KMap g ] -> A [ TKMap f ≈ TKMap g ]
+TKMap-cong : {a b : Obj A} {f g : KHom a b} → A [ KMap f ≈ KMap g ] → A [ TKMap f ≈ TKMap g ]
 TKMap-cong {a} {b} {f} {g} eq = helper a b f g eq ((hoge (T=UF RK))( id1 A b  )) 
   where 
         open ≈-Reasoning (A)
-        helper : (a b : Obj A) (f g : KHom a b) -> A [ KMap f ≈ KMap g ] ->
-                 {conv : Hom A  (FObj T b) (FObj ( U_K ○ F_K ) b) } -> ([ A ] conv ~ conv) -> A [ TKMap f ≈ TKMap g ]
+        helper : (a b : Obj A) (f g : KHom a b) → A [ KMap f ≈ KMap g ] →
+                 {conv : Hom A  (FObj T b) (FObj ( U_K ○ F_K ) b) } → ([ A ] conv ~ conv) → A [ TKMap f ≈ TKMap g ]
         helper _ _ _ _ eq (Category.Cat.refl _) = 
             (Category.IsCategory.o-resp-≈ (Category.isCategory A)) eq refl-hom
 
-kfmap : {a b : Obj A} (f : KHom a b) -> Hom B (FObj F_K a) (FObj F_K b)
+kfmap : {a b : Obj A} (f : KHom a b) → Hom B (FObj F_K a) (FObj F_K b)
 kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (TKMap f) ]
 
 open Adjunction
@@ -102,7 +102,7 @@
            ≈⟨ IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩
               id1 B (FObj F_K a)
            ∎
-         ≈-cong : {a b : Obj A} -> {f g : KHom a b} → A [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ]
+         ≈-cong : {a b : Obj A} → {f g : KHom a b} → A [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ]
          ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in
            begin
                kfmap f
--- a/comparison-functor.agda	Sun Sep 29 13:36:42 2013 +0900
+++ b/comparison-functor.agda	Sun Sep 29 14:01:07 2013 +0900
@@ -48,7 +48,7 @@
 open Adjunction
 open MResolution
 
-kfmap : {a b : Obj A} (f : KHom a b) -> Hom B (FObj F_K a) (FObj F_K b)
+kfmap : {a b : Obj A} (f : KHom a b) → Hom B (FObj F_K a) (FObj F_K b)
 kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (KMap f) ]
 
 K_T : Functor KleisliCategory B 
@@ -72,7 +72,7 @@
            ≈⟨ IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩
               id1 B (FObj F_K a)
            ∎
-         ≈-cong : {a b : Obj A} -> {f g : KHom a b} → A [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ]
+         ≈-cong : {a b : Obj A} → {f g : KHom a b} → A [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ]
          ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in
            begin
                kfmap f
@@ -133,7 +133,7 @@
               kfmap g o kfmap f
            ∎
 
-Lemma-K1 : {a b : Obj A} ( f : Hom A a b ) -> B [ FMap K_T ( FMap F_T f)  ≈ FMap F_K f ]
+Lemma-K1 : {a b : Obj A} ( f : Hom A a b ) → B [ FMap K_T ( FMap F_T f)  ≈ FMap F_K f ]
 Lemma-K1 {a} {b} f = let open ≈-Reasoning (B) in
            begin
              FMap K_T ( FMap F_T f)  
@@ -151,7 +151,7 @@
              FMap F_K f 
            ∎
 
-Lemma-K2 : {a b : Obj A} ( f : KHom a b ) -> A [ FMap U_K ( FMap K_T f)  ≈ FMap U_T f ]
+Lemma-K2 : {a b : Obj A} ( f : KHom a b ) → A [ FMap U_K ( FMap K_T f)  ≈ FMap U_T f ]
 Lemma-K2 {a} {b} f = let open ≈-Reasoning (A) in
            begin
               FMap U_K ( FMap K_T f)
@@ -165,7 +165,7 @@
               FMap U_T f
            ∎
 
-Lemma-K3 : (b : Obj A)  -> B [ FMap K_T (record { KMap = (TMap η_K b) }) ≈ id1 B (FObj F_K b) ]
+Lemma-K3 : (b : Obj A)  → B [ FMap K_T (record { KMap = (TMap η_K b) }) ≈ id1 B (FObj F_K b) ]
 Lemma-K3 b = let open ≈-Reasoning (B) in
            begin
                  FMap K_T  (record { KMap = (TMap η_K b) })
@@ -175,7 +175,7 @@
                  id1 B (FObj F_K b)
            ∎
 
-Lemma-K4 : (b c : Obj A) (g : Hom A b (FObj T_K c)) -> 
+Lemma-K4 : (b c : Obj A) (g : Hom A b (FObj T_K c)) → 
      B [ FMap K_T ( record { KMap = A [ (TMap η_K (FObj T_K c)) o g ] })  ≈ FMap F_K g ]
 Lemma-K4 b c g = let open ≈-Reasoning (B) in
            begin
@@ -192,9 +192,9 @@
                 FMap F_K g 
            ∎
 
--- Lemma-K5 : (a : Obj A) -> FObj U_K ( FObj K_T a ) = U_T a
+-- Lemma-K5 : (a : Obj A) → FObj U_K ( FObj K_T a ) = U_T a
 
-Lemma-K6 : (b c : Obj A) (g : KHom b c) -> A [ FMap U_K ( FMap K_T g )  ≈ FMap U_T g ]
+Lemma-K6 : (b c : Obj A) (g : KHom b c) → A [ FMap U_K ( FMap K_T g )  ≈ FMap U_T g ]
 Lemma-K6 b c g =  let open ≈-Reasoning (A) in
            begin
                  FMap U_K ( FMap K_T g )
--- a/em-category.agda	Sun Sep 29 13:36:42 2013 +0900
+++ b/em-category.agda	Sun Sep 29 14:01:07 2013 +0900
@@ -54,11 +54,11 @@
        homomorphism : A [ A [ (φ b)  o FMap T EMap ]  ≈ A [ EMap  o (φ a) ] ]
 open Eilenberg-Moore-Hom
 
-EMHom : (a : EMObj ) (b : EMObj ) -> Set (c₁ ⊔ c₂ ⊔ ℓ)
-EMHom = \a b -> Eilenberg-Moore-Hom a b
+EMHom : (a : EMObj ) (b : EMObj ) → Set (c₁ ⊔ c₂ ⊔ ℓ)
+EMHom = λ a b → Eilenberg-Moore-Hom a b
 
 Lemma-EM1 : {x : Obj A} {φ : Hom A (FObj T x) x} (a : EMObj )
-               -> A [ A [ φ  o FMap T (id1 A x) ]  ≈ A [ (id1 A x) o φ ] ]
+               → A [ A [ φ  o FMap T (id1 A x) ]  ≈ A [ (id1 A x) o φ ] ]
 Lemma-EM1 {x} {φ} a = let open ≈-Reasoning (A) in
    begin
        φ o FMap T (id1 A x)
@@ -70,7 +70,7 @@
        (id1 A x)  o φ
    ∎
 
-EM-id : { a : EMObj } -> EMHom a a
+EM-id : { a : EMObj } → EMHom a a
 EM-id {a} = record { EMap = id1 A (obj a);
      homomorphism = Lemma-EM1 {obj a} {phi a} a } 
 
@@ -81,7 +81,7 @@
             (c : EMObj ) 
             (g : EMHom b c)
             (f : EMHom a b)
-                 -> A [ A [ φ c  o FMap T (A [ (EMap g)  o  (EMap f) ] ) ]  
+                 → A [ A [ φ c  o FMap T (A [ (EMap g)  o  (EMap f) ] ) ]  
                       ≈ A [ (A [ (EMap g)  o  (EMap f) ])  o φ a ] ]
 Lemma-EM2 a b c g f = let 
       open ≈-Reasoning (A) in
@@ -101,23 +101,23 @@
         ( (EMap g)  o  (EMap f) )  o φ a
    ∎
 
-_∙_ :  {a b c : EMObj } -> EMHom b c -> EMHom a b -> EMHom a c
+_∙_ :  {a b c : EMObj } → EMHom b c → EMHom a b → EMHom a c
 _∙_ {a} {b} {c} g f = record { EMap = A [ EMap g  o EMap f ] ; homomorphism = Lemma-EM2 a b c g f } 
 
-_≗_ : {a : EMObj } {b : EMObj } (f g : EMHom a b ) -> Set ℓ 
+_≗_ : {a : EMObj } {b : EMObj } (f g : EMHom a b ) → Set ℓ 
 _≗_ f g = A [ EMap f ≈ EMap g ]
 
 --
 -- cannot use as identityL = EMidL
 --
-EMidL : {C D : EMObj} -> {f : EMHom C D} → (EM-id  ∙ f) ≗ f
+EMidL : {C D : EMObj} → {f : EMHom C D} → (EM-id  ∙ f) ≗ f
 EMidL {C} {D} {f} = let open ≈-Reasoning (A) in idL {obj D} 
-EMidR : {C D : EMObj} -> {f : EMHom C D} → (f ∙ EM-id)  ≗ f
+EMidR : {C D : EMObj} → {f : EMHom C D} → (f ∙ EM-id)  ≗ f
 EMidR {C} {_} {_} = let open ≈-Reasoning (A) in  idR {obj C}
-EMo-resp :  {a b c : EMObj} -> {f g : EMHom a b } → {h i : EMHom  b c } → 
+EMo-resp :  {a b c : EMObj} → {f g : EMHom a b } → {h i : EMHom  b c } → 
                           f ≗ g → h ≗ i → (h ∙ f) ≗ (i ∙ g)
 EMo-resp {a} {b} {c} {f} {g} {h} {i} = ( IsCategory.o-resp-≈ (Category.isCategory A) )
-EMassoc :   {a b c d : EMObj} -> {f : EMHom c d } → {g : EMHom b c } → {h : EMHom a b } →
+EMassoc :   {a b c d : EMObj} → {f : EMHom c d } → {g : EMHom b c } → {h : EMHom a b } →
                           (f ∙ (g ∙ h)) ≗ ((f ∙ g) ∙ h)
 EMassoc {_} {_} {_} {_} {f} {g} {h} =   ( IsCategory.associative (Category.isCategory A) )
 
@@ -130,7 +130,7 @@
                     }
      where
          open ≈-Reasoning (A) 
-         isEquivalence : {a : EMObj } {b : EMObj } ->
+         isEquivalence : {a : EMObj } {b : EMObj } →
                IsEquivalence {_} {_} {EMHom a b } _≗_
          isEquivalence {C} {D} =      -- this is the same function as A's equivalence but has different types
            record { refl  = refl-hom
@@ -155,17 +155,17 @@
 
 U^T : Functor Eilenberg-MooreCategory A
 U^T = record {
-            FObj = \a -> obj a
-          ; FMap = \f -> EMap f
+            FObj = λ a → obj a
+          ; FMap = λ f → EMap f
         ; isFunctor = record
-        {      ≈-cong   = \eq -> eq
+        {      ≈-cong   = λ eq → eq
              ; identity = refl-hom
              ; distr    = refl-hom
         }
      } where open ≈-Reasoning (A) 
 
 open Monad
-Lemma-EM4 : (x : Obj A ) -> A [ A [ TMap μ x  o TMap η (FObj T x) ] ≈ id1 A (FObj T x) ]
+Lemma-EM4 : (x : Obj A ) → A [ A [ TMap μ x  o TMap η (FObj T x) ] ≈ id1 A (FObj T x) ]
 Lemma-EM4 x = let  open ≈-Reasoning (A) in
     begin
        TMap μ x  o TMap η (FObj T x) 
@@ -173,7 +173,7 @@
        id1 A (FObj T x)
     ∎
 
-Lemma-EM5 : (x : Obj A ) -> A [ A [ ( TMap μ x)  o TMap μ (FObj T x) ] ≈ A [ ( TMap μ x) o FMap T ( TMap μ x) ] ]
+Lemma-EM5 : (x : Obj A ) → A [ A [ ( TMap μ x)  o TMap μ (FObj T x) ] ≈ A [ ( TMap μ x) o FMap T ( TMap μ x) ] ]
 Lemma-EM5 x =  let  open ≈-Reasoning (A) in
     begin
        ( TMap μ x)  o TMap μ (FObj T x) 
@@ -181,14 +181,14 @@
        ( TMap μ x) o FMap T ( TMap μ x)
     ∎
 
-ftobj : Obj A -> EMObj
-ftobj = \x -> record { a = FObj T x ; phi = TMap μ x; 
+ftobj : Obj A → EMObj
+ftobj = λ x → record { a = FObj T x ; phi = TMap μ x; 
  isAlgebra = record {
       identity = Lemma-EM4 x;
       eval     = Lemma-EM5 x
  } }
 
-Lemma-EM6 :  (a b : Obj A ) -> (f : Hom A a b ) ->
+Lemma-EM6 :  (a b : Obj A ) → (f : Hom A a b ) →
       A [ A [ (φ (ftobj b))  o FMap T (FMap T f) ]  ≈ A [ FMap T f  o (φ (ftobj a)) ] ]
 Lemma-EM6 a b f =  let  open ≈-Reasoning (A) in
     begin
@@ -201,7 +201,7 @@
        FMap T f  o (φ (ftobj a))
     ∎
 
-ftmap : {a b : Obj A} -> (Hom A a b) -> EMHom (ftobj a) (ftobj b)
+ftmap : {a b : Obj A} → (Hom A a b) → EMHom (ftobj a) (ftobj b)
 ftmap {a} {b} f = record { EMap = FMap T f; homomorphism =  Lemma-EM6 a b f }
 
 F^T : Functor A Eilenberg-MooreCategory
@@ -223,7 +223,7 @@
 
 -- T = (U^T ○ F^T)    
 
-Lemma-EM7 :  ∀{a b : Obj A} -> (f : Hom A a b ) -> A [ FMap T f  ≈ FMap (U^T ○ F^T) f ]
+Lemma-EM7 :  ∀{a b : Obj A} → (f : Hom A a b ) → A [ FMap T f  ≈ FMap (U^T ○ F^T) f ]
 Lemma-EM7 {a} {b} f = let open ≈-Reasoning (A) in
      sym ( begin
           FMap (U^T ○ F^T) f
@@ -237,7 +237,7 @@
 Lemma-EM8 f = Category.Cat.refl (Lemma-EM7 f)
 
 η^T : NTrans A A identityFunctor ( U^T ○ F^T ) 
-η^T = record { TMap = \x -> TMap η x ; isNTrans = isNTrans1 } where
+η^T = record { TMap = λ x → TMap η x ; isNTrans = isNTrans1 } where
        commute1 :  {a b : Obj A} {f : Hom A a b}
             → A [ A [ ( FMap ( U^T ○ F^T ) f ) o  ( TMap η a ) ]  ≈ A [ (TMap η b ) o  f  ] ]
        commute1 {a} {b} {f} =  let open ≈-Reasoning (A) in
@@ -248,10 +248,10 @@
           ≈⟨ nat η ⟩
               TMap η b o f
           ∎
-       isNTrans1 : IsNTrans A A identityFunctor ( U^T ○ F^T ) (\a -> TMap η a)
+       isNTrans1 : IsNTrans A A identityFunctor ( U^T ○ F^T ) (λ a → TMap η a)
        isNTrans1 = record { commute = commute1 }
 
-Lemma-EM9 : (a : EMObj) -> A [ A [ (φ a)  o FMap T (φ a) ]  ≈ A [ (φ a)  o (φ (FObj ( F^T ○ U^T ) a)) ] ]
+Lemma-EM9 : (a : EMObj) → A [ A [ (φ a)  o FMap T (φ a) ]  ≈ A [ (φ a)  o (φ (FObj ( F^T ○ U^T ) a)) ] ]
 Lemma-EM9 a = let open ≈-Reasoning (A) in
           sym ( begin
               (φ a)  o (φ (FObj ( F^T ○ U^T ) a))
@@ -261,11 +261,11 @@
               (φ a)  o FMap T (φ a)
           ∎ )
 
-emap-ε : (a : EMObj ) -> EMHom (FObj ( F^T ○ U^T ) a)  a
+emap-ε : (a : EMObj ) → EMHom (FObj ( F^T ○ U^T ) a)  a
 emap-ε a = record { EMap = φ a ; homomorphism = Lemma-EM9 a }
 
 ε^T : NTrans Eilenberg-MooreCategory Eilenberg-MooreCategory  ( F^T ○ U^T ) identityFunctor
-ε^T = record { TMap = \a -> emap-ε a; isNTrans = isNTrans1 } where
+ε^T = record { TMap = λ a → emap-ε a; isNTrans = isNTrans1 } where
        commute1 : {a b : EMObj } {f : EMHom a b}
             →  (f ∙ ( emap-ε a ) ) ≗ (( emap-ε b ) ∙(  FMap (F^T ○ U^T) f ) )
        commute1 {a} {b} {f} =  let open ≈-Reasoning (A) in
@@ -278,14 +278,14 @@
           ≈⟨⟩
              EMap (f ∙ ( emap-ε a ))
           ∎  )
-       isNTrans1 : IsNTrans  Eilenberg-MooreCategory Eilenberg-MooreCategory ( F^T ○ U^T ) identityFunctor (\a -> emap-ε a )
-       isNTrans1 = record { commute = \{a} {b} {f} ->  (IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A)) )  (homomorphism f ) }  -- naturity1 {a} {b} {f}
+       isNTrans1 : IsNTrans  Eilenberg-MooreCategory Eilenberg-MooreCategory ( F^T ○ U^T ) identityFunctor (λ a → emap-ε a )
+       isNTrans1 = record { commute = λ {a} {b} {f} →  (IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A)) )  (homomorphism f ) }  -- naturity1 {a} {b} {f}
                                                                                  
 --
 -- μ = U^T ε U^F
 --
 
-emap-μ :  (a : Obj A) -> Hom A (FObj ( U^T ○ F^T ) (FObj ( U^T ○ F^T ) a)) (FObj ( U^T ○ F^T ) a)
+emap-μ :  (a : Obj A) → Hom A (FObj ( U^T ○ F^T ) (FObj ( U^T ○ F^T ) a)) (FObj ( U^T ○ F^T ) a)
 emap-μ a = FMap U^T ( TMap ε^T ( FObj F^T a ))
 
 μ^T : NTrans A A (( U^T ○ F^T ) ○ ( U^T ○ F^T )) ( U^T ○ F^T )
@@ -307,7 +307,7 @@
         isNTrans1 : IsNTrans A A (( U^T ○ F^T ) ○ ( U^T ○ F^T )) ( U^T ○ F^T ) emap-μ
         isNTrans1 = record { commute = commute1 }
 
-Lemma-EM10 : {x : Obj A } -> A [ TMap μ^T x ≈ FMap U^T ( TMap ε^T ( FObj F^T x ) ) ]
+Lemma-EM10 : {x : Obj A } → A [ TMap μ^T x ≈ FMap U^T ( TMap ε^T ( FObj F^T x ) ) ]
 Lemma-EM10 {x} = let open ≈-Reasoning (A) in
           sym ( begin
               FMap U^T ( TMap ε^T ( FObj F^T x ) )
@@ -317,7 +317,7 @@
               TMap μ^T x
           ∎ )
 
-Lemma-EM11 : {x : Obj A } -> A [ TMap μ x ≈ FMap U^T ( TMap ε^T ( FObj F^T x ) ) ]
+Lemma-EM11 : {x : Obj A } → A [ TMap μ x ≈ FMap U^T ( TMap ε^T ( FObj F^T x ) ) ]
 Lemma-EM11 {x} = let open ≈-Reasoning (A) in
           sym ( begin
               FMap U^T ( TMap ε^T ( FObj F^T x ) )
@@ -328,7 +328,7 @@
 Adj^T : Adjunction A Eilenberg-MooreCategory U^T F^T η^T ε^T
 Adj^T = record {
            isAdjunction = record {
-               adjoint1 = \{b} -> IsAlgebra.identity (isAlgebra b) ; -- adjoint1
+               adjoint1 = λ {b} → IsAlgebra.identity (isAlgebra b) ; -- adjoint1
                adjoint2 = adjoint2
            }
        } where
--- a/equalizer.agda	Sun Sep 29 13:36:42 2013 +0900
+++ b/equalizer.agda	Sun Sep 29 14:01:07 2013 +0900
@@ -3,8 +3,8 @@
 --  Equalizer
 --
 --         e             f
---    c  --------> a ----------> b
---    ^        .     ---------->
+--    c  -------→ a ---------→ b
+--    ^        .     ---------→
 --    |      .            g
 --    |k   .
 --    |  . h
@@ -88,7 +88,7 @@
 --     e i = e j → i = j
 --
 --           e eqa f g        f
---         c ----------> a ------->b
+--         c ---------→ a ------→b
 --        ^^
 --        ||
 --       i||j
@@ -120,7 +120,7 @@
 --   Isomorphic arrows from c' to c makes another equalizer
 --
 --           e eqa f g        f
---         c ----------> a ------->b
+--         c ---------→ a ------→b
 --        |^
 --        ||
 --    h   || h-1
@@ -189,7 +189,7 @@
 --
 --
 --           e eqa f g        f
---         c ---------->a ------->b
+--         c ---------→a ------→b
 --         ^            ^     g
 --         |            |
 --         |k = id c'   |
@@ -260,7 +260,7 @@
  } where
      --
      --           e eqa f g        f
-     --         c ----------> a ------->b
+     --         c ---------→ a ------→b
      --         ^                  g
      --         |
      --         |k₁  = e eqa (f o (e (eqa f g))) (g o (e (eqa f g))))
--- a/kleisli.agda	Sun Sep 29 13:36:42 2013 +0900
+++ b/kleisli.agda	Sun Sep 29 14:01:07 2013 +0900
@@ -31,14 +31,14 @@
 open Functor
 Lemma1 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} (T : Functor A A) →  {a b c : Obj A} {g : Hom A b c} { f : Hom A a b }
      → A [ ( FMap T (A [ g o f ] ))  ≈ (A [ FMap T g o FMap T f ]) ]
-Lemma1 = \t → IsFunctor.distr ( isFunctor t )
+Lemma1 = λ t → IsFunctor.distr ( isFunctor t )
 
 
 open NTrans
 Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A} 
       → (μ : NTrans A A F G) → {a b : Obj A} { f : Hom A a b }
       → A [ A [  FMap G f o TMap μ a ]  ≈ A [ TMap μ b o  FMap F f ] ]
-Lemma2 = \n → IsNTrans.commute ( isNTrans  n  )
+Lemma2 = λ n → IsNTrans.commute ( isNTrans  n  )
 
 -- Laws of Monad
 --
@@ -57,12 +57,12 @@
                  { a : Obj A } →
                  ( M : Monad A T η μ )
     → A [ A [  TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
-Lemma3 = \m → IsMonad.assoc ( isMonad m )
+Lemma3 = λ m → IsMonad.assoc ( isMonad m )
 
 
 Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b}
     → A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ]
-Lemma4 = \a → IsCategory.identityL ( Category.isCategory a )
+Lemma4 = λ a → IsCategory.identityL ( Category.isCategory a )
 
 Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                  { T : Functor A A }
@@ -71,7 +71,7 @@
                  { a : Obj A } →
                  ( M : Monad A T η μ )
     →  A [ A [ TMap μ a o TMap η ( FObj T a )  ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-Lemma5 = \m → IsMonad.unity1 ( isMonad m )
+Lemma5 = λ m → IsMonad.unity1 ( isMonad m )
 
 Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                  { T : Functor A A }
@@ -80,7 +80,7 @@
                  { a : Obj A } →
                  ( M : Monad A T η μ )
     →  A [ A [ TMap μ a o (FMap T (TMap η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-Lemma6 = \m → IsMonad.unity2 ( isMonad m )
+Lemma6 = λ m → IsMonad.unity2 ( isMonad m )
 
 -- Laws of Kleisli Category
 --
@@ -190,7 +190,7 @@
 --
 --  o-resp in Kleisli Category ( for Functor definitions )
 --
-Lemma10 :  {a b c : Obj A} -> (f g : Hom A a (FObj T b) ) → (h i : Hom A b (FObj T c) ) → 
+Lemma10 :  {a b c : Obj A} → (f g : Hom A a (FObj T b) ) → (h i : Hom A b (FObj T c) ) → 
                           A [ f ≈ g ] → A [ h ≈ i ] → A [ (join M h f) ≈ (join M i g) ]
 Lemma10 {a} {b} {c} f g h i eq-fg eq-hi = let open ≈-Reasoning (A) in
    begin 
@@ -214,14 +214,14 @@
        KMap :  Hom A a ( FObj T b )
 
 open KleisliHom 
-KHom  = \(a b : Obj A) -> KleisliHom {c₁} {c₂} {ℓ} {A} {T} a b
+KHom  = λ (a b : Obj A) → KleisliHom {c₁} {c₂} {ℓ} {A} {T} a b
 
 K-id :  {a : Obj A} → KHom a a
 K-id {a = a} = record { KMap =  TMap η a } 
 
 open import Relation.Binary.Core
 
-_⋍_ : { a : Obj A } { b : Obj A } (f g  : KHom a b ) -> Set ℓ 
+_⋍_ : { a : Obj A } { b : Obj A } (f g  : KHom a b ) → Set ℓ 
 _⋍_ {a} {b} f g = A [ KMap f ≈ KMap g ]
 
 _*_ : { a b c : Obj A } → ( KHom b c) → (  KHom a b) → KHom a c 
@@ -236,21 +236,21 @@
                     }
      where
          open ≈-Reasoning (A) 
-         isEquivalence :  { a b : Obj A } ->
+         isEquivalence :  { a b : Obj A } →
                IsEquivalence {_} {_} {KHom a b} _⋍_
          isEquivalence {C} {D} =      -- this is the same function as A's equivalence but has different types
            record { refl  = refl-hom
              ; sym   = sym
              ; trans = trans-hom
              } 
-         KidL : {C D : Obj A} -> {f : KHom C D} → (K-id * f) ⋍ f
+         KidL : {C D : Obj A} → {f : KHom C D} → (K-id * f) ⋍ f
          KidL {_} {_} {f} =  Lemma7 (KMap f) 
-         KidR : {C D : Obj A} -> {f : KHom C D} → (f * K-id) ⋍ f
+         KidR : {C D : Obj A} → {f : KHom C D} → (f * K-id) ⋍ f
          KidR {_} {_} {f} =  Lemma8 (KMap f) 
-         Ko-resp :  {a b c : Obj A} -> {f g : KHom a b } → {h i : KHom  b c } → 
+         Ko-resp :  {a b c : Obj A} → {f g : KHom a b } → {h i : KHom  b c } → 
                           f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g)
          Ko-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = Lemma10 {a} {b} {c} (KMap f) (KMap g) (KMap h) (KMap i) eq-fg eq-hi
-         Kassoc :   {a b c d : Obj A} -> {f : KHom c d } → {g : KHom b c } → {h : KHom a b } →
+         Kassoc :   {a b c d : Obj A} → {f : KHom c d } → {g : KHom b c } → {h : KHom a b } →
                           (f * (g * h)) ⋍ ((f * g) * h)
          Kassoc {_} {_} {_} {_} {f} {g} {h} =  Lemma9 (KMap f) (KMap g) (KMap h) 
 
@@ -271,7 +271,7 @@
 --      nat-η
 --
 
-ufmap : {a b : Obj A} (f : KHom a b ) -> Hom A (FObj T a) (FObj T b)
+ufmap : {a b : Obj A} (f : KHom a b ) → Hom A (FObj T a) (FObj T b)
 ufmap {a} {b} f =  A [ TMap μ (b)  o FMap T (KMap f) ]
 
 U_T : Functor KleisliCategory A
@@ -329,12 +329,12 @@
           ∎
 
 
-ffmap :  {a b : Obj A} (f : Hom A a b) -> KHom a b
+ffmap :  {a b : Obj A} (f : Hom A a b) → KHom a b
 ffmap f = record { KMap = A [ TMap η (Category.cod A f) o f ] }
 
 F_T : Functor A KleisliCategory
 F_T = record {
-        FObj = \a -> a
+        FObj = λ a → a
         ; FMap = ffmap
         ; isFunctor = record
         { ≈-cong   = ≈-cong
@@ -390,7 +390,7 @@
 -- T = (U_T ○ F_T) 
 --
 
-Lemma11-1 :  ∀{a b : Obj A} -> (f : Hom A a b ) -> A [ FMap T f  ≈ FMap (U_T ○ F_T) f ]
+Lemma11-1 :  ∀{a b : Obj A} → (f : Hom A a b ) → A [ FMap T f  ≈ FMap (U_T ○ F_T) f ]
 Lemma11-1 {a} {b} f = let open ≈-Reasoning (A) in
      sym ( begin
           FMap (U_T ○ F_T) f
@@ -420,7 +420,7 @@
 --
 
 nat-η : NTrans A A identityFunctor ( U_T ○ F_T ) 
-nat-η = record { TMap = \x -> TMap η x ; isNTrans = isNTrans1 } where
+nat-η = record { TMap = λ x → TMap η x ; isNTrans = isNTrans1 } where
        commute1 :  {a b : Obj A} {f : Hom A a b}
             → A [ A [ (  FMap ( U_T ○ F_T ) f ) o  ( TMap η a ) ]  ≈ A [ (TMap η b ) o  f  ] ]
        commute1 {a} {b} {f} =  let open ≈-Reasoning (A) in
@@ -431,14 +431,14 @@
           ≈⟨ nat η ⟩
               TMap η b o f
           ∎ 
-       isNTrans1 : IsNTrans A A identityFunctor ( U_T ○ F_T ) (\a -> TMap η a)
+       isNTrans1 : IsNTrans A A identityFunctor ( U_T ○ F_T ) (λ a → TMap η a)
        isNTrans1 = record { commute = commute1 } 
 
-tmap-ε : (a : Obj A) -> KHom (FObj T a) a
+tmap-ε : (a : Obj A) → KHom (FObj T a) a
 tmap-ε a = record { KMap = id1 A (FObj T a) }
 
 nat-ε : NTrans KleisliCategory KleisliCategory  ( F_T ○ U_T ) identityFunctor
-nat-ε = record { TMap = \a -> tmap-ε a; isNTrans = isNTrans1 } where
+nat-ε = record { TMap = λ a → tmap-ε a; isNTrans = isNTrans1 } where
        commute1 : {a b : Obj A} {f : KHom a b}
             →  (f * ( tmap-ε a ) ) ⋍   (( tmap-ε b ) * (  FMap (F_T ○ U_T) f ) )
        commute1 {a} {b} {f} =  let open ≈-Reasoning (A) in
@@ -471,13 +471,13 @@
           ≈⟨⟩
               KMap (f * ( tmap-ε a ))
           ∎ )
-       isNTrans1 : IsNTrans  KleisliCategory KleisliCategory ( F_T ○ U_T ) identityFunctor (\a -> tmap-ε a )
+       isNTrans1 : IsNTrans  KleisliCategory KleisliCategory ( F_T ○ U_T ) identityFunctor (λ a → tmap-ε a )
        isNTrans1 = record { commute = commute1 } 
 
 --
 -- μ = U_T ε U_F
 --
-tmap-μ :  (a : Obj A) -> Hom A (FObj ( U_T ○ F_T ) (FObj ( U_T ○ F_T ) a)) (FObj ( U_T ○ F_T ) a)
+tmap-μ :  (a : Obj A) → Hom A (FObj ( U_T ○ F_T ) (FObj ( U_T ○ F_T ) a)) (FObj ( U_T ○ F_T ) a)
 tmap-μ a = FMap U_T ( TMap nat-ε ( FObj F_T a ))
 
 nat-μ : NTrans A A (( U_T ○ F_T ) ○ ( U_T ○ F_T )) ( U_T ○ F_T )
@@ -501,7 +501,7 @@
         isNTrans1 : IsNTrans A A (( U_T ○ F_T ) ○ ( U_T ○ F_T )) ( U_T ○ F_T ) tmap-μ
         isNTrans1 = record { commute = commute1 } 
 
-Lemma12 : {x : Obj A } -> A [ TMap nat-μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ]
+Lemma12 : {x : Obj A } → A [ TMap nat-μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ]
 Lemma12 {x} = let open ≈-Reasoning (A) in
           sym ( begin
               FMap U_T ( TMap nat-ε ( FObj F_T x ) )
@@ -511,7 +511,7 @@
               TMap nat-μ x
           ∎ )
 
-Lemma13 : {x : Obj A } -> A [ TMap μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ]
+Lemma13 : {x : Obj A } → A [ TMap μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ]
 Lemma13 {x} = let open ≈-Reasoning (A) in
           sym ( begin
               FMap U_T ( TMap nat-ε ( FObj F_T x ) )
--- a/level-ex.agda	Sun Sep 29 13:36:42 2013 +0900
+++ b/level-ex.agda	Sun Sep 29 14:01:07 2013 +0900
@@ -8,11 +8,11 @@
 
 postulate a : A
 
-lemma1 : Set  ℓ -> A
-lemma1  = \x -> a
+lemma1 : Set  ℓ → A
+lemma1  = λ x → a
 
-lemma2 : A -> Set  ℓ
-lemma2 = \x -> A
+lemma2 : A → Set  ℓ
+lemma2 = λ x → A
 
 lemma3 : Set  (suc ℓ)
-lemma3 = A -> Set  ℓ
+lemma3 = A → Set  ℓ
--- a/list-level.agda	Sun Sep 29 13:36:42 2013 +0900
+++ b/list-level.agda	Sun Sep 29 14:01:07 2013 +0900
@@ -15,11 +15,11 @@
 infixr 40 _::_
 data  List {a} (A : Set a) : Set a where
    [] : List A
-   _::_ : A -> List A -> List A
+   _::_ : A → List A → List A
 
 
 infixl 30 _++_
-_++_ : ∀ {a} {A : Set a} -> List A -> List A -> List A
+_++_ : ∀ {a} {A : Set a} → List A → List A → List A
 []        ++ ys = ys
 (x :: xs) ++ ys = x :: (xs ++ ys)
 
@@ -34,10 +34,10 @@
 L3 = L1 ++ L2
 
 data Node {a} ( A : Set a ) : Set a where
-   leaf  : A -> Node A
-   node  : Node A -> Node A -> Node A
+   leaf  : A → Node A
+   node  : Node A → Node A → Node A
 
-flatten : ∀{n} { A : Set n } -> Node A -> List A
+flatten : ∀{n} { A : Set n } → Node A → List A
 flatten ( leaf a )   = a :: []
 flatten ( node a b ) = flatten a ++ flatten b
 
@@ -47,31 +47,31 @@
 
 infixr 20  _==_
 
-data _==_ {n} {A : Set n} :  List A -> List A -> Set n where
-      reflection  : {x : List A} -> x == x
+data _==_ {n} {A : Set n} :  List A → List A → Set n where
+      reflection  : {x : List A} → x == x
 
-cong1 : ∀{a} {A : Set a } {b} { B : Set b } ->
-   ( f : List A -> List B ) -> {x : List A } -> {y : List A} -> x == y -> f x == f y
+cong1 : ∀{a} {A : Set a } {b} { B : Set b } →
+   ( f : List A → List B ) → {x : List A } → {y : List A} → x == y → f x == f y
 cong1 f reflection = reflection
 
-eq-cons :  ∀{n} {A : Set n} {x y : List A} ( a : A ) -> x ==  y -> ( a :: x ) == ( a :: y )
-eq-cons a z = cong1 ( \x -> ( a :: x) ) z
+eq-cons :  ∀{n} {A : Set n} {x y : List A} ( a : A ) → x ==  y → ( a :: x ) == ( a :: y )
+eq-cons a z = cong1 ( λ x → ( a :: x) ) z
 
-trans-list :  ∀{n} {A : Set n} {x y z : List A}  -> x ==  y -> y == z -> x == z
+trans-list :  ∀{n} {A : Set n} {x y z : List A}  → x ==  y → y == z → x == z
 trans-list reflection reflection = reflection
 
 
-==-to-≡ :  ∀{n} {A : Set n}  {x y : List A}  -> x ==  y -> x ≡ y
+==-to-≡ :  ∀{n} {A : Set n}  {x y : List A}  → x ==  y → x ≡ y
 ==-to-≡ reflection = refl
 
-list-id-l : { A : Set } -> { x : List A} ->  [] ++ x == x
+list-id-l : { A : Set } → { x : List A} →  [] ++ x == x
 list-id-l = reflection
 
-list-id-r : { A : Set } -> ( x : List A ) ->  x ++ [] == x
+list-id-r : { A : Set } → ( x : List A ) →  x ++ [] == x
 list-id-r [] =   reflection
 list-id-r (x :: xs) =  eq-cons x ( list-id-r xs )
 
-list-assoc : {A : Set } -> ( xs ys zs : List A ) ->
+list-assoc : {A : Set } → ( xs ys zs : List A ) →
      ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) )
 list-assoc  [] ys zs = reflection
 list-assoc  (x :: xs)  ys zs = eq-cons x ( list-assoc xs ys zs )
@@ -103,11 +103,11 @@
   _∎ : (x : List A ) → x IsRelatedTo x
   _∎ _ = relTo reflection
 
-lemma11 : ∀{n} (A : Set n) ( x : List A ) -> x == x
+lemma11 : ∀{n} (A : Set n) ( x : List A ) → x == x
 lemma11 A x =  let open ==-Reasoning A in
      begin x ∎
       
-++-assoc : ∀{n} (L : Set n) ( xs ys zs : List L ) -> (xs ++ ys) ++ zs  == xs ++ (ys ++ zs)
+++-assoc : ∀{n} (L : Set n) ( xs ys zs : List L ) → (xs ++ ys) ++ zs  == xs ++ (ys ++ zs)
 ++-assoc A [] ys zs = let open ==-Reasoning A in
   begin -- to prove ([] ++ ys) ++ zs  == [] ++ (ys ++ zs)
    ( [] ++ ys ) ++ zs
@@ -139,27 +139,27 @@
 
 --postulate Obj : Set
 
---postulate Hom : Obj -> Obj -> Set
+--postulate Hom : Obj → Obj → Set
 
 
---postulate  id : { a : Obj } -> Hom a a
+--postulate  id : { a : Obj } → Hom a a
 
 
 --infixr 80 _○_
---postulate  _○_ : { a b c  : Obj } -> Hom b c -> Hom a b -> Hom a c
+--postulate  _○_ : { a b c  : Obj } → Hom b c → Hom a b → Hom a c
 
--- postulate  axId1 : {a  b : Obj} -> ( f : Hom a b ) -> f == id ○ f
--- postulate  axId2 : {a  b : Obj} -> ( f : Hom a b ) -> f == f ○ id
+-- postulate  axId1 : {a  b : Obj} → ( f : Hom a b ) → f == id ○ f
+-- postulate  axId2 : {a  b : Obj} → ( f : Hom a b ) → f == f ○ id
 
---assoc : { a b c d : Obj } ->
---    (f : Hom c d ) -> (g : Hom b c) -> (h : Hom a b) ->
+--assoc : { a b c d : Obj } →
+--    (f : Hom c d ) → (g : Hom b c) → (h : Hom a b) →
 --    (f ○ g) ○ h == f ○ ( g ○ h)
 
 
 --a = Set
 
--- ListObj : {A : Set} -> List A
+-- ListObj : {A : Set} → List A
 -- ListObj =  List Set
 
--- ListHom : ListObj -> ListObj -> Set
+-- ListHom : ListObj → ListObj → Set
 
--- 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
--- a/list-nat.agda	Sun Sep 29 13:36:42 2013 +0900
+++ b/list-nat.agda	Sun Sep 29 14:01:07 2013 +0900
@@ -13,11 +13,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)
 
@@ -27,10 +27,10 @@
 l3 = l1 ++ l2
 
 data Node  ( A : Set  ) : Set  where
-   leaf  : A -> Node A
-   node  : Node A -> Node A -> Node A
+   leaf  : A → Node A
+   node  : Node A → Node A → Node A
 
-flatten :  { A : Set } -> Node A -> List A
+flatten :  { A : Set } → Node A → List A
 flatten ( leaf a )   = a :: []
 flatten ( node a b ) = flatten a ++ flatten b
 
@@ -40,31 +40,31 @@
 
 infixr 20  _==_
 
-data _==_  {A : Set } :  List A -> List A -> Set  where
-      reflection  : {x : List A} -> x == x
+data _==_  {A : Set } :  List A → List A → Set  where
+      reflection  : {x : List A} → x == x
 
-cong1 :  {A : Set  }  { B : Set  } ->
-   ( f : List A -> List B ) -> {x : List A } -> {y : List A} -> x == y -> f x == f y
+cong1 :  {A : Set  }  { B : Set  } →
+   ( f : List A → List B ) → {x : List A } → {y : List A} → x == y → f x == f y
 cong1 f reflection = reflection
 
-eq-cons :   {A : Set } {x y : List A} ( a : A ) -> x ==  y -> ( a :: x ) == ( a :: y )
-eq-cons a z = cong1 ( \x -> ( a :: x) ) z
+eq-cons :   {A : Set } {x y : List A} ( a : A ) → x ==  y → ( a :: x ) == ( a :: y )
+eq-cons a z = cong1 ( λ x → ( a :: x) ) z
 
-trans-list :   {A : Set } {x y z : List A}  -> x ==  y -> y == z -> x == z
+trans-list :   {A : Set } {x y z : List A}  → x ==  y → y == z → x == z
 trans-list reflection reflection = reflection
 
 
-==-to-≡ :   {A : Set }  {x y : List A}  -> x ==  y -> x ≡ y
+==-to-≡ :   {A : Set }  {x y : List A}  → x ==  y → x ≡ y
 ==-to-≡ reflection = refl
 
-list-id-l : { A : Set } -> { x : List A} ->  [] ++ x == x
+list-id-l : { A : Set } → { x : List A} →  [] ++ x == x
 list-id-l = reflection
 
-list-id-r : { A : Set } -> ( x : List A ) ->  x ++ [] == x
+list-id-r : { A : Set } → ( x : List A ) →  x ++ [] == x
 list-id-r [] =   reflection
 list-id-r (x :: xs) =  eq-cons x ( list-id-r xs )
 
-list-assoc : {A : Set } -> ( xs ys zs : List A ) ->
+list-assoc : {A : Set } → ( xs ys zs : List A ) →
      ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) )
 list-assoc  [] ys zs = reflection
 list-assoc  (x :: xs)  ys zs = eq-cons x ( list-assoc xs ys zs )
@@ -96,11 +96,11 @@
   _∎ : (x : List A ) → x IsRelatedTo x
   _∎ _ = relTo reflection
 
-lemma11 :  (A : Set ) ( x : List A ) -> x == x
+lemma11 :  (A : Set ) ( x : List A ) → x == x
 lemma11 A x =  let open ==-Reasoning A in
      begin x ∎
       
-++-assoc :  (L : Set ) ( xs ys zs : List L ) -> (xs ++ ys) ++ zs  == xs ++ (ys ++ zs)
+++-assoc :  (L : Set ) ( xs ys zs : List L ) → (xs ++ ys) ++ zs  == xs ++ (ys ++ zs)
 ++-assoc A [] ys zs = let open ==-Reasoning A in
   begin -- to prove ([] ++ ys) ++ zs  == [] ++ (ys ++ zs)
    ( [] ++ ys ) ++ zs
@@ -132,27 +132,27 @@
 
 --postulate Obj : Set
 
---postulate Hom : Obj -> Obj -> Set
+--postulate Hom : Obj → Obj → Set
 
 
---postulate  id : { a : Obj } -> Hom a a
+--postulate  id : { a : Obj } → Hom a a
 
 
 --infixr 80 _○_
---postulate  _○_ : { a b c  : Obj } -> Hom b c -> Hom a b -> Hom a c
+--postulate  _○_ : { a b c  : Obj } → Hom b c → Hom a b → Hom a c
 
--- postulate  axId1 : {a  b : Obj} -> ( f : Hom a b ) -> f == id ○ f
--- postulate  axId2 : {a  b : Obj} -> ( f : Hom a b ) -> f == f ○ id
+-- postulate  axId1 : {a  b : Obj} → ( f : Hom a b ) → f == id ○ f
+-- postulate  axId2 : {a  b : Obj} → ( f : Hom a b ) → f == f ○ id
 
---assoc : { a b c d : Obj } ->
---    (f : Hom c d ) -> (g : Hom b c) -> (h : Hom a b) ->
+--assoc : { a b c d : Obj } →
+--    (f : Hom c d ) → (g : Hom b c) → (h : Hom a b) →
 --    (f ○ g) ○ h == f ○ ( g ○ h)
 
 
 --a = Set
 
--- ListObj : {A : Set} -> List A
+-- ListObj : {A : Set} → List A
 -- ListObj =  List Set
 
--- ListHom : ListObj -> ListObj -> Set
+-- ListHom : ListObj → ListObj → Set
 
--- a/list-nat0.agda	Sun Sep 29 13:36:42 2013 +0900
+++ b/list-nat0.agda	Sun Sep 29 14:01:07 2013 +0900
@@ -9,14 +9,14 @@
 
 
 infixr 40 _::_
-data  List ∀ {a} (A : Set a) : Set a where
+data  List {a} (A : Set a) : Set a where
    [] : List A
-   _::_ : A -> List A -> List A
+   _::_ : A → List A → List A
 
 
 infixl 30 _++_
--- _++_ : {a : Level } -> {A : Set a} -> List A -> List A -> List A
-_++_ : ∀ {a} {A : Set a} -> List A -> List A -> List A
+-- _++_ : {a : Level } → {A : Set a} → List A → List A → List A
+_++_ : ∀ {a} {A : Set a} → List A → List A → List A
 []        ++ ys = ys
 (x :: xs) ++ ys = x :: (xs ++ ys)
 
@@ -28,24 +28,24 @@
 
 infixr 20  _==_
 
-data _==_ {n} {A : Set n} :  List A -> List A -> Set n where
-      reflection  : {x : List A} -> x == x
-      eq-cons : {x y : List A} { a : A } -> x ==  y -> ( a :: x ) == ( a :: y )
-      trans-list : {x y z : List A} { a : A } -> x ==  y -> y == z -> x == z
+data _==_ {n} {A : Set n} :  List A → List A → Set n where
+      reflection  : {x : List A} → x == x
+      eq-cons : {x y : List A} { a : A } → x ==  y → ( a :: x ) == ( a :: y )
+      trans-list : {x y z : List A} { a : A } → x ==  y → y == z → x == z
 --      eq-nil  : [] == []
 
-list-id-l : { A : Set } -> { x : List A} ->  [] ++ x == x
+list-id-l : { A : Set } → { x : List A} →  [] ++ x == x
 list-id-l = reflection
 
-list-id-r : { A : Set } -> ( x : List A ) ->  x ++ [] == x
+list-id-r : { A : Set } → ( x : List A ) →  x ++ [] == x
 list-id-r [] =   reflection
 list-id-r (x :: xs) =  eq-cons ( list-id-r xs )
 
 
--- listAssoc : { A : Set } -> { a b c : List A} ->  ( ( a ++ b ) ++ c ) == ( a ++ ( b ++ c ) )
+-- listAssoc : { A : Set } → { a b c : List A} →  ( ( a ++ b ) ++ c ) == ( a ++ ( b ++ c ) )
 -- listAssoc   = eq-reflection
 
-list-assoc : {A : Set } -> ( xs ys zs : List A ) ->
+list-assoc : {A : Set } → ( xs ys zs : List A ) →
      ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) )
 list-assoc  [] ys zs = reflection
 list-assoc  (x :: xs)  ys zs = eq-cons ( list-assoc xs ys zs )
@@ -55,19 +55,19 @@
 open  import  Relation.Binary.PropositionalEquality
 open ≡-Reasoning
 
-cong1 : ∀{a} {A : Set a } {b} { B : Set b } ->
-   ( f : A -> B ) -> {x : A } -> {y : A} -> x ≡ y -> f x ≡ f y
+cong1 : ∀{a} {A : Set a } {b} { B : Set b } →
+   ( f : A → B ) → {x : A } → {y : A} → x ≡ y → f x ≡ f y
 cong1 f refl = refl
 
-lemma11 :  ∀{n} ->  ( Set n ) IsRelatedTo ( Set n )
+lemma11 :  ∀{n} →  ( Set n ) IsRelatedTo ( Set n )
 lemma11  = relTo refl
 
-lemma12 : {L : Set}  ( x : List L ) -> x ++ x ≡ x ++ x
+lemma12 : {L : Set}  ( x : List L ) → x ++ x ≡ x ++ x
 lemma12 x =  begin  x ++ x  ∎
 
 
-++-assoc : {L : Set} ( xs ys zs : List L ) -> (xs ++ ys) ++ zs  ≡ xs ++ (ys ++ zs)
-++-assoc [] ys zs = -- {A : Set} ->  -- let open ==-Reasoning A in
+++-assoc : {L : Set} ( xs ys zs : List L ) → (xs ++ ys) ++ zs  ≡ xs ++ (ys ++ zs)
+++-assoc [] ys zs = -- {A : Set} →  -- let open ==-Reasoning A in
   begin -- to prove ([] ++ ys) ++ zs  ≡ [] ++ (ys ++ zs)
    ( [] ++ ys ) ++ zs
   ≡⟨ refl ⟩
@@ -76,7 +76,7 @@
     [] ++ ( ys ++ zs )
   ∎
   
-++-assoc (x :: xs) ys zs = -- {A : Set} -> -- let open  ==-Reasoning A in
+++-assoc (x :: xs) ys zs = -- {A : Set} → -- let open  ==-Reasoning A in
   begin -- to prove ((x :: xs) ++ ys) ++ zs ≡ (x :: xs) ++ (ys ++ zs)
     ((x :: xs) ++ ys) ++ zs
   ≡⟨ refl ⟩
@@ -100,27 +100,27 @@
 
 --postulate Obj : Set
 
---postulate Hom : Obj -> Obj -> Set
+--postulate Hom : Obj → Obj → Set
 
 
---postulate  id : { a : Obj } -> Hom a a
+--postulate  id : { a : Obj } → Hom a a
 
 
 --infixr 80 _○_
---postulate  _○_ : { a b c  : Obj } -> Hom b c -> Hom a b -> Hom a c
+--postulate  _○_ : { a b c  : Obj } → Hom b c → Hom a b → Hom a c
 
--- postulate  axId1 : {a  b : Obj} -> ( f : Hom a b ) -> f == id ○ f
--- postulate  axId2 : {a  b : Obj} -> ( f : Hom a b ) -> f == f ○ id
+-- postulate  axId1 : {a  b : Obj} → ( f : Hom a b ) → f == id ○ f
+-- postulate  axId2 : {a  b : Obj} → ( f : Hom a b ) → f == f ○ id
 
---assoc : { a b c d : Obj } ->
---    (f : Hom c d ) -> (g : Hom b c) -> (h : Hom a b) ->
+--assoc : { a b c d : Obj } →
+--    (f : Hom c d ) → (g : Hom b c) → (h : Hom a b) →
 --    (f ○ g) ○ h == f ○ ( g ○ h)
 
 
 --a = Set
 
--- ListObj : {A : Set} -> List A
+-- ListObj : {A : Set} → List A
 -- ListObj =  List Set
 
--- ListHom : ListObj -> ListObj -> Set
+-- ListHom : ListObj → ListObj → Set
 
--- 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)
 
--- a/pullback.agda	Sun Sep 29 13:36:42 2013 +0900
+++ b/pullback.agda	Sun Sep 29 14:01:07 2013 +0900
@@ -14,11 +14,11 @@
 --
 -- Pullback from equalizer and product
 --         f
---     a -------> c
+--     a ------→ c
 --     ^          ^
 --  π1 |          |g
 --     |          |
---    ab -------> b
+--    ab ------→ b
 --     ^   π2
 --     |
 --     | e = equalizer (f π1) (g π1)
@@ -345,14 +345,14 @@
 --      
 --        ai 
 --        ^                                       K f = id lim
---        | pi                          lim = K i ------------> K j = lim
+--        | pi                          lim = K i -----------→ K j = lim
 --        |                                     |               |
 --        p                                     |               |
 --        ^                                 ε i |               | ε j
 --        |                                     |               |
 --        | e = equalizer (id p) (id p)         |               |
 --        |                                     v               v
---       lim <------------------ d'     a i = Γ i ------------> Γ j = a j
+--       lim <------------------ d'     a i = Γ i -----------→ Γ j = a j
 --         k ( product pi )                          Γ f
 --                                              Γ f o ε i = ε j 
 --
--- a/record-ex.agda	Sun Sep 29 13:36:42 2013 +0900
+++ b/record-ex.agda	Sun Sep 29 14:01:07 2013 +0900
@@ -1,8 +1,8 @@
 module record-ex where
 
 data _∨_  (A B : Set) : Set where
-      or1 : A -> A ∨ B
-      or2 : B -> A ∨ B
+      or1 : A → A ∨ B
+      or2 : B → A ∨ B
 
 postulate A B C : Set
 postulate a1 a2 a3 : A
@@ -13,7 +13,7 @@
 y : ( A ∨ B )
 y = or2 b1
 
-f : ( A ∨ B ) -> A
+f : ( A ∨ B ) → A
 f (or1 a) = a
 f (or2 b) = a1
 
@@ -39,7 +39,7 @@
 
 data Nat : Set where
    zero : Nat
-   suc  : Nat -> Nat
+   suc  : Nat → Nat
 
 record Mod3 (m : Nat) : Set where
    field
@@ -49,6 +49,6 @@
 
 open Mod3 
 
-Lemma1 :  ( x : Mod3 ( suc (suc (suc (suc zero))))) ( y : Mod3 ( suc zero ) ) -> n x  ≡ n y 
+Lemma1 :  ( x : Mod3 ( suc (suc (suc (suc zero))))) ( y : Mod3 ( suc zero ) ) → n x  ≡ n y 
 Lemma1 x y =  mod3 y
 
--- a/universal-mapping.agda	Sun Sep 29 13:36:42 2013 +0900
+++ b/universal-mapping.agda	Sun Sep 29 14:01:07 2013 +0900
@@ -342,11 +342,11 @@
 --     naturality of left (Φ)
 --     k = Hom A b b' ; f' = k o f                        h Hom A a' a  ; f' = f o h
 --                        left                                               left
---    f : Hom A F(a)   b --------> f* : Hom B a U(b)      f' : Hom A F(a')b -------> f'* : Hom B a' U(b)
+--    f : Hom A F(a)   b -------→ f* : Hom B a U(b)      f' : Hom A F(a')b ------→ f'* : Hom B a' U(b)
 --       |                               |                     |                               |
 --       |k*                             |U(k*)                |F(h*)                          |h*
 --       v                               v                     v                               v
---    f': Hom A F(a)   b'-------> f'* : Hom B a U(b')     f: Hom A F(a)  b ---------> f* : Hom B a U(b)
+--    f': Hom A F(a)   b'------→ f'* : Hom B a U(b')     f: Hom A F(a)  b --------→ f* : Hom B a U(b)
 --                        left                                               left
 
 record UnityOfOppsite  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
@@ -359,17 +359,17 @@
                right-injective : {a : Obj A} { b : Obj B } → {f : Hom A a (FObj U b) }  → A [ left ( right f ) ≈ f ]
                left-injective  : {a : Obj A} { b : Obj B } → {f : Hom B (FObj F a) b }  → B [ right ( left f ) ≈ f ]
                ---  naturality of Φ
-               left-commute1 : {a : Obj A} {b b' : Obj B } ->
-                       { f : Hom B (FObj F a) b }  -> { k : Hom B b b' } ->
+               left-commute1 : {a : Obj A} {b b' : Obj B } →
+                       { f : Hom B (FObj F a) b }  → { k : Hom B b b' } →
                         A [  left ( B [ k o  f ] )  ≈ A [ FMap U k o left f  ] ]
-               left-commute2 : {a a' : Obj A} {b : Obj B } ->
-                       { f : Hom B (FObj F a) b }  -> { h : Hom A a' a } ->
+               left-commute2 : {a a' : Obj A} {b : Obj B } →
+                       { f : Hom B (FObj F a) b }  → { h : Hom A a' a } →
                         A [ left ( B [ f  o  FMap F h ] )  ≈  A [ left f o h ] ]
                r-cong : {a : Obj A} { b : Obj B } → { f g : Hom A a ( FObj U b ) } →  A [ f  ≈ g ] → B [ right f ≈ right g ]
                l-cong : {a : Obj A} { b : Obj B } → { f g : Hom B (FObj F a) b }   →  B [ f  ≈ g ] → A [ left f ≈ left g   ]
            --  naturality of right (Φ-1)
-           right-commute1 : {a : Obj A} {b b' : Obj B } ->
-                       { g : Hom A a (FObj U b)}  -> { k : Hom B b b' } ->
+           right-commute1 : {a : Obj A} {b b' : Obj B } →
+                       { g : Hom A a (FObj U b)}  → { k : Hom B b b' } →
                         B [ B [ k o  right g ]   ≈ right ( A [ FMap U k o g  ] ) ]
            right-commute1 {a} {b} {b'} {g} {k} =  let open ≈-Reasoning (B) in
                      begin
@@ -381,8 +381,8 @@
                      ≈⟨ r-cong (lemma-1 g k) ⟩
                          right ( A [ FMap U k o g  ] )
                      ∎ where
-                             lemma-1 : {a : Obj A} {b b' : Obj B } ->
-                               ( g : Hom A a (FObj U b))  -> ( k : Hom B b b' ) ->
+                             lemma-1 : {a : Obj A} {b b' : Obj B } →
+                               ( g : Hom A a (FObj U b))  → ( k : Hom B b b' ) →
                                 A [ A [ FMap U k o left ( right g ) ]   ≈  A [ FMap U k o g  ] ]
                              lemma-1 g k = let open ≈-Reasoning (A) in
                                    begin
@@ -390,8 +390,8 @@
                                    ≈⟨ cdr ( right-injective) ⟩
                                         FMap U k o g
                                    ∎
-           right-commute2 : {a a' : Obj A} {b : Obj B } ->
-                       { g : Hom A a (FObj U b) }  -> { h : Hom A a' a } ->
+           right-commute2 : {a a' : Obj A} {b : Obj B } →
+                       { g : Hom A a (FObj U b) }  → { h : Hom A a' a } →
                         B [ B [ right g  o  FMap F h ]   ≈  right ( A [ g o h ] ) ]
            right-commute2 {a} {a'} {b} {g} {h} =  let open ≈-Reasoning (B) in
                      begin
@@ -403,8 +403,8 @@
                      ≈⟨ r-cong ( lemma-2 g h  ) ⟩
                           right ( A [ g o h ] )
                      ∎  where
-                           lemma-2 :  {a a' : Obj A} {b : Obj B } ->
-                               ( g : Hom A a (FObj U b))  -> ( h : Hom A a' a ) ->
+                           lemma-2 :  {a a' : Obj A} {b : Obj B } →
+                               ( g : Hom A a (FObj U b))  → ( h : Hom A a' a ) →
                                 A [ A [  left ( right g ) o h ]   ≈  A [ g o h  ] ]
                            lemma-2 g h  = let open ≈-Reasoning (A) in car ( right-injective  )
 
@@ -462,8 +462,8 @@
                      ≈⟨ idR  ⟩
                         f
                      ∎
-            left-commute1 : {a : Obj A} {b b' : Obj B } ->
-                       { f : Hom B (FObj F a) b }  -> { k : Hom B b b' } ->
+            left-commute1 : {a : Obj A} {b b' : Obj B } →
+                       { f : Hom B (FObj F a) b }  → { k : Hom B b b' } →
                         A [  left ( B [ k o  f ] )  ≈ A [ FMap U k o left f  ] ]
             left-commute1 {a} {b} {b'} {f} {k} = let open ≈-Reasoning (A) in
                      begin
@@ -477,8 +477,8 @@
                      ≈⟨⟩
                          FMap U k o left f  
                      ∎
-            left-commute2 : {a a' : Obj A} {b : Obj B } ->
-                       { f : Hom B (FObj F a) b }  -> { h : Hom A a' a}  ->
+            left-commute2 : {a a' : Obj A} {b : Obj B } →
+                       { f : Hom B (FObj F a) b }  → { h : Hom A a' a}  →
                         A [ left ( B [ f  o  FMap F h ] )  ≈  A [ left f o h ] ]
             left-commute2 {a'} {a} {b} {f} {h} = let open ≈-Reasoning (A) in
                      begin
@@ -505,10 +505,10 @@
 
 open UnityOfOppsite
 
---   f                            : a -----------> U(b)
---   1_F(a)                       :F(a) ---------> F(a)
---   ε(b) = right uo (1_F(a))     :UF(b)---------> a
---   η(a) = left  uo (1_U(a))     : a -----------> FU(a)
+--   f                            : a ----------→ U(b)
+--   1_F(a)                       :F(a) --------→ F(a)
+--   ε(b) = right uo (1_F(a))     :UF(b)--------→ a
+--   η(a) = left  uo (1_U(a))     : a ----------→ FU(a)
 
 
 uo-η-map  : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
@@ -526,8 +526,8 @@
 uo-solution  : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                  ( U : Functor B A )
                  ( F : Functor A B ) →
-                 ( uo : UnityOfOppsite A B U F)  →  {a : Obj A} {b : Obj B } ->
-                       ( f : Hom A a (FObj U b )) -> Hom B (FObj F a) b
+                 ( uo : UnityOfOppsite A B U F)  →  {a : Obj A} {b : Obj B } →
+                       ( f : Hom A a (FObj U b )) → Hom B (FObj F a) b
 uo-solution A B U F uo {a} {b} f =  --  B  [ right uo (id1 A (FObj U b)) o FMap F f ]
                                      right uo f
 
--- a/yoneda.agda	Sun Sep 29 13:36:42 2013 +0900
+++ b/yoneda.agda	Sun Sep 29 14:01:07 2013 +0900
@@ -30,8 +30,8 @@
 
 open NTrans 
 Yid : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : YObj A } → YHom A a a
-Yid {_} {c₂} A {a} = record { TMap = \a -> \x -> x ; isNTrans = isNTrans1 {a} } where
-   isNTrans1 : {a : YObj A } → IsNTrans (Category.op A) (Sets {c₂}) a a (\a -> \x -> x )
+Yid {_} {c₂} A {a} = record { TMap = λ a → λ x → x ; isNTrans = isNTrans1 {a} } where
+   isNTrans1 : {a : YObj A } → IsNTrans (Category.op A) (Sets {c₂}) a a (λ a → λ x → x )
    isNTrans1 {a} = record { commute = refl  }
 
 _+_ : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b c : YObj A} → YHom A b c → YHom A a b → YHom A a c
@@ -63,7 +63,7 @@
 
 isSetsAop :   { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → IsCategory (YObj A) (YHom A) _==_ _+_ ( Yid A )
 isSetsAop {_} {c₂} {_} A =  
-  record  { isEquivalence =  record {refl = refl ; trans = \{i j k} → trans1 {_} {_} {i} {j} {k} ; sym = \{i j} → sym1  {_} {_} {i} {j}}
+  record  { isEquivalence =  record {refl = refl ; trans = λ {i j k} → trans1 {_} {_} {i} {j} {k} ; sym = λ {i j} → sym1  {_} {_} {i} {j}}
         ; identityL = refl
         ; identityR = refl
         ; o-resp-≈ =  λ{a b c f g h i } → o-resp-≈      {a} {b} {c} {f} {g} {h} {i}
@@ -122,7 +122,7 @@
         FObj = λ b → Hom (Category.op A) a b  ;
         FMap =   λ {b c : Obj A } → λ ( f : Hom  A c b ) → λ (g : Hom  A b a ) →  (Category.op A) [ f o g ] ;
         isFunctor = record {
-             identity =  \{b} → extensionality {_} {_} {_} {A} ( λ x → lemma-y-obj1 {b} x ) ;
+             identity =  λ {b} → extensionality {_} {_} {_} {A} ( λ x → lemma-y-obj1 {b} x ) ;
              distr = λ {a} {b} {c} {f} {g} → extensionality {_} {_} {_} {A} ( λ x → lemma-y-obj2 a b c f g x ) ;
              ≈-cong = λ eq → extensionality {_} {_} {_} {A} ( λ x →  lemma-y-obj3 x eq ) 
         } 
@@ -216,7 +216,7 @@
 --
 --  F : A → Sets  ∈ Obj SetsAop
 --
---  F(a) -> Nat(h_a,F)
+--  F(a) → Nat(h_a,F)
 --      x ∈ F(a) , (g : Hom A b a)  → ( FMap F g ) x
 ------