# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1374496166 -32400
# Node ID 9694f93977caae315c88769b665d315f7e23d733
# Parent  e9fa5c95eff7da789019bcf20cb885b5a911f543
Functor Identity

diff -r e9fa5c95eff7 -r 9694f93977ca category.ind
--- a/category.ind	Mon Jul 22 19:07:31 2013 +0900
+++ b/category.ind	Mon Jul 22 21:29:26 2013 +0900
@@ -205,7 +205,7 @@
 $ η(a): a->UF(a)$ 
 
 put 
-\[    F(f) = (η(U(b))f)* \]
+\[    F(f) = (η(b)f)* \]
 \[ ε : FU -> 1_B        \]
 \[  ε(b) = (1_{U(b)})* \]
 
diff -r e9fa5c95eff7 -r 9694f93977ca universal-mapping.agda
--- a/universal-mapping.agda	Mon Jul 22 19:07:31 2013 +0900
+++ b/universal-mapping.agda	Mon Jul 22 21:29:26 2013 +0900
@@ -15,7 +15,8 @@
    field
        universalMapping :   (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> 
                      A [ A [ FMap U ( f * ) o  η a' ]  ≈ f ]
-
+       unique-universalMapping :   (a' : Obj A) ( b' : Obj B ) -> ( f : Hom A a' (FObj U b') ) -> ( g :  Hom B (F a') b') -> 
+                     A [ A [ FMap U g o  η a' ]  ≈ f ] -> B [ f * ≈ g ]
 
 record UniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
                  ( U : Functor B A )
@@ -102,9 +103,29 @@
        UniversalMapping A B U F η   -> Functor A B
 FunctorF A B U F η um = record {
               FObj = F;
-              FMap = \f ->  (_* um)  (A [  η (Category.cod A f )   o f ])   ;
-              isFunctor = isFunctor1
+              FMap = myFMap ;
+              isFunctor = myIsFunctor
        } where
-         isFunctor1 : ?
-         isFunctor1 = ?
+    myFMap : {a b : Obj A} -> Hom A a b -> Hom B (F a) (F b)
+    myFMap f = (_* um)  (A [  η (Category.cod A f )   o f ]) 
+    lemma-id-1 :  {a : Obj A} ->  A [ A [ FMap U (Id {_} {_} {_} {B} (F a))  o  η a ]  ≈ (A [ (η a) o (Id {_} {_} {_} {A} a) ]) ]
+    lemma-id-1 {a} = let open ≈-Reasoning (A) in
+       begin
+            A [ FMap U (Id {_} {_} {_} {B} (F a))  o  η a ] 
+       ≈⟨ ( car ( IsFunctor.identity ( isFunctor U )))  ⟩
+            A [ (Id {_} {_} {_} {A} (FObj U ( F a )) ) o  η a ] 
+       ≈⟨ idL  ⟩
+           η a
+       ≈⟨ sym idR  ⟩
+           (A [ (η a) o (Id {_} {_} {_} {A} a) ]) 
+       ∎
+    lemma-id :  {a : Obj A} →  B [ ( (_* um) (A [ (η a) o (Id {_} {_} {_} {A} a)] )) ≈ (Id {_} {_} {_} {B} (F a)) ]
+    lemma-id {a} =   ( IsUniversalMapping.unique-universalMapping ( isUniversalMapping um ) ) 
+              a (F a)  ((A [ (η a) o (Id {_} {_} {_} {A} a)] )) ((Id {_} {_} {_} {B} (F a))) lemma-id-1
+    myIsFunctor : IsFunctor A B F myFMap
+    myIsFunctor =
+      record { ≈-cong   = {!!}
+             ; identity = lemma-id
+             ; distr    = {!!}
+             }