Mercurial > hg > Members > kono > Proof > category

changeset 197:ec50ff189f62

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 31 Aug 2013 01:47:49 +0900
parents c040369bd6d4
children 1edba4226474
files yoneda.agda
diffstat 1 files changed, 121 insertions(+), 99 deletions(-) [+]
line wrap: on
line diff
--- a/yoneda.agda	Sat Aug 31 01:23:50 2013 +0900
+++ b/yoneda.agda	Sat Aug 31 01:47:49 2013 +0900
@@ -18,94 +18,13 @@
 
 
 -- Contravariant Functor : op A → Sets  ( Obj of Sets^{A^op} )
-open Functor
-
--- A is Locally small
-postulate ≈-≡ : {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y
-
-import Relation.Binary.PropositionalEquality
--- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
-postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
-
+--   Obj and Hom of Sets^A^op
 
-CF' : (a : Obj A) → Functor A Sets
-CF' a = record {
-        FObj = λ b → Hom A a b
-        ; FMap =   λ {b c : Obj A } → λ ( f : Hom A b c ) → λ (g : Hom A a b ) →  A [ f o g ] 
-        ; isFunctor = record {
-             identity = identity
-             ; distr = λ {a} {b} {c} {f} {g} → distr1 a b c f g
-             ; ≈-cong = cong1
-        } 
-    } where
-        lemma-CF1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x
-        lemma-CF1 {b} x = let open ≈-Reasoning (A) in ≈-≡ idL
-        identity : {b : Obj A} → Sets [ (λ (g : Hom A a b ) → A [ id1 A b o g ]) ≈ ( λ g → g ) ]
-        identity {b} = extensionality lemma-CF1
-        lemma-CF2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c) → (x : Hom A a a₁ )→ A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x
-        lemma-CF2 a₁ b c f g x = let open ≈-Reasoning (A) in ≈-≡ ( begin
-               A [ A [ g o f ] o x ]
-             ≈↑⟨ assoc ⟩
-               A [ g o A [ f o x ] ] 
-             ≈⟨⟩
-               ( λ x →  A [ g o x  ]  ) ( ( λ x → A [ f o x ] ) x )
-             ∎ )
-        distr1 :   (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c) →
-                Sets [ (λ g₁ → A [ A [ g o f ] o g₁ ]) ≈ Sets [ (λ g₁ → A [ g o g₁ ]) o (λ g₁ → A [ f o g₁ ]) ] ]
-        distr1 a b c f g = extensionality ( λ x → lemma-CF2 a b c f g x )
-        cong1 :  {A₁ B : Obj A} {f g : Hom A A₁ B} → A [ f ≈ g ] → Sets [ (λ g₁ → A [ f o g₁ ]) ≈ (λ g₁ → A [ g o g₁ ]) ]
-        cong1 eq = extensionality ( λ x → ( ≈-≡ (  
-                 (IsCategory.o-resp-≈  ( Category.isCategory A )) ( IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))) eq )))
-
-open import Function
-
-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 ) 
-        } 
-    }  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 ]
-             ∎ )
+open Functor
 
 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-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 ] ]
-             ∎ ) )
-   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
@@ -161,12 +80,115 @@
          ; isCategory = isSetsAop
          }
 
