--- a/universal-mapping.agda	Mon Jul 22 21:29:26 2013 +0900
+++ b/universal-mapping.agda	Tue Jul 23 00:29:17 2013 +0900
@@ -51,16 +51,14 @@
     field
        isAdjunction : IsAdjunction A B U F η ε
 
+--
+--   Adjunction yields solution of universal mapping 
+--
+--
+
 open Adjunction
 open UniversalMapping
 
-Solution : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
-                 ( U : Functor B A )
-                 ( F : Functor A B )
-                 ( ε : NTrans B B  ( F ○  U ) identityFunctor ) ->
-     { a : Obj A} { b : Obj B} -> ( f : Hom A a (FObj U b) ) ->  Hom B (FObj F a ) b 
-Solution  A B U F ε {a} {b} f = B [ TMap ε b o FMap F f ]
-
 Lemma1 : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                  ( U : Functor B A )
                  ( F : Functor A B )
@@ -68,17 +66,20 @@
                  ( ε : NTrans B B  ( F ○  U ) identityFunctor ) ->
       Adjunction A B U F η ε  -> UniversalMapping A B U (FObj F) (TMap η) 
 Lemma1 A B U F η ε adj = record {
-         _* = Solution A B U F ε ;
+         _* = solution  ;
          isUniversalMapping = record {
-                    universalMapping  = universalMapping
+                    universalMapping  = universalMapping;
+                    unique-universalMapping = uniqness
               }
       } where
+         solution :  { a : Obj A} { b : Obj B} -> ( f : Hom A a (FObj U b) ) ->  Hom B (FObj F a ) b 
+         solution  {_} {b} f = B [ TMap ε b o FMap F f ]
          universalMapping :   (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> 
-                     A [ A [ FMap U ( Solution A B U F ε f  ) o TMap η a' ]  ≈ f ]
+                     A [ A [ FMap U ( solution f) o TMap η a' ]  ≈ f ]
          universalMapping a b {f} = 
            let open ≈-Reasoning (A) in
               begin 
-                  FMap U ( Solution A B U F ε f  ) o TMap η a 
+                  FMap U ( solution  f) o TMap η a 
               ≈⟨⟩
                   FMap U (  B [ TMap ε b o FMap F f ] ) o TMap η a 
               ≈⟨ car (IsFunctor.distr ( isFunctor U )) ⟩
@@ -94,8 +95,22 @@
               ≈⟨  idL  ⟩
                   f
               ∎
+         uniqness :   (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  TMap η a' ]  ≈ f ] -> B [ solution f  ≈ g ]
+         uniqness a b f g = {!!}
 
 
+--
+--
+--  Universal mapping yields Adjunction
+--
+--
+
+
+--
+-- F is an functor
+--
+
 FunctorF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
                  ( U : Functor B A )
                  ( F : Obj A -> Obj B )