Mercurial > hg > Members > kono > Proof > category
annotate src/yoneda.agda @ 995:1d365952dde4
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 06 Mar 2021 23:02:33 +0900 |
parents | e7848ad0c6f9 |
children | 6cd40df80dec |
rev | line source |
---|---|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
1 --- |
189 | 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 | |
987 | 12 module yoneda { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) where |
178 | 13 |
14 open import HomReasoning | |
15 open import cat-utility | |
179 | 16 open import Relation.Binary.Core |
17 open import Relation.Binary | |
781 | 18 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym ) |
19 | |
179 | 20 |
178 | 21 |
22 -- Contravariant Functor : op A → Sets ( Obj of Sets^{A^op} ) | |
197 | 23 -- Obj and Hom of Sets^A^op |
181 | 24 |
197 | 25 open Functor |
183
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
26 |
987 | 27 YObj : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) |
28 YObj = Functor (Category.op A) (Sets {c₂}) | |
29 YHom : ( f : YObj ) → (g : YObj ) → Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) | |
30 YHom f g = NTrans (Category.op A) (Sets {c₂}) f g | |
184 | 31 |
32 open NTrans | |
987 | 33 Yid : {a : YObj } → YHom a a |
34 Yid {a} = record { TMap = λ a → λ x → x ; isNTrans = isNTrans1 {a} } where | |
35 isNTrans1 : {a : YObj } → IsNTrans (Category.op A) (Sets {c₂}) a a (λ a → λ x → x ) | |
184 | 36 isNTrans1 {a} = record { commute = refl } |
37 | |
987 | 38 _+_ : {a b c : YObj} → YHom b c → YHom a b → YHom a c |
39 _+_ {a} {b} {c} f g = record { TMap = λ x → Sets [ TMap f x o TMap g x ] ; isNTrans = isNTrans1 } where | |
40 commute1 : (a b c : YObj ) (f : YHom b c) (g : YHom a b ) | |
185 | 41 (a₁ b₁ : Obj (Category.op A)) (h : Hom (Category.op A) a₁ b₁) → |
42 Sets [ Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] ≈ | |
43 Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ] | |
44 commute1 a b c f g a₁ b₁ h = let open ≈-Reasoning (Sets {c₂})in begin | |
45 Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] | |
46 ≈⟨ assoc {_} {_} {_} {_} {FMap c h } {TMap f a₁} {TMap g a₁} ⟩ | |
47 Sets [ Sets [ FMap c h o TMap f a₁ ] o TMap g a₁ ] | |
48 ≈⟨ car (nat f) ⟩ | |
49 Sets [ Sets [ TMap f b₁ o FMap b h ] o TMap g a₁ ] | |
50 ≈↑⟨ assoc {_} {_} {_} {_} { TMap f b₁} {FMap b h } {TMap g a₁}⟩ | |
51 Sets [ TMap f b₁ o Sets [ FMap b h o TMap g a₁ ] ] | |
52 ≈⟨ cdr {_} {_} {_} {_} {_} { TMap f b₁} (nat g) ⟩ | |
53 Sets [ TMap f b₁ o Sets [ TMap g b₁ o FMap a h ] ] | |
54 ≈↑⟨ assoc {_} {_} {_} {_} {TMap f b₁} {TMap g b₁} { FMap a h} ⟩ | |
55 Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] | |
56 ∎ | |
57 isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) a c (λ x → Sets [ TMap f x o TMap g x ]) | |
58 isNTrans1 = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h } | |
184 | 59 |
987 | 60 _==_ : {a b : YObj} → YHom a b → YHom a b → Set (c₂ ⊔ c₁) |
61 _==_ f g = ∀{x : Obj (Category.op A)} → (Sets {c₂}) [ TMap f x ≈ TMap g x ] | |
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
62 |
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
63 infix 4 _==_ |
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
64 |
987 | 65 isSetsAop : IsCategory (YObj) (YHom) _==_ _+_ ( Yid ) |
66 isSetsAop = | |
300 | 67 record { isEquivalence = record {refl = refl ; trans = λ {i j k} → trans1 {_} {_} {i} {j} {k} ; sym = λ {i j} → sym1 {_} {_} {i} {j}} |
189 | 68 ; identityL = refl |
69 ; identityR = refl | |
70 ; o-resp-≈ = λ{a b c f g h i } → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} | |
71 ; associative = refl | |
358 | 72 } where |
73 open ≈-Reasoning (Sets {c₂}) | |
987 | 74 sym1 : {a b : YObj } {i j : YHom a b } → i == j → j == i |
358 | 75 sym1 {a} {b} {i} {j} eq {x} = sym eq |
987 | 76 trans1 : {a b : YObj } {i j k : YHom a b} → i == j → j == k → i == k |
358 | 77 trans1 {a} {b} {i} {j} {k} i=j j=k {x} = trans-hom i=j j=k |
987 | 78 o-resp-≈ : {A₁ B C : YObj} {f g : YHom A₁ B} {h i : YHom B C} → |
189 | 79 f == g → h == i → h + f == i + g |
358 | 80 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f=g h=i {x} = resp f=g h=i |
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
81 |
987 | 82 SetsAop : Category (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (c₂ ⊔ c₁) |
83 SetsAop = | |
84 record { Obj = YObj | |
85 ; Hom = YHom | |
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
86 ; _o_ = _+_ |
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
87 ; _≈_ = _==_ |
987 | 88 ; Id = Yid |
89 ; isCategory = isSetsAop | |
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
90 } |
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
91 |
197 | 92 -- A is Locally small |
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
93 postulate ≈-≡ : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y |
197 | 94 |
949
ac53803b3b2a
reorganization for apkg
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
783
diff
changeset
|
95 import Axiom.Extensionality.Propositional |
197 | 96 -- 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 ) |
949
ac53803b3b2a
reorganization for apkg
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
783
diff
changeset
|
97 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ |
197 | 98 |
99 ---- | |
100 -- | |
101 -- Object mapping in Yoneda Functor | |
102 -- | |
103 ---- | |
104 | |
105 open import Function | |
106 | |
987 | 107 y-obj : (a : Obj A) → Functor (Category.op A) (Sets {c₂}) |
108 y-obj a = record { | |
197 | 109 FObj = λ b → Hom (Category.op A) a b ; |
110 FMap = λ {b c : Obj A } → λ ( f : Hom A c b ) → λ (g : Hom A b a ) → (Category.op A) [ f o g ] ; | |
111 isFunctor = record { | |
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
112 identity = λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ; |
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
113 distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ; |
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
114 ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq ) |
197 | 115 } |
116 } where | |
117 lemma-y-obj1 : {b : Obj A } → (x : Hom A b a) → (Category.op A) [ id1 A b o x ] ≡ x | |
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
118 lemma-y-obj1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} idL |
197 | 119 lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A b a₁) (g : Hom A c b ) → (x : Hom A a₁ a )→ |
120 Category.op A [ Category.op A [ g o f ] o x ] ≡ (Sets [ _[_o_] (Category.op A) g o _[_o_] (Category.op A) f ]) x | |
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
121 lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} ( begin |
197 | 122 Category.op A [ Category.op A [ g o f ] o x ] |
123 ≈↑⟨ assoc ⟩ | |
124 Category.op A [ g o Category.op A [ f o x ] ] | |
125 ≈⟨⟩ | |
126 ( λ x → Category.op A [ g o x ] ) ( ( λ x → Category.op A [ f o x ] ) x ) | |
127 ∎ ) | |
128 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 ] | |
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
129 lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} ( begin |
197 | 130 Category.op A [ f o x ] |
131 ≈⟨ resp refl-hom eq ⟩ | |
132 Category.op A [ g o x ] | |
133 ∎ ) | |
134 | |
135 | |
136 ---- | |
137 -- | |
138 -- Hom mapping in Yoneda Functor | |
139 -- | |
140 ---- | |
141 | |
987 | 142 y-tmap : ( a b : Obj A ) → (f : Hom A a b ) → (x : Obj (Category.op A)) → |
143 FObj (y-obj a) x → FObj (y-obj b ) x | |
144 y-tmap a b f x = λ ( g : Hom A x a ) → A [ f o g ] -- ( h : Hom A x b ) | |
197 | 145 |
987 | 146 y-map : {a b : Obj A } → (f : Hom A a b ) → YHom (y-obj a) (y-obj b) |
147 y-map {a} {b} f = record { TMap = y-tmap a b f ; isNTrans = isNTrans1 {a} {b} f } where | |
197 | 148 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 ) → |
987 | 149 Sets [ Sets [ FMap (y-obj b) g o y-tmap a b f a₁ ] ≈ |
150 Sets [ y-tmap a b f b₁ o FMap (y-obj a) g ] ] | |
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
151 lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ {_} {_} {_} {A} ( begin |
197 | 152 A [ A [ f o x ] o g ] |
153 ≈↑⟨ assoc ⟩ | |
154 A [ f o A [ x o g ] ] | |
155 ∎ ) ) | |
987 | 156 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 ) |
197 | 157 isNTrans1 {a} {b} f = record { commute = λ{a₁ b₁ g } → lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f } |
158 | |
159 ----- | |
160 -- | |
161 -- Yoneda Functor itself | |
162 -- | |
163 ----- | |
164 | |
987 | 165 YonedaFunctor : Functor A SetsAop |
166 YonedaFunctor = record { | |
167 FObj = λ a → y-obj a | |
168 ; 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
|
169 ; isFunctor = record { |
187 | 170 identity = identity |
171 ; distr = distr1 | |
172 ; ≈-cong = ≈-cong | |
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
173 |
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
174 } |
187 | 175 } where |
987 | 176 ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop [ y-map f ≈ y-map g ] |
177 ≈-cong {a} {b} {f} {g} eq = let open ≈-Reasoning A in -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [ g o g₁ ] ) | |
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
178 extensionality A ( λ h → ≈-≡ {_} {_} {_} {A} ( begin |
188
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
179 A [ f o h ] |
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
180 ≈⟨ resp refl-hom eq ⟩ |
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
181 A [ g o h ] |
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
182 ∎ |
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
183 ) ) |
987 | 184 identity : {a : Obj A} → SetsAop [ y-map (id1 A a) ≈ id1 SetsAop (y-obj a ) ] |
185 identity {a} = let open ≈-Reasoning A in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x) | |
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
186 extensionality A ( λ g → ≈-≡ {_} {_} {_} {A} ( begin |
188
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
187 A [ id1 A a o g ] |
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
188 ≈⟨ idL ⟩ |
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
189 g |
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
190 ∎ |
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
191 ) ) |
987 | 192 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 ] ] |
193 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₁ ] ] ) | |
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
194 extensionality A ( λ h → ≈-≡ {_} {_} {_} {A} ( begin |
188
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
195 A [ A [ g o f ] o h ] |
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
196 ≈↑⟨ assoc ⟩ |
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
197 A [ g o A [ f o h ] ] |
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
198 ∎ |
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
199 ) ) |
184 | 200 |
185 | 201 |
190 | 202 ------ |
203 -- | |
204 -- F : A → Sets ∈ Obj SetsAop | |
205 -- | |
300 | 206 -- F(a) → Nat(h_a,F) |
191 | 207 -- x ∈ F(a) , (g : Hom A b a) → ( FMap F g ) x |
190 | 208 ------ |
187 | 209 |
987 | 210 F2Natmap : {a : Obj A} → {F : Obj SetsAop } |
211 → {x : FObj F a} → (b : Obj (Category.op A)) → Hom Sets (FObj (y-obj a) b) (FObj F b) | |
212 F2Natmap {a} {F} {x} b = λ ( g : Hom A b a ) → ( FMap F g ) x | |
190 | 213 |
987 | 214 F2Nat : {a : Obj A} → {F : Obj SetsAop } → FObj F a → Hom SetsAop (y-obj a) F |
215 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
|
216 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
|
217 (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
|
218 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
|
219 cong ( λ f → f x ) ( sym ( distr F ) ) |
191 | 220 commute : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} → |
987 | 221 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
|
222 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
|
223 begin |
987 | 224 Sets [ FMap F f o F2Natmap {a} {F} {x} a₁ ] |
192
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
225 ≈⟨⟩ |
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
226 Sets [ FMap F f o (λ ( g : Hom A a₁ a ) → ( FMap F g ) x) ] |
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
227 ≈⟨ extensionality A ( λ (g : Hom A a₁ a) → commute1 {a₁} {b} {f} g ) ⟩ |
987 | 228 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
|
229 ≈⟨⟩ |
987 | 230 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
|
231 ∎ |
987 | 232 isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) (y-obj a) F (F2Natmap {a} {F}) |
191 | 233 isNTrans1 = record { commute = λ {a₁ b f} → commute {a₁} {b} {f} } |
190 | 234 |
235 | |
199 | 236 -- F(a) <- Nat(h_a,F) |
987 | 237 Nat2F : {a : Obj A} → {F : Obj SetsAop } → Hom SetsAop (y-obj a) F → FObj F a |
238 Nat2F {a} {F} ha = ( TMap ha a ) (id1 A a) | |
190 | 239 |
199 | 240 ---- |
241 -- | |
242 -- Prove Bijection (as routine exercise ...) | |
243 -- | |
244 ---- | |
245 | |
987 | 246 F2Nat→Nat2F : {a : Obj A } → {F : Obj SetsAop } → (fa : FObj F a) |
247 → Nat2F {a} {F} (F2Nat {a} {F} fa) ≡ fa | |
248 F2Nat→Nat2F {a} {F} fa = let open ≈-Reasoning (Sets) in cong ( λ f → f fa ) ( | |
199 | 249 -- FMap F (Category.Category.Id A) fa ≡ fa |
194 | 250 begin |
251 ( FMap F (id1 A _ )) | |
252 ≈⟨ IsFunctor.identity (isFunctor F) ⟩ | |
253 id1 Sets (FObj F a) | |
254 ∎ ) | |
255 | |
987 | 256 -- open import Relation.Binary.PropositionalEquality |
194 | 257 |
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
258 ≡-cong = Relation.Binary.PropositionalEquality.cong |
193
4e6f080f0107
isomorphic problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
192
diff
changeset
|
259 |
195 | 260 -- F : op A → Sets |
197 | 261 -- ha : NTrans (op A) Sets (y-obj {a}) F |
262 -- FMap F g o TMap ha a ≈ TMap ha b o FMap (y-obj {a}) g | |
195 | 263 |
987 | 264 Nat2F→F2Nat : {a : Obj A } → {F : Obj SetsAop } → (ha : Hom SetsAop (y-obj a) F) |
265 → SetsAop [ F2Nat {a} {F} (Nat2F {a} {F} ha) ≈ ha ] | |
266 Nat2F→F2Nat {a} {F} ha {b} = let open ≡-Reasoning in | |
194 | 267 begin |
987 | 268 TMap (F2Nat {a} {F} (Nat2F {a} {F} ha)) b |
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
269 ≡⟨⟩ |
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
270 (λ g → FMap F g (TMap ha a (Category.Category.Id A))) |
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
271 ≡⟨ extensionality A (λ g → ( |
195 | 272 begin |
273 FMap F g (TMap ha a (Category.Category.Id A)) | |
203 | 274 ≡⟨ ≡-cong (λ f → f (Category.Category.Id A)) (IsNTrans.commute (isNTrans ha)) ⟩ |
987 | 275 TMap ha b (FMap (y-obj a) g (Category.Category.Id A)) |
195 | 276 ≡⟨⟩ |
277 TMap ha b ( (A Category.o Category.Category.Id A) g ) | |
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
278 ≡⟨ ≡-cong ( TMap ha b ) ( ≈-≡ {_} {_} {_} {A} (IsCategory.identityL ( Category.isCategory A ))) ⟩ |
195 | 279 TMap ha b g |
280 ∎ | |
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
281 )) ⟩ |
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
282 TMap ha b |
195 | 283 ∎ |
194 | 284 |
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
285 -- Yoneda's Lemma |
199 | 286 -- Yoneda Functor is full and faithfull |
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
287 -- that is FMapp Yoneda is injective and surjective |
194 | 288 |
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
289 -- λ b g → (A Category.o f₁) g |
987 | 290 YondaLemma1 : {a a' : Obj A } {f : FObj (FObj YonedaFunctor a) a' } |
291 → SetsAop [ F2Nat {a'} {FObj YonedaFunctor a} f ≈ FMap YonedaFunctor f ] | |
292 YondaLemma1 {a} {a'} {f} = refl | |
293 | |
294 domF : (y : Obj SetsAop) → {x : Obj (Category.op A)} → FObj y x → Obj A | |
295 domF y {x} z = x | |
296 | |
991
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
297 -- |
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
298 -- f onto |
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
299 -- |
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
300 |
989 | 301 YondaLemma2 : {a a' b : Obj A } (f : Hom A a a' ) → NTrans (Category.op A) Sets (FObj YonedaFunctor a) (FObj YonedaFunctor a') |
302 YondaLemma2 f = FMap YonedaFunctor f | |
303 | |
304 YondaLemma3 : {a a' b : Obj A } (f : Hom A a a' ) → Hom A b a → Hom A b a' | |
305 YondaLemma3 {a} {a'} {b} f = TMap (FMap YonedaFunctor f) b | |
306 | |
307 -- YondaLemma4 : {a a' b : Obj A } → (f : Hom A a a' ) → Hom ? (id1 A b) f | |
308 -- YondaLemma4 {a} {a'} {b} f = Hom A b a → Hom A b a' | |
309 | |
991
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
310 -- |
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
311 -- f ∈ FMap (FObj YonedaFunctor a') a |
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
312 -- |
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
313 |
995 | 314 -- g f |
315 -- b --→ a ------→ a' | |
316 -- | | | |
317 -- | | | |
318 -- ↓ ↓ | |
319 -- H a ------→ H a' | |
320 -- H f | |
321 -- | |
989 | 322 _^ : {a a' b : Obj A } → (f : Hom A a a' ) → Hom A b a → Hom A b a' |
323 _^ {a} {a'} {b} f g = (FMap (FObj YonedaFunctor a') g) f | |
324 | |
325 f-unique : {a a' b : Obj A } (f : Hom A a a' ) → f ^ ≡ TMap (FMap YonedaFunctor f) b | |
326 f-unique {a} {a'} {b} f = extensionality A (λ g → begin | |
327 (f ^ ) g ≡⟨⟩ | |
328 (FMap (FObj YonedaFunctor a') g) f ≡⟨⟩ | |
329 A [ f o g ] ≡⟨⟩ | |
330 TMap (FMap YonedaFunctor f) b g ∎ ) where open ≡-Reasoning | |
331 | |
990 | 332 postulate |
333 eqObj0 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a a' b b' : Obj A} → Hom A a b ≡ Hom A a' b' → a ≡ a' | |
334 eqHom0 : {a b c : Obj A } {f f' : Hom A b c } {g g' : Hom A a b } → A [ f o g ] ≡ A [ f' o g' ] → f ≡ f' | |
335 eqHom1 : {a b c : Obj A } {f f' : Hom A b c } {g g' : Hom A a b } → A [ f o g ] ≡ A [ f' o g' ] → g ≡ g' | |
336 -- eqTMap : { y b : Obj A} { x z : Obj Sets} → {g h : NTrans (Category.op A) Sets (y-obj b) ? } {w : {!!} } → TMap g x {!!} ≡ TMap h x w → g ≡ h | |
989 | 337 |
995 | 338 open import Category.Cat |
339 | |
340 | |
341 ≃→a=a : {c₁ c₂ ℓ : Level} (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B } | |
342 → ( f : Hom B a b ) | |
343 → ( g : Hom B a' b' ) | |
344 → [_]_~_ B f g → a ≡ a' | |
345 ≃→a=a B f g (refl eqv) = refl | |
346 | |
347 ≃→b=b : {c₁ c₂ ℓ : Level} (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B } | |
348 → ( f : Hom B a b ) | |
349 → ( g : Hom B a' b' ) | |
350 → [_]_~_ B f g → b ≡ b' | |
351 ≃→b=b B f g (refl eqv) = refl | |
352 | |
353 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_) | |
354 | |
355 eqObj1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a b : Obj A} → Hom A a a ≡ Hom A a b → a ≡ b | |
356 eqObj1 A {a} {b} eq = lem (subst (λ k → k) eq (id1 A a)) eq where | |
357 lem : (f : Hom A a b ) → f ≅ id1 A a → Hom A a a ≡ Hom A a b → a ≡ b | |
358 lem _ HE.refl refl = refl | |
359 | |
989 | 360 -- full (injective ) |
987 | 361 Yoneda-injective : {a b : Obj A } → {x y : Obj SetsAop} → (g h : Hom SetsAop y (FObj YonedaFunctor a)) (f : Hom A a b ) |
362 → SetsAop [ SetsAop [ FMap YonedaFunctor f o g ] ≈ SetsAop [ FMap YonedaFunctor f o h ] ] | |
363 → SetsAop [ g ≈ h ] | |
991
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
364 Yoneda-injective {a} {b} {x} {y} g h f yg=yh = extensionality A (λ z → ≈-≡ ( begin |
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
365 TMap g _ z ≈⟨ {!!} ⟩ |
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
366 A [ id1 A _ o TMap g _ z ] ≈⟨ {!!} ⟩ |
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
367 ( Sets [ id1 Sets _ o TMap g _ ] ) z ≈⟨ {!!} ⟩ |
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
368 TMap h _ z ∎ ) ) where |
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
369 open ≈-Reasoning A |
990 | 370 ylem11 : {x : Obj A} (z : FObj y x) → A [ f o TMap g _ z ] ≡ A [ f o TMap h _ z ] |
371 ylem11 z = (cong (λ k → k z ) yg=yh ) | |
987 | 372 |
989 | 373 -- faithful (surjective) |
987 | 374 Yoneda-surjective : {a b : Obj A } → {x y : Obj SetsAop} → (g h : Hom SetsAop (FObj YonedaFunctor b) y) (f : Hom A a b ) |
375 → SetsAop [ SetsAop [ g o FMap YonedaFunctor f ] ≈ SetsAop [ h o FMap YonedaFunctor f ] ] | |
376 → SetsAop [ g ≈ h ] | |
991
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
377 Yoneda-surjective {a} {b} {x} {y} g h f yg=yh = extensionality A (λ z → ( begin |
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
378 TMap g _ z ≡⟨ {!!} ⟩ |
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
379 TMap g _ (A [ id1 A _ o z ] ) ≡⟨⟩ |
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
380 ( Sets [ TMap g _ o FMap (FObj YonedaFunctor b) z ]) (id1 A _) ≡⟨ {!!} ⟩ |
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
381 TMap g _ (A [ f o A [ {!!} o z ] ] ) ≡⟨ {!!} ⟩ |
990 | 382 ( Sets [ FMap y z o TMap g _ ] ) (id1 A _) ≡⟨ {!!} ⟩ |
991
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
383 TMap h _ z ∎ ) ) where |
990 | 384 open ≡-Reasoning |
991
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
385 ylem12 : {y : Obj A} → { z : Hom A y a } → TMap g y (A [ f o z ]) ≡ TMap h y (A [ f o z ]) |
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
386 ylem12 {y} {z} = cong (λ k → k z ) (yg=yh {y} ) |
990 | 387 ylem10 : {y : Obj A} → (λ z → TMap g y (A [ f o z ])) ≡ (λ z → TMap h y (A [ f o z ] )) |
388 ylem10 = yg=yh | |
989 | 389 |
390 Yoneda-full-embed : {a b : Obj A } → FObj YonedaFunctor a ≡ FObj YonedaFunctor b → a ≡ b | |
990 | 391 Yoneda-full-embed {a} {b} eq = eqObj1 A ylem1 where |
989 | 392 ylem1 : Hom A a a ≡ Hom A a b |
393 ylem1 = cong (λ k → FObj k a) eq | |
195 | 394 |
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
395 -- 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
|
396 |
204 | 397 -- Full embedding of Yoneda Functor requires injective on Object, |
398 -- | |
399 -- But we cannot prove like this | |
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
400 -- FObj YonedaFunctor a ≡ FObj YonedaFunctor b → a ≡ b |
989 | 401 a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B |
402 a1 HE.refl = refl | |
403 | |
783 | 404 |
405 open import Relation.Nullary | |
406 open import Data.Empty | |
407 | |
408 --YondaLemma2 : {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → | |
409 -- (a b x : Obj A ) → (FObj (FObj (YonedaFunctor A) a) x) ≡ (FObj (FObj (YonedaFunctor A) b ) x) → a ≡ b | |
410 --YondaLemma2 A a bx eq = {!!} | |
411 | |
253 | 412 -- N.B = ≡-cong gives you ! a ≡ b, so we cannot cong inv to prove a ≡ b |
783 | 413 |
414 --record Category c₁ c₂ ℓ : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where | |
415 -- infixr 9 _o_ | |
416 -- infix 4 _≈_ | |
417 -- field | |
418 -- Obj : Set c₁ | |
419 -- Hom : Obj → Obj → Set c₂ | |
420 --YondaLemma31 : {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → | |
421 -- (a b x : Obj A ) → Hom A a x ≡ Hom A b x → a ≡ b | |
422 --YondaLemma31 A a b x eq = {!!} | |
204 | 423 -- |
253 | 424 -- Instead we prove only |
204 | 425 -- inv ( FObj YonedaFunctor a ) ≡ a |
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
426 |
987 | 427 inv : {a x : Obj A} ( f : FObj (FObj YonedaFunctor a) x) → Obj A |
428 inv {a} f = Category.cod A f | |
203 | 429 |
987 | 430 YonedaLemma21 : {a x : Obj A} ( f : ( FObj (FObj YonedaFunctor a) x) ) → inv f ≡ a |
431 YonedaLemma21 {a} {x} f = refl | |
783 | 432 |
433 -- YondaLemma3 : {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → | |
434 -- (a b x : Obj A ) → Hom A a x ≅ Hom A b x → a ≡ b | |
435 -- YondaLemma3 A a b x eq = {!!} -- ≡-cong (inv A) ? | |
436 | |
949
ac53803b3b2a
reorganization for apkg
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
783
diff
changeset
|
437 -- a2 : ( a b : Set ) (f : a → a ) (g : b → a ) -> f ≅ g → a ≡ b |
ac53803b3b2a
reorganization for apkg
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
783
diff
changeset
|
438 -- a2 a b f g eq = {!!} |
783 | 439 |
440 -- YonedaInjective : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A} | |
441 -- → FObj (FObj (YonedaFunctor A ) a ) a ≅ FObj (FObj (YonedaFunctor A ) a ) b | |
442 -- → a ≡ b | |
443 -- YonedaInjective A {a} {b} eq = {!!} | |
444 | |
445 |