Mercurial > hg > Members > kono > Proof > category
annotate yoneda.agda @ 198:1edba4226474
comment
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 31 Aug 2013 01:51:38 +0900 |
| parents | ec50ff189f62 |
| children | 0ce7795fa46b |
| 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} ) | |
| 197 | 21 -- Obj and Hom of Sets^A^op |
| 181 | 22 |
| 197 | 23 open Functor |
|
183
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
24 |
| 184 | 25 YObj = Functor (Category.op A) (Sets {c₂}) |
| 26 YHom = λ (f : YObj ) → λ (g : YObj ) → NTrans (Category.op A) Sets f g | |
| 27 | |
| 28 open NTrans | |
| 29 Yid : {a : YObj} → YHom a a | |
| 30 Yid {a} = record { TMap = \a -> \x -> x ; isNTrans = isNTrans1 {a} } where | |
| 31 isNTrans1 : {a : YObj } → IsNTrans (Category.op A) (Sets {c₂}) a a (\a -> \x -> x ) | |
| 32 isNTrans1 {a} = record { commute = refl } | |
| 33 | |
| 34 _+_ : {a b c : YObj} → YHom b c → YHom a b → YHom a c | |
| 185 | 35 _+_{a} {b} {c} f g = record { TMap = λ x → Sets [ TMap f x o TMap g x ] ; isNTrans = isNTrans1 } where |
| 36 commute1 : (a b c : YObj ) (f : YHom b c) (g : YHom a b ) | |
| 37 (a₁ b₁ : Obj (Category.op A)) (h : Hom (Category.op A) a₁ b₁) → | |
| 38 Sets [ Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] ≈ | |
| 39 Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ] | |
| 40 commute1 a b c f g a₁ b₁ h = let open ≈-Reasoning (Sets {c₂})in begin | |
| 41 Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] | |
| 42 ≈⟨ assoc {_} {_} {_} {_} {FMap c h } {TMap f a₁} {TMap g a₁} ⟩ | |
| 43 Sets [ Sets [ FMap c h o TMap f a₁ ] o TMap g a₁ ] | |
| 44 ≈⟨ car (nat f) ⟩ | |
| 45 Sets [ Sets [ TMap f b₁ o FMap b h ] o TMap g a₁ ] | |
| 46 ≈↑⟨ assoc {_} {_} {_} {_} { TMap f b₁} {FMap b h } {TMap g a₁}⟩ | |
| 47 Sets [ TMap f b₁ o Sets [ FMap b h o TMap g a₁ ] ] | |
| 48 ≈⟨ cdr {_} {_} {_} {_} {_} { TMap f b₁} (nat g) ⟩ | |
| 49 Sets [ TMap f b₁ o Sets [ TMap g b₁ o FMap a h ] ] | |
| 50 ≈↑⟨ assoc {_} {_} {_} {_} {TMap f b₁} {TMap g b₁} { FMap a h} ⟩ | |
| 51 Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] | |
| 52 ∎ | |
| 53 isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) a c (λ x → Sets [ TMap f x o TMap g x ]) | |
| 54 isNTrans1 = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h } | |
| 184 | 55 |
|
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
56 _==_ : {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
|
57 _==_ 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
|
58 |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
59 infix 4 _==_ |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
60 |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
61 isSetsAop : IsCategory YObj YHom _==_ _+_ Yid |
| 189 | 62 isSetsAop = |
| 63 record { isEquivalence = record {refl = refl ; trans = ≡-trans ; sym = ≡-sym} | |
| 64 ; identityL = refl | |
| 65 ; identityR = refl | |
| 66 ; o-resp-≈ = λ{a b c f g h i } → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} | |
| 67 ; associative = refl | |
| 68 } where | |
| 69 o-resp-≈ : {A₁ B C : YObj} {f g : YHom A₁ B} {h i : YHom B C} → | |
| 70 f == g → h == i → h + f == i + g | |
| 71 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
|
72 |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
73 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
|
74 SetsAop = |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
75 record { Obj = YObj |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
76 ; Hom = YHom |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
77 ; _o_ = _+_ |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
78 ; _≈_ = _==_ |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
79 ; Id = Yid |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
80 ; isCategory = isSetsAop |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
81 } |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
82 |
| 197 | 83 -- A is Locally small |
| 84 postulate ≈-≡ : {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y | |
| 85 | |
| 86 import Relation.Binary.PropositionalEquality | |
| 87 -- 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 ) | |
| 88 postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ | |
| 89 | |
| 90 -- non cotravariant version | |
| 91 | |
| 92 y-obj' : (a : Obj A) → Functor A Sets | |
| 93 y-obj' a = record { | |
| 94 FObj = λ b → Hom A a b | |
| 95 ; FMap = λ {b c : Obj A } → λ ( f : Hom A b c ) → λ (g : Hom A a b ) → A [ f o g ] | |
| 96 ; isFunctor = record { | |
| 97 identity = identity | |
| 98 ; distr = λ {a} {b} {c} {f} {g} → distr1 a b c f g | |
| 99 ; ≈-cong = cong1 | |
| 100 } | |
| 101 } where | |
| 102 lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x | |
| 103 lemma-y-obj1 {b} x = let open ≈-Reasoning (A) in ≈-≡ idL | |
| 104 identity : {b : Obj A} → Sets [ (λ (g : Hom A a b ) → A [ id1 A b o g ]) ≈ ( λ g → g ) ] | |
| 105 identity {b} = extensionality lemma-y-obj1 | |
| 106 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 | |
| 107 lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (A) in ≈-≡ ( begin | |
| 108 A [ A [ g o f ] o x ] | |
| 109 ≈↑⟨ assoc ⟩ | |
| 110 A [ g o A [ f o x ] ] | |
| 111 ≈⟨⟩ | |
| 112 ( λ x → A [ g o x ] ) ( ( λ x → A [ f o x ] ) x ) | |
| 113 ∎ ) | |
| 114 distr1 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c) → | |
| 115 Sets [ (λ g₁ → A [ A [ g o f ] o g₁ ]) ≈ Sets [ (λ g₁ → A [ g o g₁ ]) o (λ g₁ → A [ f o g₁ ]) ] ] | |
| 116 distr1 a b c f g = extensionality ( λ x → lemma-y-obj2 a b c f g x ) | |
| 117 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₁ ]) ] | |
| 118 cong1 eq = extensionality ( λ x → ( ≈-≡ ( | |
| 119 (IsCategory.o-resp-≈ ( Category.isCategory A )) ( IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A ))) eq ))) | |
| 120 | |
| 121 ---- | |
| 122 -- | |
| 123 -- Object mapping in Yoneda Functor | |
| 124 -- | |
| 125 ---- | |
| 126 | |
| 127 open import Function | |
| 128 | |
| 129 y-obj : (a : Obj A) → Functor (Category.op A) (Sets {c₂}) | |
| 130 y-obj a = record { | |
| 131 FObj = λ b → Hom (Category.op A) a b ; | |
| 132 FMap = λ {b c : Obj A } → λ ( f : Hom A c b ) → λ (g : Hom A b a ) → (Category.op A) [ f o g ] ; | |
| 133 isFunctor = record { | |
| 134 identity = \{b} → extensionality ( λ x → lemma-y-obj1 {b} x ) ; | |
| 135 distr = λ {a} {b} {c} {f} {g} → extensionality ( λ x → lemma-y-obj2 a b c f g x ) ; | |
| 136 ≈-cong = λ eq → extensionality ( λ x → lemma-y-obj3 x eq ) | |
| 137 } | |
| 138 } where | |
| 139 lemma-y-obj1 : {b : Obj A } → (x : Hom A b a) → (Category.op A) [ id1 A b o x ] ≡ x | |
| 140 lemma-y-obj1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ idL | |
| 141 lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A b a₁) (g : Hom A c b ) → (x : Hom A a₁ a )→ | |
| 142 Category.op A [ Category.op A [ g o f ] o x ] ≡ (Sets [ _[_o_] (Category.op A) g o _[_o_] (Category.op A) f ]) x | |
| 143 lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≈-≡ ( begin | |
| 144 Category.op A [ Category.op A [ g o f ] o x ] | |
| 145 ≈↑⟨ assoc ⟩ | |
| 146 Category.op A [ g o Category.op A [ f o x ] ] | |
| 147 ≈⟨⟩ | |
| 148 ( λ x → Category.op A [ g o x ] ) ( ( λ x → Category.op A [ f o x ] ) x ) | |
| 149 ∎ ) | |
| 150 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 ] | |
| 151 lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning (Category.op A) in ≈-≡ ( begin | |
| 152 Category.op A [ f o x ] | |
| 153 ≈⟨ resp refl-hom eq ⟩ | |
| 154 Category.op A [ g o x ] | |
| 155 ∎ ) | |
| 156 | |
| 157 | |
| 158 ---- | |
| 159 -- | |
| 160 -- Hom mapping in Yoneda Functor | |
| 161 -- | |
| 162 ---- | |
| 163 | |
| 164 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 | |
| 165 y-tmap a b f x = λ ( g : Hom A x a ) → A [ f o g ] -- ( h : Hom A x b ) | |
| 166 | |
| 167 y-map : {a b : Obj A } → (f : Hom A a b ) → YHom (y-obj a) (y-obj b) | |
| 168 y-map {a} {b} f = record { TMap = y-tmap a b f ; isNTrans = isNTrans1 {a} {b} f } where | |
| 169 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 ) → | |
| 170 Sets [ Sets [ FMap (y-obj b) g o y-tmap a b f a₁ ] ≈ | |
| 171 Sets [ y-tmap a b f b₁ o FMap (y-obj a) g ] ] | |
| 172 lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality ( λ x → ≈-≡ ( begin | |
| 173 A [ A [ f o x ] o g ] | |
| 174 ≈↑⟨ assoc ⟩ | |
| 175 A [ f o A [ x o g ] ] | |
| 176 ∎ ) ) | |
| 177 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 ) | |
| 178 isNTrans1 {a} {b} f = record { commute = λ{a₁ b₁ g } → lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f } | |
| 179 | |
|
188
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
180 postulate extensionality1 : Relation.Binary.PropositionalEquality.Extensionality c₁ c₂ |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
181 |
| 197 | 182 ----- |
| 183 -- | |
| 184 -- Yoneda Functor itself | |
| 185 -- | |
| 186 ----- | |
| 187 | |
|
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
188 YonedaFunctor : Functor A SetsAop |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
189 YonedaFunctor = record { |
| 197 | 190 FObj = λ a → y-obj a |
| 191 ; FMap = λ f → y-map f | |
|
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
192 ; isFunctor = record { |
| 187 | 193 identity = identity |
| 194 ; distr = distr1 | |
| 195 ; ≈-cong = ≈-cong | |
|
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
196 |
|
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
197 } |
| 187 | 198 } where |
| 197 | 199 ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop [ y-map f ≈ y-map g ] |
|
188
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
200 ≈-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
|
201 extensionality1 ( λ x → extensionality ( |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
202 λ h → ≈-≡ ( begin |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
203 A [ f o h ] |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
204 ≈⟨ resp refl-hom eq ⟩ |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
205 A [ g o h ] |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
206 ∎ |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
207 ) ) ) |
| 197 | 208 identity : {a : Obj A} → SetsAop [ y-map (id1 A a) ≈ id1 SetsAop (y-obj a ) ] |
|
188
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
209 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
|
210 extensionality1 ( λ x → extensionality ( |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
211 λ g → ≈-≡ ( begin |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
212 A [ id1 A a o g ] |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
213 ≈⟨ idL ⟩ |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
214 g |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
215 ∎ |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
216 ) ) ) |
| 197 | 217 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 ] ] |
| 191 | 218 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
|
219 extensionality1 ( λ x → extensionality ( |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
220 λ h → ≈-≡ ( begin |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
221 A [ A [ g o f ] o h ] |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
222 ≈↑⟨ assoc ⟩ |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
223 A [ g o A [ f o h ] ] |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
224 ∎ |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
225 ) ) ) |
| 184 | 226 |
| 185 | 227 |
| 190 | 228 ------ |
| 229 -- | |
| 230 -- F : A → Sets ∈ Obj SetsAop | |
| 231 -- | |
| 232 -- F(a) ⇔ Nat(h_a,F) | |
| 191 | 233 -- x ∈ F(a) , (g : Hom A b a) → ( FMap F g ) x |
| 190 | 234 ------ |
| 187 | 235 |
| 197 | 236 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) |
| 191 | 237 F2Natmap {a} {F} {x} b = λ ( g : Hom A b a ) → ( FMap F g ) x |
| 190 | 238 |
| 197 | 239 F2Nat : {a : Obj A} → {F : Obj SetsAop} → FObj F a → Hom SetsAop (y-obj a) F |
| 191 | 240 F2Nat {a} {F} x = record { TMap = F2Natmap {a} {F} {x} ; isNTrans = isNTrans1 } where |
|
192
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
241 commute1 : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} (g : Hom A a₁ a) → |
|
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
242 (Sets [ FMap F f o FMap F g ]) x ≡ FMap F (A [ g o f ] ) x |
|
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
243 commute1 g = let open ≈-Reasoning (Sets) in |
|
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
244 cong ( λ f → f x ) ( sym ( distr F ) ) |
| 191 | 245 commute : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} → |
| 197 | 246 Sets [ Sets [ FMap F f o F2Natmap {a} {F} {x} a₁ ] ≈ Sets [ F2Natmap {a} {F} {x} b o FMap (y-obj a) f ] ] |
|
192
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
247 commute {a₁} {b} {f} = let open ≈-Reasoning (Sets) in |
|
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
248 begin |
|
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
249 Sets [ FMap F f o F2Natmap {a} {F} {x} a₁ ] |
|
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
250 ≈⟨⟩ |
|
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
251 Sets [ FMap F f o (λ ( g : Hom A a₁ a ) → ( FMap F g ) x) ] |
|
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
252 ≈⟨ extensionality ( λ (g : Hom A a₁ a) → commute1 {a₁} {b} {f} g ) ⟩ |
| 197 | 253 Sets [ (λ ( g : Hom A b a ) → ( FMap F g ) x) o FMap (y-obj a) f ] |
|
192
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
254 ≈⟨⟩ |
| 197 | 255 Sets [ F2Natmap {a} {F} {x} b o FMap (y-obj a) f ] |
|
192
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
256 ∎ |
| 197 | 257 isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) (y-obj a) F (F2Natmap {a} {F}) |
| 191 | 258 isNTrans1 = record { commute = λ {a₁ b f} → commute {a₁} {b} {f} } |
| 190 | 259 |
| 260 | |
| 197 | 261 Nat2F : {a : Obj A} → {F : Obj SetsAop} → Hom SetsAop (y-obj a) F → FObj F a |
|
193
4e6f080f0107
isomorphic problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
192
diff
changeset
|
262 Nat2F {a} {F} ha = ( TMap ha a ) (id1 A a) |
| 190 | 263 |
|
193
4e6f080f0107
isomorphic problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
192
diff
changeset
|
264 F2Nat→Nat2F : {a : Obj A } → {F : Obj SetsAop} → (fa : FObj F a) → Nat2F {a} {F} (F2Nat {a} {F} fa) ≡ fa |
| 194 | 265 -- FMap F (Category.Category.Id A) fa ≡ fa |
| 266 F2Nat→Nat2F {a} {F} fa = let open ≈-Reasoning (Sets) in cong ( λ f → f fa ) ( | |
| 267 begin | |
| 268 ( FMap F (id1 A _ )) | |
| 269 ≈⟨ IsFunctor.identity (isFunctor F) ⟩ | |
| 270 id1 Sets (FObj F a) | |
| 271 ∎ ) | |
| 272 | |
| 273 open import Relation.Binary.PropositionalEquality | |
| 274 | |
| 275 postulate extensionality2 : Relation.Binary.PropositionalEquality.Extensionality c₁ c₂ | |
| 276 postulate extensionality3 : Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ | |
|
193
4e6f080f0107
isomorphic problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
192
diff
changeset
|
277 |
| 195 | 278 -- F : op A → Sets |
| 197 | 279 -- ha : NTrans (op A) Sets (y-obj {a}) F |
| 280 -- FMap F g o TMap ha a ≈ TMap ha b o FMap (y-obj {a}) g | |
| 195 | 281 |
| 197 | 282 Nat2F→F2Nat : {a : Obj A } → {F : Obj SetsAop} → (ha : Hom SetsAop (y-obj a) F) → SetsAop [ F2Nat {a} {F} (Nat2F {a} {F} ha) ≈ ha ] |
| 194 | 283 Nat2F→F2Nat {a} {F} ha = let open ≡-Reasoning in |
| 284 begin | |
| 285 ( λ (b : Obj A ) → λ (g : Hom A b a ) → FMap F g (TMap ha a (Category.Category.Id A)) ) | |
| 195 | 286 ≡⟨ extensionality2 ( λ b → extensionality3 (λ g → ( |
| 287 begin | |
| 288 FMap F g (TMap ha a (Category.Category.Id A)) | |
| 289 ≡⟨ Relation.Binary.PropositionalEquality.cong (λ f → f (Category.Category.Id A)) (IsNTrans.commute (isNTrans ha)) ⟩ | |
| 197 | 290 TMap ha b (FMap (y-obj a) g (Category.Category.Id A)) |
| 195 | 291 ≡⟨⟩ |
| 292 TMap ha b ( (A Category.o Category.Category.Id A) g ) | |
| 293 ≡⟨ Relation.Binary.PropositionalEquality.cong ( TMap ha b ) ( ≈-≡ (IsCategory.identityL ( Category.isCategory A ))) ⟩ | |
| 294 TMap ha b g | |
| 295 ∎ | |
| 296 ))) ⟩ | |
| 194 | 297 TMap ha |
| 195 | 298 ∎ |
| 194 | 299 |
|
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
300 -- Yoneda's Lemma |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
301 -- full and faithfull |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
302 -- that is FMapp Yoneda is injective and surjective |
| 194 | 303 |
|
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
304 -- λ b g → (A Category.o f₁) g |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
305 YondaLemma1 : {a a' : Obj A } {f : FObj (FObj YonedaFunctor a) a' } → SetsAop [ F2Nat {a'} {FObj YonedaFunctor a} f ≈ FMap YonedaFunctor f ] |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
306 YondaLemma1 {a} {a'} {f} = refl |
| 195 | 307 |
|
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
308 -- F2Nat is bijection so FMap YonedaFunctor also ( using functional extensionality ) |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
309 |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
310 -- Full embedding requires injective on Object, that is |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
311 -- FObj YonedaFunctor a ≡ FObj YonedaFunctor b → a ≡ b |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
312 |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
313 dom-equivalence : {a b : Obj A} → {f g : Hom A a b} → A [ f ≈ g ] → Category.dom A f ≡ Category.dom A g |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
314 dom-equivalence eq = refl |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
315 |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
316 equive-elm : ∀{n} {a b : Set n} → (f : a ) → a ≡ b → b |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
317 equive-elm f refl = f |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
318 |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
319 equive-arrow : {a b : Obj A } → (f : Hom A a b ) → Hom A a b ≡ Hom A a a → Hom A a a |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
320 equive-arrow f eq = equive-elm f eq |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
321 |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
322 -- equive-hom : {a b : Obj A } → {f : Hom A a b } → Hom A a b ≡ Hom A a a → a ≡ b |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
323 -- equive-hom {a} {b} {f} eq = {!!} |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
324 |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
325 -- YondaLemma2 : {a b : Obj A } → (λ x → FObj (FObj YonedaFunctor a) x) ≡ (λ x → FObj (FObj YonedaFunctor b ) x) → |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
326 -- {f : Hom A a b } → a ≡ b |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
327 -- YondaLemma2 {a} {b} eq {f} = {!!} eq |
| 198 | 328 -- I cannot prove this, sorry |