--- a/em-category.agda	Wed Jul 31 15:26:25 2013 +0900
+++ b/em-category.agda	Wed Jul 31 15:42:38 2013 +0900
@@ -32,6 +32,10 @@
 open Functor
 open NTrans
 record IsEMAlgebra (a : Obj A) (φ : Hom A (FObj T a) a ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
+   obj : Obj A
+   obj = a
+   phi : Hom A (FObj T a) a
+   phi = φ
    field
        identity : A [ A [ φ  o TMap η a ] ≈ id1 A a ]
        eval     : A [ A [ φ  o TMap μ a ] ≈ A [ φ o FMap T φ ] ]
@@ -42,37 +46,37 @@
      isEMAlbgebra : IsEMAlgebra a φ 
 open EMAlgebra
      
-data EMObj {a : Obj A}  {φ  : Hom A (FObj T a) a }  : Set ( c₁ ⊔ c₂ ) where
-            emObj : \a φ -> (IsEMAlgebra a φ) -> EMObj {a} {φ}
+data EMObj {a : Obj A}  {φ  : Hom A (FObj T a) a }  : Set (suc ( c₁ ⊔ c₂  ⊔ ℓ)) where
+            emObj : (IsEMAlgebra a φ) -> EMObj {a} {φ}
 
 emobj : EMObj -> Obj A
-emobj (emObj x φ isAlgebra) = x
+emobj (emObj isAlgebra) = obj isAlgebra
 
-record IsEMHom { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } 
-              {x y : Obj A} {φ  : FObj T x -> x } {φ'  : FObj T y -> y }
-              (a : EMObj {c₁} {c₂} {ℓ} {A} {T} x φ  ) 
-              (b : EMObj {c₁} {c₂} {ℓ} {A} {T} y φ' ) 
-              (α : Hom A a b) : Set c₂ where
+record IsEMHom {x y : Obj A} {φ  : Hom A (FObj T x) x } {φ'  : Hom A (FObj T y) y }
+              (a : EMObj {x} {φ}  ) 
+              (b : EMObj {y} {φ'} ) 
+              (α : Hom A x y) : Set ℓ where
    field
        homomorphism : A [ A [ φ'  o FMap T α ]  ≈ A [ α  o φ ] ]
 open IsEMHom
 
-record EMHom { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } 
-              {x y : Obj A }
-              (a : EMObj {c₁} {c₂} {ℓ} {A} {T} x) 
-              (b : EMObj {c₁} {c₂} {ℓ} {A} {T} y) 
-              {α : Hom A a b} : Set c₂ where
+record EMHom {x y : Obj A }
+              (a : EMObj {x}) 
+              (b : EMObj {y}) 
+              {α : Hom A x y} : Set (c₂  ⊔ ℓ) where
    field
        EMap :  Hom A x y
-       isEMHom : IsEMHom {c₁} {c₂} {ℓ} {A} {T} a b α
+       isEMHom : IsEMHom a b α
 open EMHom
 
-Lemma-EM1 : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A }
-              {x : Obj A}
-              {φ : FObj T x -> x }
-              (a : EMObj {c₁} {c₂} {ℓ} {A} {T} x φ)
+Lemma-EM1 : {x : Obj A}
+              {φ : Hom A (FObj T x) x}
+              (a : EMObj {x} {φ})
                -> A [ A [ φ  o FMap T (id1 A x) ]  ≈ A [ (id1 A x) o φ ] ]
-Lemma-EM1 (emObj x φ isAlgebra ) = let open ≈-Reasoning (A) in
+Lemma-EM1 (emObj isAlgebra ) = let 
+         x = obj isAlgebra
+         φ = phi isAlgebra
+         open ≈-Reasoning (A) in
    begin
        φ o FMap T (id1 A x)
    ≈⟨ cdr ( IsFunctor.identity (isFunctor T) ) ⟩
@@ -89,15 +93,17 @@
 
 open import Relation.Binary.Core
 
-Lemma-EM2 : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A }
-              (a b : EMObj)
+Lemma-EM2 : (a b : EMObj)
               {x : Obj A}
-              {φ  : FObj T x -> x } 
-              (c : EMObj {c₁} {c₂} {ℓ} {A} {T} x φ)
+              {φ : Hom A (FObj T x) x }
+              (c : EMObj {x} {φ})
               (g : EMHom b c)
               (f : EMHom a b) -> A [ A [ φ  o FMap T (A [ (EMap g)  o  (EMap f) ] ) ]  
                       ≈ A [ (A [ (EMap g)  o  (EMap f) ])  o φ ] ]
-Lemma-EM2 _ _ (emObj c φ isAlgebra ) g f = let open ≈-Reasoning (A) in
+Lemma-EM2 _ _ (emObj isAlgebra ) g f = let 
+      x = obj isAlgebra
+      φ = phi isAlgebra
+      open ≈-Reasoning (A) in
    begin
         φ  o FMap T (A [ (EMap g)  o  (EMap f) ] )
    ≈⟨ ? ⟩