Mercurial > hg > Members > kono > Proof > category

annotate yoneda.agda @ 790:1e7319868d77

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Sets is CCC
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 19 Apr 2019 23:42:19 +0900
parents bded2347efa4
children 232cea484067
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
202
58ee98bbb333 remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 199
diff changeset
1 ---
189
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
2 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
3 -- A → Sets^A^op : Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
4 -- Contravariant Functor h_a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
5 -- Nat(h_a,F)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
6 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
7 ----
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
8
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Category -- https://github.com/konn/category-agda
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Level
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Category.Sets
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
12 module yoneda where
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
13 -- { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 open import HomReasoning
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 open import cat-utility
179
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 178
diff changeset
17 open import Relation.Binary.Core
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 178
diff changeset
18 open import Relation.Binary
781
340708e8d54f fix for 2.5.4.2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 693
diff changeset
19 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
340708e8d54f fix for 2.5.4.2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 693
diff changeset
20
179
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 178
diff changeset
21
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 -- Contravariant Functor : op A → Sets ( Obj of Sets^{A^op} )
197
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
24 -- Obj and Hom of Sets^A^op
181
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
25
197
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
26 open Functor
183
ea6fc610b480 Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 182
diff changeset
27
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
28 YObj : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁))
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
29 YObj {_} {c₂} A = Functor (Category.op A) (Sets {c₂})
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
30 YHom : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (f : YObj A ) → (g : YObj A ) → Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁))
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
31 YHom {_} {c₂} A f g = NTrans (Category.op A) (Sets {c₂}) f g
184
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
32
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
33 open NTrans
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
34 Yid : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : YObj A } → YHom A a a
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 299
diff changeset
35 Yid {_} {c₂} A {a} = record { TMap = λ a → λ x → x ; isNTrans = isNTrans1 {a} } where
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 299
diff changeset
36 isNTrans1 : {a : YObj A } → IsNTrans (Category.op A) (Sets {c₂}) a a (λ a → λ x → x )
184
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
37 isNTrans1 {a} = record { commute = refl }
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
38
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
39 _+_ : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b c : YObj A} → YHom A b c → YHom A a b → YHom A a c
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
40 _+_ {_} {c₂} {_} {A} {a} {b} {c} f g = record { TMap = λ x → Sets [ TMap f x o TMap g x ] ; isNTrans = isNTrans1 } where
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
41 commute1 : (a b c : YObj A ) (f : YHom A b c) (g : YHom A a b )
185
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
42 (a₁ b₁ : Obj (Category.op A)) (h : Hom (Category.op A) a₁ b₁) →
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
43 Sets [ Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] ≈
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
44 Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ]
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
45 commute1 a b c f g a₁ b₁ h = let open ≈-Reasoning (Sets {c₂})in begin
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
46 Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ]
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
47 ≈⟨ assoc {_} {_} {_} {_} {FMap c h } {TMap f a₁} {TMap g a₁} ⟩
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
48 Sets [ Sets [ FMap c h o TMap f a₁ ] o TMap g a₁ ]
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
49 ≈⟨ car (nat f) ⟩
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
50 Sets [ Sets [ TMap f b₁ o FMap b h ] o TMap g a₁ ]
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
51 ≈↑⟨ assoc {_} {_} {_} {_} { TMap f b₁} {FMap b h } {TMap g a₁}⟩
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
52 Sets [ TMap f b₁ o Sets [ FMap b h o TMap g a₁ ] ]
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
53 ≈⟨ cdr {_} {_} {_} {_} {_} { TMap f b₁} (nat g) ⟩
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
54 Sets [ TMap f b₁ o Sets [ TMap g b₁ o FMap a h ] ]
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
55 ≈↑⟨ assoc {_} {_} {_} {_} {TMap f b₁} {TMap g b₁} { FMap a h} ⟩
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
56 Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ]
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
57 ∎
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
58 isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) a c (λ x → Sets [ TMap f x o TMap g x ])
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
59 isNTrans1 = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h }
184
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
60
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
61 _==_ : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b : YObj A} → YHom A a b → YHom A a b → Set (c₂ ⊔ c₁)
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
62 _==_ {_} { c₂} {_} {A} 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
63
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
64 infix 4 _==_
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
65
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
66 isSetsAop : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → IsCategory (YObj A) (YHom A) _==_ _+_ ( Yid A )
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
67 isSetsAop {_} {c₂} {_} A =
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 299
diff changeset
68 record { isEquivalence = record {refl = refl ; trans = λ {i j k} → trans1 {_} {_} {i} {j} {k} ; sym = λ {i j} → sym1 {_} {_} {i} {j}}
189
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
69 ; identityL = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
70 ; identityR = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
71 ; o-resp-≈ = λ{a b c f g h i } → o-resp-≈ {a} {b} {c} {f} {g} {h} {i}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
72 ; associative = refl
358
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
73 } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
74 open ≈-Reasoning (Sets {c₂})
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
75 sym1 : {a b : YObj A } {i j : YHom A a b } → i == j → j == i
358
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
76 sym1 {a} {b} {i} {j} eq {x} = sym eq
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
77 trans1 : {a b : YObj A } {i j k : YHom A a b} → i == j → j == k → i == k
358
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
78 trans1 {a} {b} {i} {j} {k} i=j j=k {x} = trans-hom i=j j=k
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
79 o-resp-≈ : {A₁ B C : YObj A} {f g : YHom A A₁ B} {h i : YHom A B C} →
189
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
80 f == g → h == i → h + f == i + g
358
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
81 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
82
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
83 SetsAop : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Category (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (c₂ ⊔ c₁)
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
84 SetsAop {_} {c₂} {_} A =
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
85 record { Obj = YObj A
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
86 ; Hom = YHom A
186
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
87 ; _o_ = _+_
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
88 ; _≈_ = _==_
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
89 ; Id = Yid A
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
90 ; isCategory = isSetsAop A
186
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
91 }
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
92
197
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
93 -- A is Locally small
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
94 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
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
95
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
96 import Relation.Binary.PropositionalEquality
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
97 -- 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 )
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 358
diff changeset
98 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
197
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
99
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
100
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
101 ----
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
102 --
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
103 -- Object mapping in Yoneda Functor
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
104 --
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
105 ----
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
106
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
107 open import Function
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
108
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
109 y-obj : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor (Category.op A) (Sets {c₂})
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
110 y-obj {_} {c₂} {_} A a = record {
197
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
111 FObj = λ b → Hom (Category.op A) a b ;
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
112 FMap = λ {b c : Obj A } → λ ( f : Hom A c b ) → λ (g : Hom A b a ) → (Category.op A) [ f o g ] ;
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
113 isFunctor = record {
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 358
diff changeset
114 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
115 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
116 ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq )
197
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
117 }
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
118 } where
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
119 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
120 lemma-y-obj1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} idL
197
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
121 lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A b a₁) (g : Hom A c b ) → (x : Hom A a₁ a )→
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
122 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
123 lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} ( begin
197
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
124 Category.op A [ Category.op A [ g o f ] o x ]
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
125 ≈↑⟨ assoc ⟩
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
126 Category.op A [ g o Category.op A [ f o x ] ]
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
127 ≈⟨⟩
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
128 ( λ x → Category.op A [ g o x ] ) ( ( λ x → Category.op A [ f o x ] ) x )
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
129 ∎ )
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
130 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
131 lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} ( begin
197
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
132 Category.op A [ f o x ]
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
133 ≈⟨ resp refl-hom eq ⟩
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
134 Category.op A [ g o x ]
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
135 ∎ )
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
136
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
137
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
138 ----
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
139 --
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
140 -- Hom mapping in Yoneda Functor
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
141 --
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
142 ----
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
143
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
144 y-tmap : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( a b : Obj A ) → (f : Hom A a b ) → (x : Obj (Category.op A)) →
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
145 FObj (y-obj A a) x → FObj (y-obj A b ) x
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
146 y-tmap {_} {c₂} {_} A a b f x = λ ( g : Hom A x a ) → A [ f o g ] -- ( h : Hom A x b )
197
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
147
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
148 y-map : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } → (f : Hom A a b ) → YHom A (y-obj A a) (y-obj A b)
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
149 y-map {_} {c₂} {_} A {a} {b} f = record { TMap = y-tmap A a b f ; isNTrans = isNTrans1 {a} {b} f } where
197
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
150 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 ) →
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
151 Sets [ Sets [ FMap (y-obj A b) g o y-tmap A a b f a₁ ] ≈
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
152 Sets [ y-tmap A a b f b₁ o FMap (y-obj A a) g ] ]
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 358
diff changeset
153 lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ {_} {_} {_} {A} ( begin
197
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
154 A [ A [ f o x ] o g ]
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
155 ≈↑⟨ assoc ⟩
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
156 A [ f o A [ x o g ] ]
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
157 ∎ ) )
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
158 isNTrans1 : {a b : Obj A } → (f : Hom A a b ) → IsNTrans (Category.op A) (Sets {c₂}) (y-obj A a) (y-obj A b) (y-tmap A a b f )
197
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
159 isNTrans1 {a} {b} f = record { commute = λ{a₁ b₁ g } → lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f }
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
160
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
161 -----
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
162 --
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
163 -- Yoneda Functor itself
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
164 --
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
165 -----
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
166
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
167 YonedaFunctor : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Functor A (SetsAop A)
783
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
168 YonedaFunctor A = record {
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
169 FObj = λ a → y-obj A a
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
170 ; FMap = λ f → y-map A f
186
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
171 ; isFunctor = record {
187
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 186
diff changeset
172 identity = identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 186
diff changeset
173 ; distr = distr1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 186
diff changeset
174 ; ≈-cong = ≈-cong
196
c040369bd6d4 give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 195
diff changeset
175
186
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
176 }
187
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 186
diff changeset
177 } where
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
178 ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop A [ y-map A f ≈ y-map A g ]
202
58ee98bbb333 remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 199
diff changeset
179 ≈-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
180 extensionality A ( λ h → ≈-≡ {_} {_} {_} {A} ( begin
188
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
181 A [ f o h ]
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
182 ≈⟨ resp refl-hom eq ⟩
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
183 A [ g o h ]
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
184 ∎
202
58ee98bbb333 remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 199
diff changeset
185 ) )
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
186 identity : {a : Obj A} → SetsAop A [ y-map A (id1 A a) ≈ id1 (SetsAop A) (y-obj A a ) ]
188
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
187 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
188 extensionality A ( λ g → ≈-≡ {_} {_} {_} {A} ( begin
188
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 ∎
202
58ee98bbb333 remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 199
diff changeset
193 ) )
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
194 distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop A [ y-map A (A [ g o f ]) ≈ SetsAop A [ y-map A g o y-map A f ] ]
191
45191dc3f78a nat continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
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₁ ] ] )
468
c375d8f93a2c discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 358
diff changeset
196 extensionality A ( λ h → ≈-≡ {_} {_} {_} {A} ( begin
188
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
197 A [ A [ g o f ] o h ]
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
198 ≈↑⟨ assoc ⟩
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
199 A [ g o A [ f o h ] ]
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
200 ∎
202
58ee98bbb333 remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 199
diff changeset
201 ) )
184
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
202
185
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
203
190
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
204 ------
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
205 --
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
206 -- F : A → Sets ∈ Obj SetsAop
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
207 --
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 299
diff changeset
208 -- F(a) → Nat(h_a,F)
191
45191dc3f78a nat continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
209 -- x ∈ F(a) , (g : Hom A b a) → ( FMap F g ) x
190
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
210 ------
187
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 186
diff changeset
211
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
212 F2Natmap : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A} → {F : Obj ( SetsAop A) }
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
213 → {x : FObj F a} → (b : Obj (Category.op A)) → Hom Sets (FObj (y-obj A a) b) (FObj F b)
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
214 F2Natmap A {a} {F} {x} b = λ ( g : Hom A b a ) → ( FMap F g ) x
190
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
215
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
216 F2Nat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A} → {F : Obj (SetsAop A )} → FObj F a → Hom (SetsAop A) (y-obj A a) F
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
217 F2Nat {_} {c₂} A {a} {F} x = record { TMap = F2Natmap A {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
218 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
219 (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
220 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
221 cong ( λ f → f x ) ( sym ( distr F ) )
191
45191dc3f78a nat continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
222 commute : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} →
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
223 Sets [ Sets [ FMap F f o F2Natmap A {a} {F} {x} a₁ ] ≈ Sets [ F2Natmap A {a} {F} {x} b o FMap (y-obj A a) f ] ]
192
d7e4b7b441be F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 191
diff changeset
224 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
225 begin
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
226 Sets [ FMap F f o F2Natmap A {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
227 ≈⟨⟩
d7e4b7b441be F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 191
diff changeset
228 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
229 ≈⟨ extensionality A ( λ (g : Hom A a₁ a) → commute1 {a₁} {b} {f} g ) ⟩
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
230 Sets [ (λ ( g : Hom A b a ) → ( FMap F g ) x) o FMap (y-obj A a) f ]
192
d7e4b7b441be F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 191
diff changeset
231 ≈⟨⟩
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
232 Sets [ F2Natmap A {a} {F} {x} b o FMap (y-obj A a) f ]
192
d7e4b7b441be F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 191
diff changeset
233 ∎
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
234 isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) (y-obj A a) F (F2Natmap A {a} {F})
191
45191dc3f78a nat continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
235 isNTrans1 = record { commute = λ {a₁ b f} → commute {a₁} {b} {f} }
190
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
236
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
237
199
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 198
diff changeset
238 -- F(a) <- Nat(h_a,F)
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
239 Nat2F : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A} → {F : Obj (SetsAop A) } → Hom (SetsAop A) (y-obj A a) F → FObj F a
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
240 Nat2F A {a} {F} ha = ( TMap ha a ) (id1 A a)
190
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
241
199
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 198
diff changeset
242 ----
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 198
diff changeset
243 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 198
diff changeset
244 -- Prove Bijection (as routine exercise ...)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 198
diff changeset
245 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 198
diff changeset
246 ----
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 198
diff changeset
247
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
248 F2Nat→Nat2F : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A } → {F : Obj (SetsAop A)} → (fa : FObj F a)
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
249 → Nat2F A {a} {F} (F2Nat A {a} {F} fa) ≡ fa
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
250 F2Nat→Nat2F A {a} {F} fa = let open ≈-Reasoning (Sets) in cong ( λ f → f fa ) (
199
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 198
diff changeset
251 -- FMap F (Category.Category.Id A) fa ≡ fa
194
3271d2d04b17 F2Nat→Nat2F done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
252 begin
3271d2d04b17 F2Nat→Nat2F done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
253 ( FMap F (id1 A _ ))
3271d2d04b17 F2Nat→Nat2F done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
254 ≈⟨ IsFunctor.identity (isFunctor F) ⟩
3271d2d04b17 F2Nat→Nat2F done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
255 id1 Sets (FObj F a)
3271d2d04b17 F2Nat→Nat2F done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
256 ∎ )
3271d2d04b17 F2Nat→Nat2F done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
257
3271d2d04b17 F2Nat→Nat2F done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
258 open import Relation.Binary.PropositionalEquality
3271d2d04b17 F2Nat→Nat2F done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
259
202
58ee98bbb333 remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 199
diff changeset
260 ≡-cong = Relation.Binary.PropositionalEquality.cong
193
4e6f080f0107 isomorphic problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 192
diff changeset
261
195
428d46dfd5aa Nat2F→F2Nat done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 194
diff changeset
262 -- F : op A → Sets
197
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
263 -- ha : NTrans (op A) Sets (y-obj {a}) F
ec50ff189f62 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 196
diff changeset
264 -- FMap F g o TMap ha a ≈ TMap ha b o FMap (y-obj {a}) g
195
428d46dfd5aa Nat2F→F2Nat done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 194
diff changeset
265
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
266 Nat2F→F2Nat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A } → {F : Obj (SetsAop A)} → (ha : Hom (SetsAop A) (y-obj A a) F)
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
267 → SetsAop A [ F2Nat A {a} {F} (Nat2F A {a} {F} ha) ≈ ha ]
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
268 Nat2F→F2Nat A {a} {F} ha {b} = let open ≡-Reasoning in
194
3271d2d04b17 F2Nat→Nat2F done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
269 begin
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
270 TMap (F2Nat A {a} {F} (Nat2F A {a} {F} ha)) b
202
58ee98bbb333 remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 199
diff changeset
271 ≡⟨⟩
58ee98bbb333 remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 199
diff changeset
272 (λ 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
273 ≡⟨ extensionality A (λ g → (
195
428d46dfd5aa Nat2F→F2Nat done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 194
diff changeset
274 begin
428d46dfd5aa Nat2F→F2Nat done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 194
diff changeset
275 FMap F g (TMap ha a (Category.Category.Id A))
203
1c16d18a8d67 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 202
diff changeset
276 ≡⟨ ≡-cong (λ f → f (Category.Category.Id A)) (IsNTrans.commute (isNTrans ha)) ⟩
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
277 TMap ha b (FMap (y-obj A a) g (Category.Category.Id A))
195
428d46dfd5aa Nat2F→F2Nat done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 194
diff changeset
278 ≡⟨⟩
428d46dfd5aa Nat2F→F2Nat done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 194
diff changeset
279 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
280 ≡⟨ ≡-cong ( TMap ha b ) ( ≈-≡ {_} {_} {_} {A} (IsCategory.identityL ( Category.isCategory A ))) ⟩
195
428d46dfd5aa Nat2F→F2Nat done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 194
diff changeset
281 TMap ha b g
428d46dfd5aa Nat2F→F2Nat done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 194
diff changeset
282 ∎
202
58ee98bbb333 remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 199
diff changeset
283 )) ⟩
58ee98bbb333 remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 199
diff changeset
284 TMap ha b
195
428d46dfd5aa Nat2F→F2Nat done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 194
diff changeset
285 ∎
194
3271d2d04b17 F2Nat→Nat2F done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
286
196
c040369bd6d4 give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 195
diff changeset
287 -- Yoneda's Lemma
199
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 198
diff changeset
288 -- 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
289 -- that is FMapp Yoneda is injective and surjective
194
3271d2d04b17 F2Nat→Nat2F done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
290
196
c040369bd6d4 give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 195
diff changeset
291 -- λ b g → (A Category.o f₁) g
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
292 YondaLemma1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a a' : Obj A } {f : FObj (FObj (YonedaFunctor A) a) a' }
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
293 → SetsAop A [ F2Nat A {a'} {FObj (YonedaFunctor A) a} f ≈ FMap (YonedaFunctor A) f ]
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
294 YondaLemma1 A {a} {a'} {f} = refl
195
428d46dfd5aa Nat2F→F2Nat done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 194
diff changeset
295
196
c040369bd6d4 give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 195
diff changeset
296 -- 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
297
204
b2874c5086ea embedding done?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 203
diff changeset
298 -- Full embedding of Yoneda Functor requires injective on Object,
b2874c5086ea embedding done?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 203
diff changeset
299 --
b2874c5086ea embedding done?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 203
diff changeset
300 -- 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
301 -- FObj YonedaFunctor a ≡ FObj YonedaFunctor b → a ≡ b
783
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
302
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
303 open import Relation.Nullary
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
304 open import Data.Empty
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
305
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
306 --YondaLemma2 : {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) →
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
307 -- (a b x : Obj A ) → (FObj (FObj (YonedaFunctor A) a) x) ≡ (FObj (FObj (YonedaFunctor A) b ) x) → a ≡ b
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
308 --YondaLemma2 A a bx eq = {!!}
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
309
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 204
diff changeset
310 -- N.B = ≡-cong gives you ! a ≡ b, so we cannot cong inv to prove a ≡ b
783
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
311
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
312 --record Category c₁ c₂ ℓ : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
313 -- infixr 9 _o_
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
314 -- infix 4 _≈_
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
315 -- field
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
316 -- Obj : Set c₁
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
317 -- Hom : Obj → Obj → Set c₂
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
318 --YondaLemma31 : {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) →
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
319 -- (a b x : Obj A ) → Hom A a x ≡ Hom A b x → a ≡ b
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
320 --YondaLemma31 A a b x eq = {!!}
204
b2874c5086ea embedding done?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 203
diff changeset
321 --
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 204
diff changeset
322 -- Instead we prove only
204
b2874c5086ea embedding done?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 203
diff changeset
323 -- inv ( FObj YonedaFunctor a ) ≡ a
196
c040369bd6d4 give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 195
diff changeset
324
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
325 inv : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a x : Obj A} ( f : FObj (FObj (YonedaFunctor A) a) x) → Obj A
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
326 inv A {a} f = Category.cod A f
203
1c16d18a8d67 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 202
diff changeset
327
299
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
328 YonedaLemma21 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a x : Obj A} ( f : ( FObj (FObj (YonedaFunctor A ) a) x) ) → inv A f ≡ a
8c72f5284bc8 remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
329 YonedaLemma21 A {a} {x} f = refl
203
1c16d18a8d67 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 202
diff changeset
330
693
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 660
diff changeset
331 open import Relation.Binary.HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 660
diff changeset
332 a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 660
diff changeset
333 a1 refl = refl
783
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
334
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
335 -- YondaLemma3 : {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) →
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
336 -- (a b x : Obj A ) → Hom A a x ≅ Hom A b x → a ≡ b
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
337 -- YondaLemma3 A a b x eq = {!!} -- ≡-cong (inv A) ?
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
338
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
339 a2 : ( a b : Set ) (f : a → a ) (g : b → a ) -> f ≅ g → a ≡ b
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
340 a2 a b f g eq = {!!}
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
341
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
342 -- YonedaInjective : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A}
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
343 -- → FObj (FObj (YonedaFunctor A ) a ) a ≅ FObj (FObj (YonedaFunctor A ) a ) b
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
344 -- → a ≡ b
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
345 -- YonedaInjective A {a} {b} eq = {!!}
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
346
bded2347efa4 CCC by equation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 781
diff changeset
347