Mercurial > hg > Members > kono > Proof > category

changeset 194:3271d2d04b17

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
F2Nat→Nat2F done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 30 Aug 2013 19:46:40 +0900
parents 4e6f080f0107
children 428d46dfd5aa
files yoneda.agda
diffstat 1 files changed, 27 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/yoneda.agda	Fri Aug 30 16:49:28 2013 +0900
+++ b/yoneda.agda	Fri Aug 30 19:46:40 2013 +0900
@@ -239,8 +239,33 @@
 Nat2F {a} {F} ha =  ( TMap ha a ) (id1 A a)
 
 F2Nat→Nat2F : {a : Obj A } → {F : Obj SetsAop} → (fa : FObj F a) →  Nat2F {a} {F} (F2Nat {a} {F} fa) ≡ fa 
-F2Nat→Nat2F  = {!!}
+-- FMap F (Category.Category.Id A) fa ≡ fa
+F2Nat→Nat2F {a} {F} fa = let open ≈-Reasoning (Sets) in cong ( λ f → f fa ) (
+             begin
+               ( FMap F (id1 A _ )) 
+             ≈⟨ IsFunctor.identity (isFunctor F)    ⟩
+                id1 Sets (FObj F a)
+             ∎ )
+
+open  import  Relation.Binary.PropositionalEquality
+
+postulate extensionality2 : Relation.Binary.PropositionalEquality.Extensionality  c₁ c₂ 
+postulate extensionality3 : Relation.Binary.PropositionalEquality.Extensionality  c₂ c₂
 
 Nat2F→F2Nat : {a : Obj A } → {F : Obj SetsAop} → (ha : Hom SetsAop (CF {a}) F) →  SetsAop [ F2Nat {a} {F} (Nat2F {a} {F} ha) ≈ ha ]
-Nat2F→F2Nat = {!!}
+-- (λ b g → FMap F g (TMap ha a (Category.Category.Id A))) ≡ TMap ha
+Nat2F→F2Nat {a} {F} ha = let open ≡-Reasoning in
+             begin
+                ( λ (b : Obj A ) → λ (g : Hom A b a ) → FMap F g (TMap ha a (Category.Category.Id A))  )
+             ≡⟨ extensionality2 ( λ b → extensionality3 (λ g → lemma1 {a} {F} ha b g )) ⟩
+                TMap ha   
+             ∎ where
+               lemma1 :  {a : Obj A } → {F : Obj SetsAop} → (ha : Hom SetsAop (CF {a}) F) →  (b : Obj A ) → (g : Hom A b a ) → 
+                            FMap F g (TMap ha a (Category.Category.Id A)) ≡  TMap ha b g
+               lemma1 {a} {F} ha b g =  ?
 
+--     F :  op A → Sets
+--     ha : NTrans (op A) Sets (CF {a}) F
+--                FMap (CF {a}) g  o TMap ha a ≈   TMap ha b  o FMap F g
+
+