Mercurial > hg > Members > kono > Proof > category

changeset 189:c6ce3115cb1b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 29 Aug 2013 12:47:28 +0900
parents f4c9d7cbcbb9
children b82d7b054f28
files yoneda.agda
diffstat 1 files changed, 29 insertions(+), 27 deletions(-) [+]
line wrap: on
line diff
--- a/yoneda.agda	Thu Aug 29 10:14:59 2013 +0900
+++ b/yoneda.agda	Thu Aug 29 12:47:28 2013 +0900
@@ -1,3 +1,11 @@
+----
+--
+--  A → Sets^A^op  : Yoneda Functor
+--     Contravariant Functor h_a
+--     Nat(h_a,F)
+--                        Shinji KONO <kono@ie.u-ryukyu.ac.jp>
+----
+
 open import Category -- https://github.com/konn/category-agda                                                                                     
 open import Level
 open import Category.Sets
@@ -53,12 +61,12 @@
 
 CF : {a : Obj A} → Functor (Category.op A) (Sets {c₂})
 CF {a} = record {
-        FObj = λ b → Hom (Category.op A) a b  
-          ; 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} → extensionality ( λ x → lemma-CF2 a b c f g x ) 
-             ; ≈-cong = λ eq → extensionality ( λ x →  lemma-CF3 x eq ) 
+        FObj = λ b → Hom (Category.op A) a b  ;
+        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} → 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
@@ -87,21 +95,14 @@
 
 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
+   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 A in extensionality ( λ x →  ≈-≡ ( 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 } 
 
@@ -139,15 +140,16 @@
 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
+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 =