# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1374479265 -32400
# Node ID ad997bd9788ba849ce95b39f6a288d4235f05533
# Parent  4ac419251f866d8802436c989d8e6b5e26aa3b7c
isUniversalMapping

diff -r 4ac419251f86 -r ad997bd9788b universal-mapping.agda
--- a/universal-mapping.agda	Mon Jul 22 16:04:23 2013 +0900
+++ b/universal-mapping.agda	Mon Jul 22 16:47:45 2013 +0900
@@ -12,7 +12,7 @@
                  ( _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) ->  Hom B (F a ) b )
                  : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
    field
-       universalMapping :   {a' : Obj A} { b' : Obj B } -> ( f : Hom A a' (FObj U b') ) -> 
+       universalMapping :   (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> 
                      A [ A [ FMap U ( f * ) o η a' ]  ≈ f ]
 
 record UniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
@@ -54,7 +54,7 @@
                  ( 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 
+     { 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₂' ℓ')
@@ -62,12 +62,11 @@
                  ( 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 η) (Solution A B U F ε)
 Lemma1 A B U F η ε adj = record {
-         isUniversalMapping = {!!}
-      }
-
-
-
-
-
+         isUniversalMapping = record {
+                    universalMapping  = univeralMapping
+              }
+      } where
+         univeralMapping : {!!}
+         univeralMapping = {!!}