--- a/yoneda.agda	Sat Aug 31 01:51:38 2013 +0900
+++ b/yoneda.agda	Sat Aug 31 01:57:35 2013 +0900
@@ -87,36 +87,6 @@
 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
 postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
--- non cotravariant version 
-
-y-obj' : (a : Obj A) → Functor A Sets
-y-obj' a = record {
-        FObj = λ b → Hom A a b
-        ; FMap =   λ {b c : Obj A } → λ ( f : Hom A b c ) → λ (g : Hom A a b ) →  A [ f o g ] 
-        ; isFunctor = record {
-             identity = identity
-             ; distr = λ {a} {b} {c} {f} {g} → distr1 a b c f g
-             ; ≈-cong = cong1
-        } 
-    } where
-        lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x
-        lemma-y-obj1 {b} x = let open ≈-Reasoning (A) in ≈-≡ idL
-        identity : {b : Obj A} → Sets [ (λ (g : Hom A a b ) → A [ id1 A b o g ]) ≈ ( λ g → g ) ]
-        identity {b} = extensionality lemma-y-obj1
-        lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c) → (x : Hom A a a₁ )→ A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x
-        lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (A) in ≈-≡ ( begin
-               A [ A [ g o f ] o x ]
-             ≈↑⟨ assoc ⟩
-               A [ g o A [ f o x ] ] 
-             ≈⟨⟩
-               ( λ x →  A [ g o x  ]  ) ( ( λ x → A [ f o x ] ) x )
-             ∎ )
-        distr1 :   (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c) →
-                Sets [ (λ g₁ → A [ A [ g o f ] o g₁ ]) ≈ Sets [ (λ g₁ → A [ g o g₁ ]) o (λ g₁ → A [ f o g₁ ]) ] ]
-        distr1 a b c f g = extensionality ( λ x → lemma-y-obj2 a b c f g x )
-        cong1 :  {A₁ B : Obj A} {f g : Hom A A₁ B} → A [ f ≈ g ] → Sets [ (λ g₁ → A [ f o g₁ ]) ≈ (λ g₁ → A [ g o g₁ ]) ]
-        cong1 eq = extensionality ( λ x → ( ≈-≡ (  
-                 (IsCategory.o-resp-≈  ( Category.isCategory A )) ( IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))) eq )))
 
 ----
 --
@@ -229,7 +199,7 @@
 --
 --  F : A → Sets  ∈ Obj SetsAop
 --
---  F(a) ⇔ Nat(h_a,F)
+--  F(a) -> Nat(h_a,F)
 --      x ∈ F(a) , (g : Hom A b a)  → ( FMap F g ) x
 ------
 
@@ -258,12 +228,19 @@
    isNTrans1 = record { commute = λ {a₁ b f}  →  commute {a₁} {b} {f} } 
 
 
+--  F(a) <- Nat(h_a,F)
 Nat2F : {a : Obj A} → {F : Obj SetsAop} →  Hom SetsAop (y-obj a) F  → FObj F a 
 Nat2F {a} {F} ha =  ( TMap ha a ) (id1 A a)
 
+----
+--
+-- Prove  Bijection (as routine exercise ...)
+--
+----
+
 F2Nat→Nat2F : {a : Obj A } → {F : Obj SetsAop} → (fa : FObj F a) →  Nat2F {a} {F} (F2Nat {a} {F} fa) ≡ fa 
--- FMap F (Category.Category.Id A) fa ≡ fa
 F2Nat→Nat2F {a} {F} fa = let open ≈-Reasoning (Sets) in cong ( λ f → f fa ) (
+             -- FMap F (Category.Category.Id A) fa ≡ fa
              begin
                ( FMap F (id1 A _ )) 
              ≈⟨ IsFunctor.identity (isFunctor F)    ⟩
@@ -298,7 +275,7 @@
              ∎ 
 
 -- Yoneda's Lemma
---    full and faithfull
+--    Yoneda Functor is full and faithfull
 --    that is FMapp Yoneda is injective and surjective
 
 --  λ b g → (A Category.o f₁) g
@@ -307,7 +284,7 @@
 
 --  F2Nat is bijection so FMap YonedaFunctor also ( using functional extensionality )
 
---  Full embedding requires injective on Object, that is
+--  Full embedding of Yoneda Functor requires injective on Object, that is
 --     FObj YonedaFunctor a   ≡ FObj YonedaFunctor b → a  ≡ b
 
 dom-equivalence : {a b : Obj A} → {f g : Hom A a b} → A [ f ≈ g ] → Category.dom A f ≡ Category.dom A g
@@ -325,4 +302,4 @@
 -- YondaLemma2 : {a b : Obj A }  → (λ x → FObj (FObj YonedaFunctor a) x)  ≡ (λ x → FObj (FObj YonedaFunctor b  ) x)  →  
 --        {f : Hom A a b } → a ≡ b 
 -- YondaLemma2 {a} {b} eq  {f}  = {!!} eq
--- I cannot prove this, sorry
+-- I cannot prove this, please help.