+-- A is Locally small
+postulate ≈-≡ : {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y
+
+import Relation.Binary.PropositionalEquality
+-- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
+postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
+
+-- non cotravariant version 
+
+y-obj' : (a : Obj A) → Functor A Sets
+y-obj' a = record {
+        FObj = λ b → Hom A a b
+        ; FMap =   λ {b c : Obj A } → λ ( f : Hom A b c ) → λ (g : Hom A a b ) →  A [ f o g ] 
+        ; isFunctor = record {
+             identity = identity
+             ; distr = λ {a} {b} {c} {f} {g} → distr1 a b c f g
+             ; ≈-cong = cong1
+        } 
+    } where
+        lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x
+        lemma-y-obj1 {b} x = let open ≈-Reasoning (A) in ≈-≡ idL
+        identity : {b : Obj A} → Sets [ (λ (g : Hom A a b ) → A [ id1 A b o g ]) ≈ ( λ g → g ) ]
+        identity {b} = extensionality lemma-y-obj1
+        lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c) → (x : Hom A a a₁ )→ A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x
+        lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (A) in ≈-≡ ( begin
+               A [ A [ g o f ] o x ]
+             ≈↑⟨ assoc ⟩
+               A [ g o A [ f o x ] ] 
+             ≈⟨⟩
+               ( λ x →  A [ g o x  ]  ) ( ( λ x → A [ f o x ] ) x )
+             ∎ )
+        distr1 :   (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c) →
+                Sets [ (λ g₁ → A [ A [ g o f ] o g₁ ]) ≈ Sets [ (λ g₁ → A [ g o g₁ ]) o (λ g₁ → A [ f o g₁ ]) ] ]
+        distr1 a b c f g = extensionality ( λ x → lemma-y-obj2 a b c f g x )
+        cong1 :  {A₁ B : Obj A} {f g : Hom A A₁ B} → A [ f ≈ g ] → Sets [ (λ g₁ → A [ f o g₁ ]) ≈ (λ g₁ → A [ g o g₁ ]) ]
+        cong1 eq = extensionality ( λ x → ( ≈-≡ (  
+                 (IsCategory.o-resp-≈  ( Category.isCategory A )) ( IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))) eq )))
+
+----
+--
+--  Object mapping in Yoneda Functor
+--
+----
+
+open import Function
+
+y-obj : (a : Obj A) → Functor (Category.op A) (Sets {c₂})
+y-obj 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-y-obj1 {b} x ) ;
+             distr = λ {a} {b} {c} {f} {g} → extensionality ( λ x → lemma-y-obj2 a b c f g x ) ;
+             ≈-cong = λ eq → extensionality ( λ x →  lemma-y-obj3 x eq ) 
+        } 
+    }  where
+        lemma-y-obj1 : {b : Obj A } → (x : Hom A b a) →  (Category.op A) [ id1 A b o x ] ≡ x
+        lemma-y-obj1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ idL
+        lemma-y-obj2 :  (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-y-obj2 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-y-obj3 :  {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-y-obj3 {_} {_} {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 ]
+             ∎ )
+
+
+----
+--
+--  Hom mapping in Yoneda Functor
+--
+----
+
+y-tmap :  ( a b : Obj A ) → (f : Hom A a b ) → (x : Obj (Category.op A)) → FObj (y-obj a) x → FObj (y-obj b ) x 
+y-tmap  a b f x = λ ( g : Hom A x a ) → A [ f o g ]  --  ( h : Hom A x b ) 
+
+y-map : {a b : Obj A } → (f : Hom A a b ) → YHom (y-obj a) (y-obj b) 
+y-map {a} {b} f = record { TMap =  y-tmap  a b f ; isNTrans = isNTrans1 {a} {b} f } where
+   lemma-y-obj4 : {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 (y-obj b) g o y-tmap a b f a₁ ] ≈
+        Sets [ y-tmap a b f b₁ o FMap (y-obj a) g ] ]
+   lemma-y-obj4 {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 ] ]
+             ∎ ) )
+   isNTrans1 : {a b : Obj A } →  (f : Hom A a b ) → IsNTrans (Category.op A) (Sets {c₂}) (y-obj a) (y-obj b) (y-tmap a b f )
+   isNTrans1 {a} {b} f = record { commute = λ{a₁ b₁ g } → lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f } 
+
 postulate extensionality1 : Relation.Binary.PropositionalEquality.Extensionality c₁ c₂
 
+-----
+--
+-- Yoneda Functor itself
+--
+-----
+
 YonedaFunctor : Functor A SetsAop
 YonedaFunctor = record {
-         FObj = λ a → CF {a}
-       ; FMap = λ f → y-nat f
+         FObj = λ a → y-obj a
+       ; FMap = λ f → y-map f
        ; isFunctor = record {
              identity =  identity
              ; distr = distr1
@@ -174,7 +196,7 @@
 
         } 
   } where
-        ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop [ y-nat f ≈ y-nat g ]
+        ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop [ y-map f ≈ y-map g ]
         ≈-cong {a} {b} {f} {g} eq =  let open ≈-Reasoning (A) in  -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [  g o  g₁ ] )
            extensionality1 ( λ x → extensionality (
              λ h →  ≈-≡  ( begin
@@ -183,7 +205,7 @@
                 A [ g o h ]
              ∎
           ) )  )
