--- a/universal-mapping.agda	Mon Jul 22 16:47:45 2013 +0900
+++ b/universal-mapping.agda	Mon Jul 22 17:11:05 2013 +0900
@@ -5,6 +5,7 @@
 open import Category.HomReasoning
 
 open Functor
+
 record IsUniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
                  ( U : Functor B A )
                  ( F : Obj A -> Obj B )
@@ -13,15 +14,17 @@
                  : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
    field
        universalMapping :   (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> 
-                     A [ A [ FMap U ( f * ) o η a' ]  ≈ f ]
+                     A [ A [ FMap U ( f * ) o  η a' ]  ≈ f ]
+
 
 record UniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
                  ( U : Functor B A )
                  ( F : Obj A -> Obj B )
                  ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) )
-                 ( _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) ->  Hom B (F a ) b )
                  : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
+    infixr 11 _*
     field
+       _* :  { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) ->  Hom B (F a ) b 
        isUniversalMapping : IsUniversalMapping A B U F η _*
 
 open NTrans
@@ -62,11 +65,13 @@
                  ( F : Functor A B )
                  ( η : NTrans A A identityFunctor ( U ○  F ) )
                  ( ε : NTrans B B  ( F ○  U ) identityFunctor ) ->
-      Adjunction A B U F η ε  -> UniversalMapping A B U (FObj F) (TMap η) (Solution A B U F ε)
+      Adjunction A B U F η ε  -> UniversalMapping A B U (FObj F) (TMap η) 
 Lemma1 A B U F η ε adj = record {
+         _* = Solution A B U F ε ;
          isUniversalMapping = record {
-                    universalMapping  = univeralMapping
+                    universalMapping  = universalMapping
               }
       } where
-         univeralMapping : {!!}
-         univeralMapping = {!!}
+         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 ]
+         universalMapping a b  = ?