# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1377700344 -32400
# Node ID b2e01aa0924d33afc369f57ccf8327c11e8eb69b
# Parent  173d078ee443d24da6e720d13a7e3f16dd6b9dcf
y-nat (FMap of Yoneda Functor )

diff -r 173d078ee443 -r b2e01aa0924d yoneda.agda
--- a/yoneda.agda	Wed Aug 28 21:51:59 2013 +0900
+++ b/yoneda.agda	Wed Aug 28 23:32:24 2013 +0900
@@ -82,6 +82,29 @@
 YObj = Functor (Category.op A) (Sets {c₂})
 YHom = λ (f : YObj ) → λ (g : YObj ) → NTrans (Category.op A) Sets f g
 
+y-map :  ( a b : Obj A ) → (f : Hom A a b ) → (x : Obj (Category.op A)) → FObj (CF {a}) x → FObj (CF {b} ) x 
+y-map  a b f x = λ ( g : Hom A x a ) → A [ f o g ]  --  ( h : Hom A x b ) 
+
+y-nat : {a b : Obj A } → (f : Hom A a b ) → YHom (CF {a}) (CF {b}) 
+y-nat {a} {b} f = record { TMap =  y-map  a b f ; isNTrans = isNTrans1 {a} {b} f } where
+   lemma-CF5 : {a₁ b₁ : Obj (Category.op A)} {g : Hom (Category.op A) a₁ b₁} → {a b : Obj A } → (x : Hom A a₁ a) → (f : Hom A a b ) →
+                    (Sets [ FMap CF g o y-map a b f a₁ ]) x ≡ (Sets [ y-map a b f b₁ o FMap CF g ]) x
+   lemma-CF5 {a₁} {b₁} {g} {a} {b} x f = let open ≈-Reasoning (A) in ≈-≡ ( begin
+                A [ A [ f o x ] o g ]
+             ≈↑⟨ assoc ⟩
+                A [ f o A [ x  o g ] ]
+             ∎ )
+   lemma-CF4 : {a₁ b₁ : Obj (Category.op A)} {g : Hom (Category.op A) a₁ b₁} → {a b : Obj A } → (f : Hom A a b ) →
+        Sets [ Sets [ FMap CF g o y-map a b f a₁ ] ≈
+        Sets [ y-map a b f b₁ o FMap CF g ] ]
+   lemma-CF4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning (Sets {c₂})in begin
+                Sets [ FMap CF g o y-map a b f a₁ ]
+             ≈⟨ extensionality ( λ x → lemma-CF5 {a₁} {b₁} {g} {a} {b} x f)  ⟩
+                Sets [ y-map a b f b₁ o FMap CF g ]
+             ∎
+   isNTrans1 : {a b : Obj A } →  (f : Hom A a b ) → IsNTrans (Category.op A) (Sets {c₂}) (CF {a}) (CF {b}) (y-map a b f )
+   isNTrans1 {a} {b} f = record { commute = λ{a₁ b₁ g } → lemma-CF4 {a₁} {b₁} {g} {a} {b} f } 
+
 open NTrans 
 Yid : {a : YObj} → YHom a a
 Yid {a} = record { TMap = \a -> \x -> x ; isNTrans = isNTrans1 {a} } where
@@ -110,12 +133,41 @@
    isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) a c (λ x → Sets [ TMap f x o TMap g x ]) 
    isNTrans1 = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h }
 
-isSetsAop :  IsCategory YObj YHom _≡_ _+_ Yid
-isSetsAop  =  record  { isEquivalence =  ?
-                    ; identityL =   ?
-                    ; identityR =   ?
-                    ; o-resp-≈ =    ?
-                    ; associative = ?
-                    }
+_==_  :  {a b : YObj} → YHom a b → YHom a b → Set (c₂ ⊔ c₁)
+_==_  f g =  TMap f ≡ TMap g 
+
+infix  4 _==_
+
+isSetsAop :  IsCategory YObj YHom _==_ _+_ Yid
+isSetsAop  =  record  { isEquivalence =  record {refl = refl ; trans = ≡-trans ; sym = ≡-sym}
+                    ; identityL = refl
+                    ; identityR = refl
+                    ; o-resp-≈ =  λ{a b c f g h i } → o-resp-≈      {a} {b} {c} {f} {g} {h} {i}
+                    ; associative = refl
+                    } where
+                        o-resp-≈ : {A₁ B C : YObj} {f g : YHom A₁ B} {h i : YHom B C} → 
+                                f == g → h == i → h + f == i + g
+                        o-resp-≈ refl refl =  refl
+
+SetsAop : Category (suc (ℓ ⊔ (suc c₂) ⊔ c₁)) (suc ( ℓ ⊔ (suc c₂) ⊔ c₁))  (c₂ ⊔ c₁)
+SetsAop =
+  record { Obj = YObj
+         ; Hom = YHom
+         ; _o_ = _+_
+         ; _≈_ = _==_
+         ; Id  = Yid
+         ; isCategory = isSetsAop
+         }
+
+YonedaFunctor : Functor A SetsAop
+YonedaFunctor = record {
+         FObj = λ a → CF {a}
+       ; FMap = λ f → y-nat f
+       ; isFunctor = record {
+             identity =  {!!}
+             ; distr = {!!}
+             ; ≈-cong = {!!}
+        } 
+  }