-        identity : {a : Obj A} → SetsAop [ y-nat (id1 A a) ≈ id1 SetsAop (CF {a} )  ]
+        identity : {a : Obj A} → SetsAop [ y-map (id1 A a) ≈ id1 SetsAop (y-obj a )  ]
         identity  {a} =  let open ≈-Reasoning (A) in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x)
            extensionality1 ( λ x → extensionality (
              λ g →  ≈-≡  ( begin
@@ -192,7 +214,7 @@
                 g
              ∎
           ) )  )
-        distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop [ y-nat (A [ g o f ]) ≈ SetsAop [ y-nat g o y-nat f ] ]
+        distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop [ y-map (A [ g o f ]) ≈ SetsAop [ y-map g o y-map f ] ]
         distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in -- (λ x g₁ → (A [  (A [ g o f]  o g₁ ]))) ≡ (λ x x₁ → A [  g o A [ f o x₁ ] ] )
            extensionality1 ( λ x → extensionality (
              λ h →  ≈-≡  ( begin
@@ -211,32 +233,32 @@
 --      x ∈ F(a) , (g : Hom A b a)  → ( FMap F g ) x
 ------
 
-F2Natmap :  {a : Obj A} → {F : Obj SetsAop} → {x : FObj F a} → (b : Obj (Category.op A)) → Hom Sets (FObj (CF {a}) b) (FObj F b)
+F2Natmap :  {a : Obj A} → {F : Obj SetsAop} → {x : FObj F a} → (b : Obj (Category.op A)) → Hom Sets (FObj (y-obj a) b) (FObj F b)
 F2Natmap {a} {F} {x} b = λ ( g : Hom A b a ) → ( FMap F g ) x
 
-F2Nat : {a : Obj A} → {F : Obj SetsAop} →  FObj F a  → Hom SetsAop (CF {a}) F
+F2Nat : {a : Obj A} → {F : Obj SetsAop} →  FObj F a  → Hom SetsAop (y-obj 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 ] ]
+        Sets [ Sets [ FMap F f o F2Natmap {a} {F} {x} a₁ ] ≈ Sets [ F2Natmap {a} {F} {x} b o FMap (y-obj a) f ] ]
    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 [  (λ ( g : Hom A b a ) → ( FMap F g ) x) o FMap (y-obj a) f ] 
              ≈⟨⟩
-                Sets [ F2Natmap {a} {F} {x} b o FMap CF f ] 
+                Sets [ F2Natmap {a} {F} {x} b o FMap (y-obj a) f ] 
              ∎
-   isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) (CF {a}) F (F2Natmap {a} {F})
+   isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) (y-obj a) F (F2Natmap {a} {F})
    isNTrans1 = record { commute = λ {a₁ b f}  →  commute {a₁} {b} {f} } 
 
 
-Nat2F : {a : Obj A} → {F : Obj SetsAop} →  Hom SetsAop (CF {a}) F  → FObj F a 
+Nat2F : {a : Obj A} → {F : Obj SetsAop} →  Hom SetsAop (y-obj a) F  → FObj F a 
 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 
@@ -254,10 +276,10 @@
 postulate extensionality3 : Relation.Binary.PropositionalEquality.Extensionality  c₂ c₂
 
 --     F :  op A → Sets
---     ha : NTrans (op A) Sets (CF {a}) F
---                FMap F  g  o TMap ha a ≈   TMap ha b  o FMap (CF {a}) g
+--     ha : NTrans (op A) Sets (y-obj {a}) F
+--                FMap F  g  o TMap ha a ≈   TMap ha b  o FMap (y-obj {a}) g
 
-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 : {a : Obj A } → {F : Obj SetsAop} → (ha : Hom SetsAop (y-obj a) F) →  SetsAop [ F2Nat {a} {F} (Nat2F {a} {F} ha) ≈ 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))  )
@@ -265,7 +287,7 @@
                 begin
                     FMap F g (TMap ha a (Category.Category.Id A)) 
                 ≡⟨  Relation.Binary.PropositionalEquality.cong (λ f → f (Category.Category.Id A)) (IsNTrans.commute (isNTrans ha)) ⟩
-                    TMap ha b (FMap (CF {a}) g (Category.Category.Id A))
+                    TMap ha b (FMap (y-obj a) g (Category.Category.Id A))
                 ≡⟨⟩
                     TMap ha b ( (A Category.o Category.Category.Id A) g )
                 ≡⟨  Relation.Binary.PropositionalEquality.cong ( TMap ha b ) ( ≈-≡ (IsCategory.identityL  ( Category.isCategory A ))) ⟩