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