Mercurial > hg > Members > kono > Proof > category

changeset 183:ea6fc610b480

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Contravariant functor done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 28 Aug 2013 17:29:01 +0900
parents 346e8eb35ec3
children d2d749318bee
files yoneda.agda
diffstat 1 files changed, 18 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/yoneda.agda	Wed Aug 28 17:00:49 2013 +0900
+++ b/yoneda.agda	Wed Aug 28 17:29:01 2013 +0900
@@ -57,9 +57,25 @@
           ; FMap =   λ {b c : Obj A } → λ ( f : Hom  A c b ) → λ (g : Hom  A b a ) →  (Category.op A) [ f o g ] 
         ; isFunctor = record {
              identity =  \{b} → extensionality ( λ x → lemma-CF1 {b} x )
-             ; distr = λ {a} {b} {c} {f} {g} → {!!}
-             ; ≈-cong = {!!}
+             ; distr = λ {a} {b} {c} {f} {g} → extensionality ( λ x → lemma-CF2 a b c f g x ) 
+             ; ≈-cong = λ eq → extensionality ( λ x →  lemma-CF3 x eq ) 
         } 
     }  where
         lemma-CF1 : {b : Obj A } → (x : Hom A b a) →  (Category.op A) [ id1 A b o x ] ≡ x
         lemma-CF1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ idL
+        lemma-CF2 :  (a₁ b c : Obj A) (f : Hom A b a₁) (g : Hom A c b ) → (x : Hom A a₁ a )→ 
+               Category.op A [ Category.op A [ g o f ] o x ] ≡ (Sets [ _[_o_] (Category.op A) g o _[_o_] (Category.op A) f ]) x
+        lemma-CF2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≈-≡ ( begin
+               Category.op A [ Category.op A [ g o f ] o x ]
+             ≈↑⟨ assoc ⟩
+               Category.op A [ g o Category.op A [ f o x ] ]
+             ≈⟨⟩
+               ( λ x →  Category.op A [ g o x  ]  ) ( ( λ x → Category.op A [ f o x ] ) x )
+             ∎ )
+        lemma-CF3 :  {b c : Obj A} {f g : Hom A c b } → (x : Hom A b a ) → A [ f ≈ g ] →  Category.op A [ f o x ] ≡ Category.op A [ g o x ]
+        lemma-CF3 {_} {_} {f} {g} x eq =  let open ≈-Reasoning (Category.op A) in ≈-≡   ( begin
+                Category.op A [ f o x ]
+             ≈⟨ resp refl-hom eq ⟩
+                Category.op A [ g o x ]
+             ∎ )
+