Mercurial > hg > Members > kono > Proof > category

changeset 192:d7e4b7b441be

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
F(a) → Nat(h_a,F) done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 30 Aug 2013 16:34:48 +0900
parents 45191dc3f78a
children 4e6f080f0107
files yoneda.agda
diffstat 1 files changed, 14 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/yoneda.agda	Fri Aug 30 15:28:57 2013 +0900
+++ b/yoneda.agda	Fri Aug 30 16:34:48 2013 +0900
@@ -215,9 +215,22 @@
 
 F2Nat : {a : Obj A} → {F : Obj SetsAop} →  FObj F a  → Hom SetsAop (CF {a}) F
 F2Nat {a} {F} x = record { TMap = F2Natmap {a} {F} {x} ; isNTrans = isNTrans1 } where
+   commute1 : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} (g : Hom A  a₁ a) →
+                (Sets [ FMap F f o  FMap F g ]) x ≡ FMap F (A [ g o  f ] ) x
+   commute1 g =  let open ≈-Reasoning (Sets) in
+            cong ( λ f → f x ) ( sym ( distr F )  )
    commute : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} → 
         Sets [ Sets [ FMap F f o F2Natmap {a} {F} {x} a₁ ] ≈ Sets [ F2Natmap {a} {F} {x} b o FMap CF f ] ]
-   commute {a₁} {b} {f} =  extensionality ( λ (g : Hom A a₁ a ) →　?  )
+   commute {a₁} {b} {f} =  let open ≈-Reasoning (Sets) in
+             begin
+                Sets [ FMap F f o F2Natmap {a} {F} {x} a₁ ]
+             ≈⟨⟩
+                Sets [ FMap F f o (λ ( g : Hom A a₁ a ) → ( FMap F g ) x) ]
+             ≈⟨ extensionality ( λ (g : Hom A  a₁ a) → commute1 {a₁} {b} {f} g ) ⟩
+                Sets [  (λ ( g : Hom A b a ) → ( FMap F g ) x) o FMap CF f ] 
+             ≈⟨⟩
+                Sets [ F2Natmap {a} {F} {x} b o FMap CF f ] 
+             ∎
    isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) (CF {a}) F (F2Natmap {a} {F})
    isNTrans1 = record { commute = λ {a₁ b f}  →  commute {a₁} {b} {f} }