--- a/universal-mapping.agda	Fri Aug 23 15:38:03 2013 +0900
+++ b/universal-mapping.agda	Fri Aug 23 17:30:04 2013 +0900
@@ -389,18 +389,14 @@
 
 open UnityOfOppsite
 
---    f   :   a -> U(b)
---    f*  : F(a)->   b
-
---   U(f*) :     UF(a) ->   U(b)
+--   f                            : a -----------> U(b)
+--   FMap U ( right uo f )        :      UF(a) --> U(b)
+--   FMap U ( right uo f ) o η    : a -> UF(a) --> U(b)
+--   right (FMap U ( right uo f )  o η)
 
---   ∃g          F(g) = right f         <-----       left F(g) = f
---   ∃g          UF(g) = U(f*)
-
---   ∃f          U(f) = left g         <-----        right U(f) = g
-
---   UF(f) :     UF(a) -> UFU(b)
-
+--   right f                      : F(a) --------> b
+--   ε  o (FMap F f)              : F(a)--FU(b)--> b
+--   left (ε  o (FMap F f))       : a -----------> U(b) 
 
 
 uo-η-map  : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ'} 
@@ -414,36 +410,27 @@
                  ( F : Functor A B ) → 
                  ( uo : UnityOfOppsite A B U F)  →  {a : Obj A} {b : Obj B } -> 
                        ( f : Hom A a (FObj U b )) -> Hom B (FObj F a) b
-uo-solution A B U F uo {a} {b} f =  B  [ right uo (id1 A (FObj U b)) o FMap F f ] --   right uo f
-
-lemma-u1 :  {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)  →
-                {a : Obj A} {b : Obj B } -> ( f : Hom A a (FObj U b ))  ->
-        B [ B  [ right uo (id1 A (FObj U b)) o FMap F f ] ≈  right uo f ]
-lemma-u1 = {!!}
+uo-solution A B U F uo {a} {b} f =  {!!} -- B  [ right uo (id1 A (FObj U b)) o FMap F f ] 
+                                    -- right uo f
 
 lemma-u2 :  {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)  →
-                {a : Obj A} {b : Obj B } -> ( f* : Hom B (FObj F a ) b )  ->
-        A [ A  [ FMap U f*  o  left uo (id1 B (FObj F a)) ] ≈  left uo f* ]
+                {a : Obj A} {b : Obj B } -> ( f : Hom A a (FObj U b ))  ->
+        B [ B  [ right uo (id1 A (FObj U b)) o FMap F f ] ≈  right uo f ]
 lemma-u2 = {!!}
----   FMap U f*  o id  = FMap U f*
----       left uo f * = FMap U f*
----       left uo id1 = FMap U id = id
---            f = right (FMap U f)
 
-lemma-u3 :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ'}
+lemma-u1 :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁' c₂' ℓ'}
                  { U : Functor B A }
-                 { F : Functor A B } →
+                 { F : Functor A B } →  
                  ( uo : UnityOfOppsite A B U F)  →
-                {a : Obj A} {b : Obj B } -> ( f* : Hom B (FObj F a ) b )  ->
-        B [  right uo ( FMap U f*) ≈  ? ]
-lemma-u3 = ?
+                {a : Obj A} {b : Obj B } -> ( f : Hom A a (FObj U b ) )  ->
+        A [ A  [ FMap U (right uo f)  o  left uo (id1 B (FObj F a)) ] ≈  f ]
+lemma-u1 = {!!}
 
+--     F(ε(b)) o η(F(b))
+--     F( right uo (id1 A (FObj U b))  ) o  left uo (id1 B (FObj F a)) ] == 1
 
 UO2UM  : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                  ( U : Functor B A )