--- a/comparison-em.agda	Wed Nov 08 19:57:43 2017 +0900
+++ b/comparison-em.agda	Sat Nov 11 21:34:58 2017 +0900
@@ -19,14 +19,13 @@
                  { T : Functor A A }
                  { η : NTrans A A identityFunctor T }
                  { μ : NTrans A A (T ○ T) T }
-                 { M' : Monad A T η μ }
+                 { M' : IsMonad A T η μ }
       {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' ) 
       { U^K : Functor B A } { F^K : Functor A B }
       { η^K : NTrans A A identityFunctor ( U^K ○ F^K ) }
       { ε^K : NTrans B B ( F^K ○ U^K ) identityFunctor } 
       { μ^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 )
+      ( Adj^K : IsAdjunction A B U^K F^K η^K ε^K )
   where
 
 open import adj-monad
@@ -36,8 +35,8 @@
 μ^K' : NTrans A A (( U^K ○ F^K ) ○ ( U^K ○ F^K )) ( U^K ○ F^K ) 
 μ^K'  = UεF A B U^K F^K ε^K 
 
-M : Monad A (U^K ○ F^K ) η^K μ^K' 
-M =  Adj2Monad A B {U^K} {F^K} {η^K} {ε^K} Adj^K
+M : IsMonad A (U^K ○ F^K ) η^K μ^K' 
+M = Monad.isMonad ( Adj2Monad A B ( record { U = U^K; F = F^K ; η = η^K ; ε = ε^K ; isAdjunction =  Adj^K } ) )
 
 open import em-category {c₁} {c₂} {ℓ} {A} { U^K ○ F^K } { η^K } { μ^K' } { M } 
 
@@ -55,7 +54,7 @@
       identity1 b =  let open ≈-Reasoning (A) in
            begin
                 (FMap U^K (TMap ε^K b))  o TMap η^K (FObj U^K b)
-           ≈⟨ IsAdjunction.adjoint1 (isAdjunction Adj^K) ⟩
+           ≈⟨ IsAdjunction.adjoint1 Adj^K ⟩
                 id1 A (FObj U^K b)
            ∎