Mercurial > hg > Members > kono > Proof > category
annotate yoneda.agda @ 191:45191dc3f78a
nat continue...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 30 Aug 2013 15:28:57 +0900 |
| parents | b82d7b054f28 |
| children | d7e4b7b441be |
| rev | line source |
|---|---|
| 189 | 1 ---- |
| 2 -- | |
| 3 -- A → Sets^A^op : Yoneda Functor | |
| 4 -- Contravariant Functor h_a | |
| 5 -- Nat(h_a,F) | |
| 6 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> | |
| 7 ---- | |
| 8 | |
| 178 | 9 open import Category -- https://github.com/konn/category-agda |
| 10 open import Level | |
| 11 open import Category.Sets | |
| 12 module yoneda { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where | |
| 13 | |
| 14 open import HomReasoning | |
| 15 open import cat-utility | |
| 179 | 16 open import Relation.Binary.Core |
| 17 open import Relation.Binary | |
| 18 | |
| 178 | 19 |
| 20 -- Contravariant Functor : op A → Sets ( Obj of Sets^{A^op} ) | |
| 179 | 21 open Functor |
| 178 | 22 |
| 181 | 23 -- A is Locally small |
| 24 postulate ≈-≡ : {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y | |
| 25 | |
| 26 import Relation.Binary.PropositionalEquality | |
| 27 -- 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 ) | |
| 28 postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ | |
| 29 | |
| 30 | |
|
182
346e8eb35ec3
contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
181
diff
changeset
|
31 CF' : (a : Obj A) → Functor A Sets |
|
346e8eb35ec3
contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
181
diff
changeset
|
32 CF' a = record { |
| 178 | 33 FObj = λ b → Hom A a b |
|
180
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
34 ; FMap = λ {b c : Obj A } → λ ( f : Hom A b c ) → λ (g : Hom A a b ) → A [ f o g ] |
| 178 | 35 ; isFunctor = record { |
|
180
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
36 identity = identity |
|
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
37 ; distr = λ {a} {b} {c} {f} {g} → distr1 a b c f g |
| 178 | 38 ; ≈-cong = cong1 |
| 39 } | |
| 40 } where | |
| 181 | 41 lemma-CF1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x |
| 42 lemma-CF1 {b} x = let open ≈-Reasoning (A) in ≈-≡ idL | |
|
180
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
43 identity : {b : Obj A} → Sets [ (λ (g : Hom A a b ) → A [ id1 A b o g ]) ≈ ( λ g → g ) ] |
| 181 | 44 identity {b} = extensionality lemma-CF1 |
| 45 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 | |
| 46 lemma-CF2 a₁ b c f g x = let open ≈-Reasoning (A) in ≈-≡ ( begin | |
| 47 A [ A [ g o f ] o x ] | |
| 48 ≈↑⟨ assoc ⟩ | |
| 49 A [ g o A [ f o x ] ] | |
| 50 ≈⟨⟩ | |
| 51 ( λ x → A [ g o x ] ) ( ( λ x → A [ f o x ] ) x ) | |
| 52 ∎ ) | |
|
180
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
53 distr1 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c) → |
|
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
54 Sets [ (λ g₁ → A [ A [ g o f ] o g₁ ]) ≈ Sets [ (λ g₁ → A [ g o g₁ ]) o (λ g₁ → A [ f o g₁ ]) ] ] |
| 181 | 55 distr1 a b c f g = extensionality ( λ x → lemma-CF2 a b c f g x ) |
|
180
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
56 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₁ ]) ] |
| 181 | 57 cong1 eq = extensionality ( λ x → ( ≈-≡ ( |
| 58 (IsCategory.o-resp-≈ ( Category.isCategory A )) ( IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A ))) eq ))) | |
| 178 | 59 |
|
182
346e8eb35ec3
contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
181
diff
changeset
|
60 open import Function |
| 178 | 61 |
| 184 | 62 CF : {a : Obj A} → Functor (Category.op A) (Sets {c₂}) |
| 63 CF {a} = record { | |
| 189 | 64 FObj = λ b → Hom (Category.op A) a b ; |
| 65 FMap = λ {b c : Obj A } → λ ( f : Hom A c b ) → λ (g : Hom A b a ) → (Category.op A) [ f o g ] ; | |
| 66 isFunctor = record { | |
| 67 identity = \{b} → extensionality ( λ x → lemma-CF1 {b} x ) ; | |
| 68 distr = λ {a} {b} {c} {f} {g} → extensionality ( λ x → lemma-CF2 a b c f g x ) ; | |
| 69 ≈-cong = λ eq → extensionality ( λ x → lemma-CF3 x eq ) | |
|
182
346e8eb35ec3
contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
181
diff
changeset
|
70 } |
|
346e8eb35ec3
contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
181
diff
changeset
|
71 } where |
|
346e8eb35ec3
contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
181
diff
changeset
|
72 lemma-CF1 : {b : Obj A } → (x : Hom A b a) → (Category.op A) [ id1 A b o x ] ≡ x |
|
346e8eb35ec3
contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
181
diff
changeset
|
73 lemma-CF1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ idL |
|
183
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
74 lemma-CF2 : (a₁ b c : Obj A) (f : Hom A b a₁) (g : Hom A c b ) → (x : Hom A a₁ a )→ |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
75 Category.op A [ Category.op A [ g o f ] o x ] ≡ (Sets [ _[_o_] (Category.op A) g o _[_o_] (Category.op A) f ]) x |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
76 lemma-CF2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≈-≡ ( begin |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
77 Category.op A [ Category.op A [ g o f ] o x ] |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
78 ≈↑⟨ assoc ⟩ |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
79 Category.op A [ g o Category.op A [ f o x ] ] |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
80 ≈⟨⟩ |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
81 ( λ x → Category.op A [ g o x ] ) ( ( λ x → Category.op A [ f o x ] ) x ) |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
82 ∎ ) |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
83 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 ] |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
84 lemma-CF3 {_} {_} {f} {g} x eq = let open ≈-Reasoning (Category.op A) in ≈-≡ ( begin |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
85 Category.op A [ f o x ] |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
86 ≈⟨ resp refl-hom eq ⟩ |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
87 Category.op A [ g o x ] |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
88 ∎ ) |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
89 |
| 184 | 90 YObj = Functor (Category.op A) (Sets {c₂}) |
| 91 YHom = λ (f : YObj ) → λ (g : YObj ) → NTrans (Category.op A) Sets f g | |
| 92 | |
|
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
93 y-map : ( a b : Obj A ) → (f : Hom A a b ) → (x : Obj (Category.op A)) → FObj (CF {a}) x → FObj (CF {b} ) x |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
94 y-map a b f x = λ ( g : Hom A x a ) → A [ f o g ] -- ( h : Hom A x b ) |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
95 |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
96 y-nat : {a b : Obj A } → (f : Hom A a b ) → YHom (CF {a}) (CF {b}) |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
97 y-nat {a} {b} f = record { TMap = y-map a b f ; isNTrans = isNTrans1 {a} {b} f } where |
| 189 | 98 lemma-CF4 : {a₁ b₁ : Obj (Category.op A)} {g : Hom (Category.op A) a₁ b₁} → {a b : Obj A } → (f : Hom A a b ) → |
| 99 Sets [ Sets [ FMap CF g o y-map a b f a₁ ] ≈ | |
| 100 Sets [ y-map a b f b₁ o FMap CF g ] ] | |
| 101 lemma-CF4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality ( λ x → ≈-≡ ( begin | |
|
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
102 A [ A [ f o x ] o g ] |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
103 ≈↑⟨ assoc ⟩ |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
104 A [ f o A [ x o g ] ] |
| 189 | 105 ∎ ) ) |
|
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
106 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 ) |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
107 isNTrans1 {a} {b} f = record { commute = λ{a₁ b₁ g } → lemma-CF4 {a₁} {b₁} {g} {a} {b} f } |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
108 |
| 184 | 109 open NTrans |
| 110 Yid : {a : YObj} → YHom a a | |
| 111 Yid {a} = record { TMap = \a -> \x -> x ; isNTrans = isNTrans1 {a} } where | |
| 112 isNTrans1 : {a : YObj } → IsNTrans (Category.op A) (Sets {c₂}) a a (\a -> \x -> x ) | |
| 113 isNTrans1 {a} = record { commute = refl } | |
| 114 | |
| 115 _+_ : {a b c : YObj} → YHom b c → YHom a b → YHom a c | |
| 185 | 116 _+_{a} {b} {c} f g = record { TMap = λ x → Sets [ TMap f x o TMap g x ] ; isNTrans = isNTrans1 } where |
| 117 commute1 : (a b c : YObj ) (f : YHom b c) (g : YHom a b ) | |
| 118 (a₁ b₁ : Obj (Category.op A)) (h : Hom (Category.op A) a₁ b₁) → | |
| 119 Sets [ Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] ≈ | |
| 120 Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ] | |
| 121 commute1 a b c f g a₁ b₁ h = let open ≈-Reasoning (Sets {c₂})in begin | |
| 122 Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] | |
| 123 ≈⟨ assoc {_} {_} {_} {_} {FMap c h } {TMap f a₁} {TMap g a₁} ⟩ | |
| 124 Sets [ Sets [ FMap c h o TMap f a₁ ] o TMap g a₁ ] | |
| 125 ≈⟨ car (nat f) ⟩ | |
| 126 Sets [ Sets [ TMap f b₁ o FMap b h ] o TMap g a₁ ] | |
| 127 ≈↑⟨ assoc {_} {_} {_} {_} { TMap f b₁} {FMap b h } {TMap g a₁}⟩ | |
| 128 Sets [ TMap f b₁ o Sets [ FMap b h o TMap g a₁ ] ] | |
| 129 ≈⟨ cdr {_} {_} {_} {_} {_} { TMap f b₁} (nat g) ⟩ | |
| 130 Sets [ TMap f b₁ o Sets [ TMap g b₁ o FMap a h ] ] | |
| 131 ≈↑⟨ assoc {_} {_} {_} {_} {TMap f b₁} {TMap g b₁} { FMap a h} ⟩ | |
| 132 Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] | |
| 133 ∎ | |
| 134 isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) a c (λ x → Sets [ TMap f x o TMap g x ]) | |
| 135 isNTrans1 = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h } | |
| 184 | 136 |
|
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
137 _==_ : {a b : YObj} → YHom a b → YHom a b → Set (c₂ ⊔ c₁) |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
138 _==_ f g = TMap f ≡ TMap g |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
139 |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
140 infix 4 _==_ |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
141 |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
142 isSetsAop : IsCategory YObj YHom _==_ _+_ Yid |
| 189 | 143 isSetsAop = |
| 144 record { isEquivalence = record {refl = refl ; trans = ≡-trans ; sym = ≡-sym} | |
| 145 ; identityL = refl | |
| 146 ; identityR = refl | |
| 147 ; o-resp-≈ = λ{a b c f g h i } → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} | |
| 148 ; associative = refl | |
| 149 } where | |
| 150 o-resp-≈ : {A₁ B C : YObj} {f g : YHom A₁ B} {h i : YHom B C} → | |
| 151 f == g → h == i → h + f == i + g | |
| 152 o-resp-≈ refl refl = refl | |
|
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
153 |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
154 SetsAop : Category (suc (ℓ ⊔ (suc c₂) ⊔ c₁)) (suc ( ℓ ⊔ (suc c₂) ⊔ c₁)) (c₂ ⊔ c₁) |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
155 SetsAop = |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
156 record { Obj = YObj |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
157 ; Hom = YHom |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
158 ; _o_ = _+_ |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
159 ; _≈_ = _==_ |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
160 ; Id = Yid |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
161 ; isCategory = isSetsAop |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
162 } |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
163 |
|
188
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
164 postulate extensionality1 : Relation.Binary.PropositionalEquality.Extensionality c₁ c₂ |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
165 |
|
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
166 YonedaFunctor : Functor A SetsAop |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
167 YonedaFunctor = record { |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
168 FObj = λ a → CF {a} |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
169 ; FMap = λ f → y-nat f |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
170 ; isFunctor = record { |
| 187 | 171 identity = identity |
| 172 ; distr = distr1 | |
| 173 ; ≈-cong = ≈-cong | |
|
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
174 } |
| 187 | 175 } where |
| 176 ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop [ y-nat f ≈ y-nat g ] | |
|
188
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
177 ≈-cong {a} {b} {f} {g} eq = let open ≈-Reasoning (A) in -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [ g o g₁ ] ) |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
178 extensionality1 ( λ x → extensionality ( |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
179 λ h → ≈-≡ ( begin |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
180 A [ f o h ] |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
181 ≈⟨ resp refl-hom eq ⟩ |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
182 A [ g o h ] |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
183 ∎ |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
184 ) ) ) |
| 187 | 185 identity : {a : Obj A} → SetsAop [ y-nat (id1 A a) ≈ id1 SetsAop (CF {a} ) ] |
|
188
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
186 identity {a} = let open ≈-Reasoning (A) in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x) |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
187 extensionality1 ( λ x → extensionality ( |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
188 λ g → ≈-≡ ( begin |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
189 A [ id1 A a o g ] |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
190 ≈⟨ idL ⟩ |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
191 g |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
192 ∎ |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
193 ) ) ) |
| 187 | 194 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 ] ] |
| 191 | 195 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₁ ] ] ) |
|
188
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
196 extensionality1 ( λ x → extensionality ( |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
197 λ h → ≈-≡ ( begin |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
198 A [ A [ g o f ] o h ] |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
199 ≈↑⟨ assoc ⟩ |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
200 A [ g o A [ f o h ] ] |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
201 ∎ |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
202 ) ) ) |
| 184 | 203 |
| 185 | 204 |
| 190 | 205 ------ |
| 206 -- | |
| 207 -- F : A → Sets ∈ Obj SetsAop | |
| 208 -- | |
| 209 -- F(a) ⇔ Nat(h_a,F) | |
| 191 | 210 -- x ∈ F(a) , (g : Hom A b a) → ( FMap F g ) x |
| 190 | 211 ------ |
| 187 | 212 |
| 191 | 213 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) |
| 214 F2Natmap {a} {F} {x} b = λ ( g : Hom A b a ) → ( FMap F g ) x | |
| 190 | 215 |
| 216 F2Nat : {a : Obj A} → {F : Obj SetsAop} → FObj F a → Hom SetsAop (CF {a}) F | |
| 191 | 217 F2Nat {a} {F} x = record { TMap = F2Natmap {a} {F} {x} ; isNTrans = isNTrans1 } where |
| 218 commute : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} → | |
| 219 Sets [ Sets [ FMap F f o F2Natmap {a} {F} {x} a₁ ] ≈ Sets [ F2Natmap {a} {F} {x} b o FMap CF f ] ] | |
| 220 commute {a₁} {b} {f} = extensionality ( λ (g : Hom A a₁ a ) → ? ) | |
| 221 isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) (CF {a}) F (F2Natmap {a} {F}) | |
| 222 isNTrans1 = record { commute = λ {a₁ b f} → commute {a₁} {b} {f} } | |
| 190 | 223 |
| 224 | |
| 225 Nat2F : {a : Obj A} → {F : Obj SetsAop} → Hom SetsAop (CF {a}) F → FObj F a | |
| 226 Nat2F = {!!} | |
| 227 |