--- 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