Mercurial > hg > Members > kono > Proof > category
annotate src/yoneda.agda @ 1028:28569574e3cf
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 30 Mar 2021 15:20:08 +0900 |
| parents | e7b0db851a70 |
| children | 40c39d3e6a75 |
| 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 | |
| 996 | 12 open import cat-utility |
| 13 module yoneda { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (I : Set c₁) ( small : Small A I ) where | |
| 178 | 14 |
| 15 open import HomReasoning | |
| 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 |
| 996 | 26 open NTrans |
| 184 | 27 |
| 996 | 28 SetsAop : Category (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (c₂ ⊔ c₁) |
| 29 SetsAop = record { Obj = YObj | |
| 30 ; Hom = YHom | |
| 31 ; _o_ = _+_ | |
| 32 ; _≈_ = _==_ | |
| 33 ; Id = Yid | |
| 34 ; isCategory = record { | |
| 35 isEquivalence = record {refl = refl ; trans = λ {i} {j} {k} → trans1 {_} {_} {i} {j} {k} ; sym = λ {i j} → sym1 {_} {_} {i} {j}} | |
| 36 ; identityL = refl | |
| 37 ; identityR = refl | |
| 38 ; o-resp-≈ = λ{a b c f g h i } → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} | |
| 39 ; associative = refl | |
| 40 } } where | |
| 41 open ≈-Reasoning (Sets {c₂}) | |
| 42 YObj : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) | |
| 43 YObj = Functor (Category.op A) (Sets {c₂}) | |
| 44 YHom : ( f : YObj ) → (g : YObj ) → Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) | |
| 45 YHom f g = NTrans (Category.op A) (Sets {c₂}) f g | |
| 184 | 46 |
| 996 | 47 Yid : {a : YObj } → YHom a a |
| 48 Yid {a} = record { TMap = λ a → λ x → x ; isNTrans = isNTrans1 {a} } where | |
| 49 isNTrans1 : {a : YObj } → IsNTrans (Category.op A) (Sets {c₂}) a a (λ a → λ x → x ) | |
| 50 isNTrans1 {a} = record { commute = refl } | |
| 184 | 51 |
| 996 | 52 _+_ : {a b c : YObj} → YHom b c → YHom a b → YHom a c |
| 53 _+_ {a} {b} {c} f g = | |
| 54 record { TMap = λ x → Sets [ TMap f x o TMap g x ] ; | |
| 55 isNTrans = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h } } where | |
| 56 commute1 : (a b c : YObj ) (f : YHom b c) (g : YHom a b ) | |
| 57 (a₁ b₁ : Obj (Category.op A)) (h : Hom (Category.op A) a₁ b₁) → | |
| 58 Sets [ Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] ≈ | |
| 59 Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ] | |
| 60 commute1 a b c f g a₁ b₁ h = begin | |
| 61 Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] ≈⟨ assoc {_} {_} {_} {_} {FMap c h } {TMap f a₁} {TMap g a₁} ⟩ | |
| 62 Sets [ Sets [ FMap c h o TMap f a₁ ] o TMap g a₁ ] ≈⟨ car (nat f) ⟩ | |
| 63 Sets [ Sets [ TMap f b₁ o FMap b h ] o TMap g a₁ ] ≈↑⟨ assoc {_} {_} {_} {_} { TMap f b₁} {FMap b h } {TMap g a₁}⟩ | |
| 64 Sets [ TMap f b₁ o Sets [ FMap b h o TMap g a₁ ] ] ≈⟨ cdr {_} {_} {_} {_} {_} { TMap f b₁} (nat g) ⟩ | |
| 65 Sets [ TMap f b₁ o Sets [ TMap g b₁ o FMap a h ] ] ≈↑⟨ assoc {_} {_} {_} {_} {TMap f b₁} {TMap g b₁} { FMap a h} ⟩ | |
| 66 Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ∎ | |
|
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
67 |
| 996 | 68 _==_ : {a b : YObj} → YHom a b → YHom a b → Set (c₂ ⊔ c₁) |
| 69 _==_ f g = ∀{x : Obj (Category.op A)} → (Sets {c₂}) [ TMap f x ≈ TMap g x ] | |
| 70 | |
| 987 | 71 sym1 : {a b : YObj } {i j : YHom a b } → i == j → j == i |
| 358 | 72 sym1 {a} {b} {i} {j} eq {x} = sym eq |
| 987 | 73 trans1 : {a b : YObj } {i j k : YHom a b} → i == j → j == k → i == k |
| 358 | 74 trans1 {a} {b} {i} {j} {k} i=j j=k {x} = trans-hom i=j j=k |
| 987 | 75 o-resp-≈ : {A₁ B C : YObj} {f g : YHom A₁ B} {h i : YHom B C} → |
| 996 | 76 f == g → h == i → (h + f) == (i + g) |
| 358 | 77 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
|
78 |
| 197 | 79 -- A is Locally small |
| 996 | 80 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 | 81 |
|
949
ac53803b3b2a
reorganization for apkg
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
783
diff
changeset
|
82 import Axiom.Extensionality.Propositional |
| 197 | 83 -- 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
|
84 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ |
| 197 | 85 |
| 86 ---- | |
| 87 -- | |
| 88 -- Object mapping in Yoneda Functor | |
| 89 -- | |
| 90 ---- | |
| 91 | |
| 92 open import Function | |
| 93 | |
| 987 | 94 y-obj : (a : Obj A) → Functor (Category.op A) (Sets {c₂}) |
| 95 y-obj a = record { | |
| 197 | 96 FObj = λ b → Hom (Category.op A) a b ; |
| 97 FMap = λ {b c : Obj A } → λ ( f : Hom A c b ) → λ (g : Hom A b a ) → (Category.op A) [ f o g ] ; | |
| 98 isFunctor = record { | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
99 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
|
100 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
|
101 ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq ) |
| 197 | 102 } |
| 103 } where | |
| 104 lemma-y-obj1 : {b : Obj A } → (x : Hom A b a) → (Category.op A) [ id1 A b o x ] ≡ x | |
| 996 | 105 lemma-y-obj1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ A idL |
| 197 | 106 lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A b a₁) (g : Hom A c b ) → (x : Hom A a₁ a )→ |
| 107 Category.op A [ Category.op A [ g o f ] o x ] ≡ (Sets [ _[_o_] (Category.op A) g o _[_o_] (Category.op A) f ]) x | |
| 996 | 108 lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≈-≡ A ( begin |
| 109 Category.op A [ Category.op A [ g o f ] o x ] ≈↑⟨ assoc ⟩ | |
| 110 Category.op A [ g o Category.op A [ f o x ] ] ≈⟨⟩ | |
| 111 ( λ x → Category.op A [ g o x ] ) ( ( λ x → Category.op A [ f o x ] ) x ) ∎ ) | |
| 197 | 112 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 ] |
| 996 | 113 lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning (Category.op A) in ≈-≡ A ( begin |
| 114 Category.op A [ f o x ] ≈⟨ resp refl-hom eq ⟩ | |
| 115 Category.op A [ g o x ] ∎ ) | |
| 197 | 116 |
| 117 ---- | |
| 118 -- | |
| 119 -- Hom mapping in Yoneda Functor | |
| 120 -- | |
| 121 ---- | |
| 122 | |
| 987 | 123 y-tmap : ( a b : Obj A ) → (f : Hom A a b ) → (x : Obj (Category.op A)) → |
| 124 FObj (y-obj a) x → FObj (y-obj b ) x | |
| 125 y-tmap a b f x = λ ( g : Hom A x a ) → A [ f o g ] -- ( h : Hom A x b ) | |
| 197 | 126 |
| 996 | 127 y-map : {a b : Obj A } → (f : Hom A a b ) → NTrans (Category.op A) (Sets {c₂}) (y-obj a) (y-obj b) |
| 987 | 128 y-map {a} {b} f = record { TMap = y-tmap a b f ; isNTrans = isNTrans1 {a} {b} f } where |
| 197 | 129 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 | 130 Sets [ Sets [ FMap (y-obj b) g o y-tmap a b f a₁ ] ≈ |
| 131 Sets [ y-tmap a b f b₁ o FMap (y-obj a) g ] ] | |
| 996 | 132 lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin |
| 133 A [ A [ f o x ] o g ] ≈↑⟨ assoc ⟩ | |
| 134 A [ f o A [ x o g ] ] ∎ ) ) | |
| 987 | 135 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 | 136 isNTrans1 {a} {b} f = record { commute = λ{a₁ b₁ g } → lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f } |
| 137 | |
| 138 ----- | |
| 139 -- | |
| 140 -- Yoneda Functor itself | |
| 141 -- | |
| 142 ----- | |
| 143 | |
| 987 | 144 YonedaFunctor : Functor A SetsAop |
| 145 YonedaFunctor = record { | |
| 146 FObj = λ a → y-obj a | |
| 147 ; 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
|
148 ; isFunctor = record { |
| 187 | 149 identity = identity |
| 150 ; distr = distr1 | |
| 151 ; ≈-cong = ≈-cong | |
| 996 | 152 } } where |
| 987 | 153 ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop [ y-map f ≈ y-map g ] |
| 154 ≈-cong {a} {b} {f} {g} eq = let open ≈-Reasoning A in -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [ g o g₁ ] ) | |
| 996 | 155 extensionality A ( λ h → ≈-≡ A ( begin |
| 156 A [ f o h ] ≈⟨ resp refl-hom eq ⟩ | |
| 157 A [ g o h ] ∎ ) ) | |
| 987 | 158 identity : {a : Obj A} → SetsAop [ y-map (id1 A a) ≈ id1 SetsAop (y-obj a ) ] |
| 159 identity {a} = let open ≈-Reasoning A in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x) | |
| 996 | 160 extensionality A ( λ g → ≈-≡ A ( begin |
| 161 A [ id1 A a o g ] ≈⟨ idL ⟩ | |
| 162 g ∎ ) ) | |
| 987 | 163 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 ] ] |
| 164 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₁ ] ] ) | |
| 996 | 165 extensionality A ( λ h → ≈-≡ A ( begin |
| 166 A [ A [ g o f ] o h ] ≈↑⟨ assoc ⟩ | |
| 167 A [ g o A [ f o h ] ] ∎ ) ) | |
| 185 | 168 |
| 190 | 169 ------ |
| 170 -- | |
| 996 | 171 -- Hom(_ , _) : Obj (op A) → Obj A → Sets |
| 172 -- | |
| 173 -- | |
| 174 ------ | |
| 175 | |
| 176 -- module _ where | |
| 177 -- | |
| 178 -- open import Category.Constructions.Product | |
| 179 -- open import Data.Product renaming (_×_ to _*_) | |
| 180 -- | |
| 181 -- HomAAop : Functor ((Category.op A) × A) (Sets {c₂}) | |
| 182 -- HomAAop = record { | |
| 183 -- FObj = λ x → Hom A (proj₁ x) (proj₂ x) | |
| 184 -- -- f : Hom (Category.op A × A) A₁ B | |
| 185 -- -- g : Category.Category.Hom A (proj₁ A₁) (proj₂ A₁) | |
| 186 -- ; FMap = λ f g → A [ A [ proj₂ f o g ] o proj₁ f ] | |
| 187 -- ; isFunctor = record { ≈-cong = λ {a} {b} {f} {g} f=g → extensionality A ( λ h → cong (λ k → A [ A [ proj₂ k o h ] o (proj₁ k) ] ) {!!}) | |
| 188 -- ; distr = {!!} ; identity = {!!} } | |
| 189 -- } where open ≈-Reasoning A | |
| 190 | |
| 191 ------ | |
| 192 -- | |
| 193 -- Yoneda Lemma | |
| 194 -- | |
| 195 -- (F : Obj SetsAop) → ( | |
| 196 -- Hom SetsAop (FObj YonedaFunctor a , F ) ≅ FObj F a | |
| 197 -- | |
| 198 -- F : Functor (co A) Sets ∈ Obj SetsAop | |
| 190 | 199 -- |
| 300 | 200 -- F(a) → Nat(h_a,F) |
| 191 | 201 -- x ∈ F(a) , (g : Hom A b a) → ( FMap F g ) x |
| 190 | 202 ------ |
| 187 | 203 |
| 987 | 204 F2Natmap : {a : Obj A} → {F : Obj SetsAop } |
| 205 → {x : FObj F a} → (b : Obj (Category.op A)) → Hom Sets (FObj (y-obj a) b) (FObj F b) | |
| 206 F2Natmap {a} {F} {x} b = λ ( g : Hom A b a ) → ( FMap F g ) x | |
| 190 | 207 |
| 987 | 208 F2Nat : {a : Obj A} → {F : Obj SetsAop } → FObj F a → Hom SetsAop (y-obj a) F |
| 209 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
|
210 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
|
211 (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
|
212 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
|
213 cong ( λ f → f x ) ( sym ( distr F ) ) |
| 191 | 214 commute : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} → |
| 987 | 215 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
|
216 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
|
217 begin |
| 987 | 218 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
|
219 ≈⟨⟩ |
|
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
220 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
|
221 ≈⟨ extensionality A ( λ (g : Hom A a₁ a) → commute1 {a₁} {b} {f} g ) ⟩ |
| 987 | 222 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
|
223 ≈⟨⟩ |
| 987 | 224 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
|
225 ∎ |
| 987 | 226 isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) (y-obj a) F (F2Natmap {a} {F}) |
| 191 | 227 isNTrans1 = record { commute = λ {a₁ b f} → commute {a₁} {b} {f} } |
| 190 | 228 |
|
1000
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
229 -- |
|
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
230 -- Obj Part : SetAop (Y - , F) ≅ F |
|
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
231 -- |
| 190 | 232 |
| 199 | 233 -- F(a) <- Nat(h_a,F) |
| 987 | 234 Nat2F : {a : Obj A} → {F : Obj SetsAop } → Hom SetsAop (y-obj a) F → FObj F a |
| 235 Nat2F {a} {F} ha = ( TMap ha a ) (id1 A a) | |
| 190 | 236 |
| 199 | 237 ---- |
| 238 -- | |
| 239 -- Prove Bijection (as routine exercise ...) | |
| 240 -- | |
| 241 ---- | |
| 242 | |
| 987 | 243 F2Nat→Nat2F : {a : Obj A } → {F : Obj SetsAop } → (fa : FObj F a) |
| 244 → Nat2F {a} {F} (F2Nat {a} {F} fa) ≡ fa | |
| 245 F2Nat→Nat2F {a} {F} fa = let open ≈-Reasoning (Sets) in cong ( λ f → f fa ) ( | |
| 199 | 246 -- FMap F (Category.Category.Id A) fa ≡ fa |
| 194 | 247 begin |
| 248 ( FMap F (id1 A _ )) | |
| 249 ≈⟨ IsFunctor.identity (isFunctor F) ⟩ | |
| 250 id1 Sets (FObj F a) | |
| 251 ∎ ) | |
| 252 | |
|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
253 ≡-cong = Relation.Binary.PropositionalEquality.cong |
|
193
4e6f080f0107
isomorphic problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
192
diff
changeset
|
254 |
| 197 | 255 -- ha : NTrans (op A) Sets (y-obj {a}) F |
| 256 -- FMap F g o TMap ha a ≈ TMap ha b o FMap (y-obj {a}) g | |
| 987 | 257 Nat2F→F2Nat : {a : Obj A } → {F : Obj SetsAop } → (ha : Hom SetsAop (y-obj a) F) |
| 258 → SetsAop [ F2Nat {a} {F} (Nat2F {a} {F} ha) ≈ ha ] | |
| 996 | 259 Nat2F→F2Nat {a} {F} ha {b} = let open ≡-Reasoning in begin |
| 260 TMap (F2Nat {a} {F} (Nat2F {a} {F} ha)) b ≡⟨⟩ | |
| 261 (λ g → FMap F g (TMap ha a (id1 A _))) ≡⟨ extensionality A (λ g → ( begin | |
| 262 FMap F g (TMap ha a (id1 A _)) ≡⟨ ≡-cong (λ f → f (id1 A _)) (IsNTrans.commute (isNTrans ha)) ⟩ | |
| 263 TMap ha b (FMap (y-obj a) g (id1 A _)) ≡⟨⟩ | |
| 264 TMap ha b ( A [ id1 A _ o g ] ) ≡⟨ ≡-cong ( TMap ha b ) ( ≈-≡ A (≈-Reasoning.idL A)) ⟩ | |
| 265 TMap ha b g ∎ )) ⟩ | |
| 266 TMap ha b | |
| 267 ∎ | |
| 268 | |
|
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
269 -- Yoneda's Lemma |
| 199 | 270 -- 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
|
271 -- that is FMapp Yoneda is injective and surjective |
| 194 | 272 |
|
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
273 -- λ b g → (A Category.o f₁) g |
|
1000
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
274 YonedaLemma1 : {a a' : Obj A } {f : FObj (FObj YonedaFunctor a) a' } |
| 987 | 275 → SetsAop [ F2Nat {a'} {FObj YonedaFunctor a} f ≈ FMap YonedaFunctor f ] |
|
1000
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
276 YonedaLemma1 {a} {a'} {f} = refl |
|
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
277 |
|
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
278 YonedaIso0 : {a a' : Obj A } {f : FObj (FObj YonedaFunctor a) a' } |
|
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
279 → Nat2F ( FMap YonedaFunctor f ) ≡ f |
|
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
280 YonedaIso0 {a} {a'} {f} = ≈-≡ A (≈-Reasoning.idR A) |
|
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
281 |
|
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
282 YonedaIso1 : {a a' : Obj A } → (ha : Hom SetsAop (y-obj a) (y-obj a')) |
|
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
283 → SetsAop [ FMap YonedaFunctor (Nat2F {a} ha) ≈ ha ] |
|
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
284 YonedaIso1 {a} {a'} ha = Nat2F→F2Nat ha |
| 987 | 285 |
| 286 domF : (y : Obj SetsAop) → {x : Obj (Category.op A)} → FObj y x → Obj A | |
| 287 domF y {x} z = x | |
| 288 | |
|
1000
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
289 YonedaLemma2 : {a a' b : Obj A } (f : Hom A a a' ) → NTrans (Category.op A) Sets (FObj YonedaFunctor a) (FObj YonedaFunctor a') |
|
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
290 YonedaLemma2 f = FMap YonedaFunctor f |
|
991
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
291 |
|
1000
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
292 YonedaLemma3 : {a a' b : Obj A } (f : Hom A a a' ) → (g : Hom A b a ) → Hom A b a' -- f o g |
|
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
293 YonedaLemma3 {a} {a'} {b} f g = TMap (FMap YonedaFunctor f) b g |
| 989 | 294 |
|
1000
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
295 YonedaLemma4 : {a a' b : Obj A } (f : Hom A a a' ) → (g : Hom A b a ) → Hom A b a' -- f o g |
|
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
296 YonedaLemma4 {a} {a'} {b} f = TMap (FMap YonedaFunctor f) b |
| 989 | 297 |
|
991
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
298 -- |
|
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
299 -- f ∈ FMap (FObj YonedaFunctor a') a |
|
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
300 -- |
|
e7848ad0c6f9
remove suc level in CCCGraph
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
990
diff
changeset
|
301 |
| 996 | 302 -- g f |
| 303 -- b --→ a ------→ a' | |
| 304 -- | | | |
| 305 -- TMap (H f) b | | TMap (H id) a' | |
| 306 -- o g ↓ ↓ o (f o g) | |
| 307 -- H a ------→ H a' | |
| 308 -- H f | |
| 995 | 309 -- |
|
1000
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
310 |
| 989 | 311 _^ : {a a' b : Obj A } → (f : Hom A a a' ) → Hom A b a → Hom A b a' |
| 312 _^ {a} {a'} {b} f g = (FMap (FObj YonedaFunctor a') g) f | |
| 313 | |
| 314 f-unique : {a a' b : Obj A } (f : Hom A a a' ) → f ^ ≡ TMap (FMap YonedaFunctor f) b | |
| 315 f-unique {a} {a'} {b} f = extensionality A (λ g → begin | |
| 316 (f ^ ) g ≡⟨⟩ | |
| 317 (FMap (FObj YonedaFunctor a') g) f ≡⟨⟩ | |
| 318 A [ f o g ] ≡⟨⟩ | |
| 319 TMap (FMap YonedaFunctor f) b g ∎ ) where open ≡-Reasoning | |
| 320 | |
|
1000
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
321 f-u : {a a' b : Obj A } (f : FObj (FObj YonedaFunctor a') a ) → Sets [ f ^ ≈ TMap (FMap YonedaFunctor f ) b ] |
|
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
322 f-u = f-unique |
|
3ef1b472e9f9
yoneda full and faithful
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
997
diff
changeset
|
323 |
| 1001 | 324 -- faithful (injective ) |
| 1003 | 325 Yoneda-injective : {a b b' : Obj A } → {x y : Obj SetsAop} → (g h : Hom A b b' ) (f : Hom A a b ) |
| 326 → SetsAop [ FMap YonedaFunctor g ≈ FMap YonedaFunctor h ] | |
| 327 → A [ g ≈ h ] | |
| 1001 | 328 Yoneda-injective {a} {b} {x} {y} g h f yg=yh = begin |
| 1003 | 329 g ≈↑⟨ idR ⟩ |
| 330 Nat2F (FMap YonedaFunctor g) ≈⟨ ylem11 yg=yh ⟩ | |
| 331 Nat2F (FMap YonedaFunctor h) ≈⟨ idR ⟩ | |
| 332 h ∎ where | |
| 333 ylem11 : SetsAop [ FMap YonedaFunctor g ≈ FMap YonedaFunctor h ] → A [ Nat2F (FMap YonedaFunctor g) ≈ Nat2F (FMap YonedaFunctor h) ] | |
| 334 ylem11 yg=yh with yg=yh {b} | |
| 335 ... | eq = ≈-Reasoning.≈←≡ A ( cong (λ k → k (id1 A b)) eq ) | |
| 336 open ≈-Reasoning A | |
| 1001 | 337 |
| 338 -- full (surjective) | |
| 339 | |
| 340 record CatSurjective { c₁ c₂ ℓ c₁' c₂' ℓ' : Level} ( A : Category c₁ c₂ ℓ ) ( B : Category c₁' c₂' ℓ' ) (F : Functor A B) | |
| 341 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ')) where | |
| 342 field | |
| 343 sur : {a a' : Obj A} (g : Hom B (FObj F a) (FObj F a')) → Hom A a a' | |
| 344 surjective : {a a' : Obj A} (g : Hom B (FObj F a) (FObj F a')) → B [ FMap F (sur g) ≈ g ] | |
| 345 | |
| 1002 | 346 open CatSurjective |
| 347 | |
| 1004 | 348 CatEpi : {c : Level} (F : Functor (Sets {c}) (Sets {c})) |
| 349 → (s : CatSurjective Sets Sets F ) | |
| 350 → {a a' : Obj Sets } {b : Obj Sets} (g h : Hom Sets (FObj F a') b) | |
| 1005 | 351 → Sets [ Sets [ g o FMap F ( sur s (id1 Sets _)) ] ≈ Sets [ h o FMap F ( sur s (id1 Sets _)) ] ] → Sets [ g ≈ h ] |
| 352 CatEpi F s g h eq = begin | |
| 353 g ≈↑⟨ idR ⟩ | |
| 354 Sets [ g o id1 Sets _ ] ≈↑⟨ cdr (surjective s (id1 Sets _) ) ⟩ | |
| 355 Sets [ g o FMap F (sur s (id1 Sets _)) ] ≈⟨ eq ⟩ | |
| 356 Sets [ h o FMap F (sur s (id1 Sets _)) ] ≈⟨ cdr (surjective s (id1 Sets _) ) ⟩ | |
| 357 Sets [ h o id1 Sets _ ] ≈⟨ idR ⟩ | |
| 1001 | 358 h ∎ |
| 359 where | |
| 1004 | 360 open ≈-Reasoning Sets |
| 1002 | 361 -- sj : B [ FMap F ( CatSurjective.sur s (FMap F (f g h))) ≈ FMap F (f g h) ] |
| 362 -- sj = CatSurjective.surjective s (FMap F (f g h)) | |
| 1001 | 363 |
| 364 Yoneda-surjective : CatSurjective A SetsAop YonedaFunctor | |
| 365 Yoneda-surjective = record { sur = λ {a} {a'} g → f g ; surjective = λ g → | |
| 366 begin | |
| 367 TMap (FMap YonedaFunctor (f g) ) _ ≈⟨ YonedaIso1 g ⟩ | |
| 368 TMap g _ ∎ | |
| 369 } where | |
| 370 open ≈-Reasoning Sets | |
| 371 f : {a a' : Obj A } → (g : Hom SetsAop (FObj YonedaFunctor a) (FObj YonedaFunctor a')) → Hom A a a' | |
| 372 f g = Nat2F g | |
| 373 | |
| 1005 | 374 Yoneda-epi : { b : Obj A } {x y : Obj SetsAop} → (g h : Hom SetsAop (FObj YonedaFunctor b) y) |
| 375 → ( {a : Obj A } (f : Hom A a b ) → SetsAop [ SetsAop [ g o FMap YonedaFunctor f ] ≈ SetsAop [ h o FMap YonedaFunctor f ] ] ) | |
| 1001 | 376 → SetsAop [ g ≈ h ] |
| 1005 | 377 Yoneda-epi {b} {x} {y} g h yg=yh = begin |
| 378 TMap g _ ≈↑⟨ idR ⟩ | |
| 379 Sets [ TMap g _ o id1 Sets _ ] ≈↑⟨ cdr (surjective Yoneda-surjective (id1 SetsAop _)) ⟩ | |
| 380 Sets [ TMap g _ o (λ z → A [ sur Yoneda-surjective (id1 SetsAop _) o z ] ) ] ≈⟨⟩ | |
| 381 (λ z → TMap g _ (A [ id1 A _ o z ] )) ≈⟨ yg=yh (id1 A b) ⟩ | |
| 382 Sets [ TMap h _ o (λ z → A [ sur Yoneda-surjective (id1 SetsAop _) o z ] ) ] ≈⟨ cdr (surjective Yoneda-surjective (id1 SetsAop _)) ⟩ | |
| 383 Sets [ TMap h _ o id1 Sets _ ] ≈⟨ idR ⟩ | |
| 1001 | 384 TMap h _ |
| 385 ∎ where | |
| 1002 | 386 open ≈-Reasoning Sets |
| 1001 | 387 s : CatSurjective A SetsAop YonedaFunctor |
| 388 s = Yoneda-surjective | |
| 389 | |
| 1008 | 390 --- How to prove it? from smallness? |
| 1005 | 391 |
| 1008 | 392 data _~_ {a b : Obj A} (f : Hom A a b) |
| 393 : ∀{x y : Obj A} → Hom A x y → Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where | |
| 394 refl : {g : Hom A a b} → (eqv : A [ f ≈ g ]) → f ~ g | |
| 1005 | 395 |
| 1008 | 396 postulate -- ? |
| 397 eqObj1 : {a b a' b' : Obj A } → Hom A a b ≡ Hom A a' b' → b ≡ b' | |
| 996 | 398 |
| 989 | 399 Yoneda-full-embed : {a b : Obj A } → FObj YonedaFunctor a ≡ FObj YonedaFunctor b → a ≡ b |
| 1008 | 400 Yoneda-full-embed {a} {b} eq = eqObj1 ylem1 where |
| 989 | 401 ylem1 : Hom A a a ≡ Hom A a b |
| 402 ylem1 = cong (λ k → FObj k a) eq | |
| 783 | 403 |