--- a/comparison-em.agda	Sat Mar 04 11:05:55 2017 +0900
+++ b/comparison-em.agda	Sat Mar 04 16:26:57 2017 +0900
@@ -27,7 +27,7 @@
       { μ^K : NTrans A A (( U^K ○ F^K ) ○ ( U^K ○ F^K )) ( U^K ○ F^K ) }
       ( Adj^K : Adjunction A B U^K F^K η^K ε^K )
       ( RK : MResolution A B T U^K F^K {η^K} {ε^K} {μ^K} Adj^K )
-where
+  where
 
 open import adj-monad
 
@@ -45,11 +45,11 @@
 open NTrans
 open Adjunction
 open MResolution
-open Eilenberg-Moore-Hom
+open EMHom
 
 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 }
+     obj = FObj U^K b ; φ = 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 =  let open ≈-Reasoning (A) in