--- a/universal-mapping.agda	Sat Aug 24 17:16:07 2013 +0900
+++ b/universal-mapping.agda	Sat Aug 24 22:14:29 2013 +0900
@@ -346,7 +346,11 @@
             right =  right ;
             left  =  left ; 
             right-injective =  right-injective  ;
-            left-injective = left-injective  
+            left-injective = left-injective  ;
+            left-commute1 = left-commute1 ;
+            left-commute2 = left-commute2 ;
+            r-cong = r-cong ;
+            l-cong = l-cong 
       } where
             right  : {a : Obj A} { b : Obj B } → Hom A a ( FObj U b ) → Hom B (FObj F a) b
             right {a} {b} f = B [ TMap ε b o FMap F f ] 
@@ -386,6 +390,19 @@
                      ≈⟨ idR  ⟩
                         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-commute1 = {!!}
+            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 ] ]
+            left-commute2 = {!!}
+            r-cong : {a : Obj A} { b : Obj B } → { f g : Hom A a ( FObj U b ) } →  A [ f  ≈ g ] → B [ right f ≈ right g ]
+            r-cong eq = let open ≈-Reasoning (B) in ( cdr ( fcong F  eq ) )
+            l-cong : {a : Obj A} { b : Obj B } → { f g : Hom B (FObj F a) b }   →  B [ f  ≈ g ] → A [ left f ≈ left g   ]
+            l-cong eq = let open ≈-Reasoning (A) in ( car ( fcong U  eq ) )
+
 
 open UnityOfOppsite
 
@@ -436,15 +453,29 @@
                     FMap U ( uo-solution A B U F uo f) o ( uo-η-map uo  ) a
                ≈⟨⟩
                     FMap U ( right uo  f) o left uo ( id1 B (FObj F a)  )
-               ≈⟨ {!!} ⟩
+               ≈↑⟨  left-commute1 uo ( id1 B (FObj F a)) ( right uo  f)  ⟩
+                    left uo ( B [  right uo  f o  id1 B (FObj F a) ] )
+               ≈⟨ l-cong uo lemma-1  ⟩
+                    left uo ( right uo f )
+               ≈⟨ right-injective uo ⟩
                     f
-               ∎
+               ∎ where
+                  lemma-1 :  B [ B [  right uo f o  id1 B (FObj F a) ] ≈ right uo f ]
+                  lemma-1 = let open ≈-Reasoning (B) in idR
          uniqueness :   {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g :  Hom B (FObj F a') b'} →
                      A [ A [ FMap U g o  ( uo-η-map uo  ) a' ]  ≈ f ] → B [ uo-solution A B U F uo f  ≈ g ]
          uniqueness {a} {b} {f} {g} eq = let open ≈-Reasoning (B) in
                begin
                     uo-solution A B U F uo f
-               ≈⟨ {!!} ⟩
+               ≈⟨⟩
+                    right uo  f
+               ≈↑⟨ r-cong uo eq ⟩
+                    right uo  ( A [  FMap U g o  left uo ( id1 B (FObj F a) ) ] )
+               ≈↑⟨ r-cong uo ( left-commute1 uo ( id1 B (FObj F a) ) g ) ⟩
+                    right uo ( left uo ( g  o ( id1 B (FObj F a) ) ) )
+               ≈⟨ left-injective uo  ⟩
+                    g  o ( id1 B (FObj F a) )
+               ≈⟨ idR ⟩
                     g
                ∎ 
 
@@ -458,18 +489,20 @@
                  { U : Functor B A }
                  { F : Functor A B }→  
                  ( uo : UnityOfOppsite A B U F)  → NTrans A A identityFunctor ( U ○  F )
-uo-η = {!!}
+uo-η  = {!!}
 
 UO2Adj : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                  { U : Functor B A }
                  { F : Functor A B }
-                 ( uo : UnityOfOppsite A B U F)  → Adjunction A B U F (uo-η uo) (uo-ε uo )
+                 ( uo : UnityOfOppsite A B U F)  
+                    → Adjunction A B U F ( uo-η uo ) (uo-ε uo )
 UO2Adj A B {U} {F} uo = record {
            isAdjunction = record {
                adjoint1 = adjoint1 ; 
                adjoint2 = adjoint2
            } 
        } where
+          um = UO2UM A B U F uo 
           adjoint1 :   { b : Obj B } →
                      A [ A [ ( FMap U ( TMap (uo-ε uo) b ))  o ( TMap (uo-η uo) ( FObj U b )) ]  ≈ id1 A (FObj U b) ]
           adjoint1  {b} = {!!}