--- a/cat-utility.agda	Sat Aug 24 22:14:29 2013 +0900
+++ b/cat-utility.agda	Sun Aug 25 09:44:00 2013 +0900
@@ -34,72 +34,6 @@
                _* :  { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b 
                isUniversalMapping : IsUniversalMapping A B U F η _*
 
---     naturality of left
---     f' = k* f   k*: Hom A F(a) k,                                                                                                                        
---                        left                                               left                                                                           
---    f : Hom A F(a)   b --------> f* : Hom B a U(b)      f : Hom A F(a')b --------> f* : Hom B a' U(b)                                                     
---       |                               |                     |                               |                                                            
---       |k*                             |U(k*)                |F(h*)                          |h*                                                          
---       v                               v                     v                               v                                                            
---    f': Hom A F(a)   b'--------> f* : Hom B a U(b')     f': Hom A F(a)  b --------> f* : Hom B a U(b)                                                     
---                        left                                                                                                                              
-
-        record UnityOfOppsite  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
-                         ( U : Functor B A )
-                         ( F : Functor A B )
-                         : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
-           field
-               right  : {a : Obj A} { b : Obj B } → Hom A a ( FObj U b ) → Hom B (FObj F a) b
-               left   : {a : Obj A} { b : Obj B } → Hom B (FObj F a) b   → Hom A a ( FObj U b ) 
-               right-injective : {a : Obj A} { b : Obj B } → {f : Hom A a (FObj U b) }  → A [ left ( right f ) ≈ f ]
-               left-injective  : {a : Obj A} { b : Obj B } → {f : Hom B (FObj F a) b }  → B [ right ( left f ) ≈ f ]
-               left-commute1 : {a : Obj A} {b b' : Obj B } ->
-                       ( f : Hom B (FObj F a) b )  -> ( k : Hom B b b' ) ->
-                        A [  left ( B [ k o  f ] )  ≈ A [ FMap U k o left f  ] ]
-               left-commute2 : {a a' : Obj A} {b : Obj B } ->
-                       ( f : Hom B (FObj F a) b )  -> ( h : Hom A a' a ) ->
-                        A [ left ( B [ f  o  FMap F h ] )  ≈  A [ left f o h ] ]
-               r-cong : {a : Obj A} { b : Obj B } → { f g : Hom A a ( FObj U b ) } →  A [ f  ≈ g ] → B [ right f ≈ right g ]
-               l-cong : {a : Obj A} { b : Obj B } → { f g : Hom B (FObj F a) b }   →  B [ f  ≈ g ] → A [ left f ≈ left g   ]
-           right-commute1 : {a : Obj A} {b b' : Obj B } ->
-                       ( g : Hom A a (FObj U b))  -> ( k : Hom B b b' ) ->
-                        B [ B [ k o  right g ]   ≈ right ( A [ FMap U k o g  ] ) ]
-           right-commute1 g k =  let open ≈-Reasoning (B) in
-                     begin
-                          k o  right g
-                     ≈⟨ sym left-injective ⟩
-                          right ( left ( k o  right g ) )
-                     ≈⟨ r-cong ( left-commute1 (right g) k ) ⟩
-                          right ( A [ FMap U k o left ( right g ) ] )
-                     ≈⟨ r-cong (lemma-1 g k) ⟩
-                         right ( A [ FMap U k o g  ] ) 
-                     ∎ where
-                             lemma-1 : {a : Obj A} {b b' : Obj B } ->
-                               ( g : Hom A a (FObj U b))  -> ( k : Hom B b b' ) ->
-                                A [ A [ FMap U k o left ( right g ) ]   ≈  A [ FMap U k o g  ] ]
-                             lemma-1 g k = let open ≈-Reasoning (A) in
-                                   begin
-                                        FMap U k o left ( right g ) 
-                                   ≈⟨ cdr ( right-injective) ⟩
-                                        FMap U k o g  
-                                   ∎ 
-           right-commute2 : {a a' : Obj A} {b : Obj B } ->
-                       ( g : Hom A a (FObj U b) )  -> ( h : Hom A a' a ) ->
-                        B [ B [ right g  o  FMap F h ]   ≈  right ( A [ g o h ] ) ]
-           right-commute2 g h =  let open ≈-Reasoning (B) in
-                     begin
-                          right g  o  FMap F h 
-                     ≈⟨  sym left-injective ⟩
-                          right ( left ( right g  o  FMap F h  ))
-                     ≈⟨ r-cong ( left-commute2 (right g) h ) ⟩
-                          right ( A [ left ( right g ) o h ] )
-                     ≈⟨ r-cong ( lemma-2 g h  ) ⟩
-                          right ( A [ g o h ] )
-                     ∎  where
-                           lemma-2 :  {a a' : Obj A} {b : Obj B } ->
-                               ( g : Hom A a (FObj U b))  -> ( h : Hom A a' a ) ->
-                                A [ A [  left ( right g ) o h ]   ≈  A [ g o h  ] ]
-                           lemma-2 g h  = let open ≈-Reasoning (A) in car ( right-injective  )
         open NTrans
         open import Category.Cat
         record IsAdjunction  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')