Mercurial > hg > Members > kono > Proof > category
annotate pullback.agda @ 292:a84fab7cf46a
on going
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 25 Sep 2013 18:15:43 +0900 |
parents | c8e26650ddf9 |
children | fb0ab8c72e15 |
rev | line source |
---|---|
260 | 1 -- Pullback from product and equalizer |
2 -- | |
3 -- | |
4 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> | |
5 ---- | |
6 | |
7 open import Category -- https://github.com/konn/category-agda | |
8 open import Level | |
266 | 9 module pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ') ( Γ : Functor I A ) where |
260 | 10 |
11 open import HomReasoning | |
12 open import cat-utility | |
13 | |
282 | 14 -- |
264 | 15 -- Pullback from equalizer and product |
260 | 16 -- f |
17 -- a -------> c | |
282 | 18 -- ^ ^ |
260 | 19 -- π1 | |g |
20 -- | | | |
21 -- ab -------> b | |
22 -- ^ π2 | |
23 -- | | |
282 | 24 -- | e = equalizer (f π1) (g π1) |
264 | 25 -- | |
26 -- d <------------------ d' | |
27 -- k (π1' × π2' ) | |
260 | 28 |
261 | 29 open Equalizer |
30 open Product | |
31 open Pullback | |
32 | |
282 | 33 pullback-from : (a b c ab d : Obj A) |
260 | 34 ( f : Hom A a c ) ( g : Hom A b c ) |
261 | 35 ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( e : Hom A d ab ) |
282 | 36 ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g ) |
37 ( prod : Product A a b ab π1 π2 ) → Pullback A a b c d f g | |
261 | 38 ( A [ π1 o equalizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ){e} ) ] ) |
282 | 39 ( A [ π2 o equalizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ){e} ) ] ) |
261 | 40 pullback-from a b c ab d f g π1 π2 e eqa prod = record { |
260 | 41 commute = commute1 ; |
282 | 42 p = p1 ; |
43 π1p=π1 = λ {d} {π1'} {π2'} {eq} → π1p=π11 {d} {π1'} {π2'} {eq} ; | |
44 π2p=π2 = λ {d} {π1'} {π2'} {eq} → π2p=π21 {d} {π1'} {π2'} {eq} ; | |
260 | 45 uniqueness = uniqueness1 |
282 | 46 } where |
261 | 47 commute1 : A [ A [ f o A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ≈ A [ g o A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ] |
262 | 48 commute1 = let open ≈-Reasoning (A) in |
49 begin | |
282 | 50 f o ( π1 o equalizer (eqa ( f o π1 ) ( g o π2 )) ) |
262 | 51 ≈⟨ assoc ⟩ |
282 | 52 ( f o π1 ) o equalizer (eqa ( f o π1 ) ( g o π2 )) |
262 | 53 ≈⟨ fe=ge (eqa (A [ f o π1 ]) (A [ g o π2 ])) ⟩ |
282 | 54 ( g o π2 ) o equalizer (eqa ( f o π1 ) ( g o π2 )) |
262 | 55 ≈↑⟨ assoc ⟩ |
282 | 56 g o ( π2 o equalizer (eqa ( f o π1 ) ( g o π2 )) ) |
262 | 57 ∎ |
282 | 58 lemma1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → |
262 | 59 A [ A [ A [ f o π1 ] o (prod × π1') π2' ] ≈ A [ A [ g o π2 ] o (prod × π1') π2' ] ] |
282 | 60 lemma1 {d'} { π1' } { π2' } eq = let open ≈-Reasoning (A) in |
262 | 61 begin |
62 ( f o π1 ) o (prod × π1') π2' | |
63 ≈↑⟨ assoc ⟩ | |
64 f o ( π1 o (prod × π1') π2' ) | |
65 ≈⟨ cdr (π1fxg=f prod) ⟩ | |
66 f o π1' | |
67 ≈⟨ eq ⟩ | |
68 g o π2' | |
69 ≈↑⟨ cdr (π2fxg=g prod) ⟩ | |
70 g o ( π2 o (prod × π1') π2' ) | |
71 ≈⟨ assoc ⟩ | |
72 ( g o π2 ) o (prod × π1') π2' | |
73 ∎ | |
261 | 74 p1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d' d |
282 | 75 p1 {d'} { π1' } { π2' } eq = |
262 | 76 let open ≈-Reasoning (A) in k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) ( lemma1 eq ) |
282 | 77 π1p=π11 : {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → |
262 | 78 A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π1' ] |
79 π1p=π11 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in | |
80 begin | |
81 ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq | |
82 ≈⟨⟩ | |
83 ( π1 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) | |
84 ≈↑⟨ assoc ⟩ | |
85 π1 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) ) | |
86 ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩ | |
282 | 87 π1 o (_×_ prod π1' π2' ) |
262 | 88 ≈⟨ π1fxg=f prod ⟩ |
89 π1' | |
90 ∎ | |
282 | 91 π2p=π21 : {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → |
263 | 92 A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π2' ] |
262 | 93 π2p=π21 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in |
94 begin | |
95 ( π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq | |
96 ≈⟨⟩ | |
97 ( π2 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) | |
98 ≈↑⟨ assoc ⟩ | |
99 π2 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) ) | |
100 ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩ | |
282 | 101 π2 o (_×_ prod π1' π2' ) |
262 | 102 ≈⟨ π2fxg=g prod ⟩ |
103 π2' | |
104 ∎ | |
261 | 105 uniqueness1 : {d₁ : Obj A} (p' : Hom A d₁ d) {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → |
106 {eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} → | |
107 {eq2 : A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} → | |
108 A [ p1 eq ≈ p' ] | |
264 | 109 uniqueness1 {d'} p' {π1'} {π2'} {eq} {eq1} {eq2} = let open ≈-Reasoning (A) in |
263 | 110 begin |
111 p1 eq | |
112 ≈⟨⟩ | |
113 k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) | |
264 | 114 ≈⟨ Equalizer.uniqueness (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e}) ( begin |
115 e o p' | |
116 ≈⟨⟩ | |
117 equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p' | |
118 ≈↑⟨ Product.uniqueness prod ⟩ | |
119 (prod × ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p') ) ( π2 o (equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p')) | |
120 ≈⟨ ×-cong prod (assoc) (assoc) ⟩ | |
121 (prod × (A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ])) | |
282 | 122 (A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]) |
264 | 123 ≈⟨ ×-cong prod eq1 eq2 ⟩ |
124 ((prod × π1') π2') | |
125 ∎ ) ⟩ | |
263 | 126 p' |
127 ∎ | |
128 | |
266 | 129 ------ |
130 -- | |
131 -- Limit | |
132 -- | |
133 ----- | |
134 | |
135 -- Constancy Functor | |
136 | |
291 | 137 K : { c₁' c₂' ℓ' : Level} (A : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( I : Category c₁'' c₂'' ℓ'' ) |
138 → ( a : Obj A ) → Functor I A | |
139 K A I a = record { | |
265 | 140 FObj = λ i → a ; |
141 FMap = λ f → id1 A a ; | |
142 isFunctor = let open ≈-Reasoning (A) in record { | |
143 ≈-cong = λ f=g → refl-hom | |
144 ; identity = refl-hom | |
145 ; distr = sym idL | |
146 } | |
147 } | |
148 | |
149 open NTrans | |
150 | |
291 | 151 record Limit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) |
152 ( a0 : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where | |
265 | 153 field |
291 | 154 limit : ( a : Obj A ) → ( t : NTrans I A ( K A I a ) Γ ) → Hom A a a0 |
155 t0f=t : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → ∀ { i : Obj I } → | |
265 | 156 A [ A [ TMap t0 i o limit a t ] ≈ TMap t i ] |
291 | 157 limit-uniqueness : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } → |
271 | 158 A [ A [ TMap t0 i o f ] ≈ TMap t i ] ) → A [ limit a t ≈ f ] |
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
159 A0 : Obj A |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
160 A0 = a0 |
291 | 161 T0 : NTrans I A ( K A I a0 ) Γ |
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
162 T0 = t0 |
265 | 163 |
266 | 164 -------------------------------- |
165 -- | |
166 -- If we have two limits on c and c', there are isomorphic pair h, h' | |
167 | |
168 open Limit | |
169 | |
170 iso-l : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) | |
291 | 171 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) ( t0' : NTrans I A ( K A I a0' ) Γ ) |
172 ( lim : Limit A I Γ a0 t0 ) → ( lim' : Limit A I Γ a0' t0' ) | |
266 | 173 → Hom A a0 a0' |
174 iso-l I Γ a0 a0' t0 t0' lim lim' = limit lim' a0 t0 | |
175 | |
176 iso-r : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) | |
291 | 177 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) ( t0' : NTrans I A ( K A I a0' ) Γ ) |
178 ( lim : Limit A I Γ a0 t0 ) → ( lim' : Limit A I Γ a0' t0' ) | |
266 | 179 → Hom A a0' a0 |
180 iso-r I Γ a0 a0' t0 t0' lim lim' = limit lim a0' t0' | |
181 | |
182 | |
183 iso-lr : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) | |
291 | 184 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ ) ( t0' : NTrans I A ( K A I a0' ) Γ ) |
185 ( lim : Limit A I Γ a0 t0 ) → ( lim' : Limit A I Γ a0' t0' ) → ∀{ i : Obj I } → | |
266 | 186 A [ A [ iso-l I Γ a0 a0' t0 t0' lim lim' o iso-r I Γ a0 a0' t0 t0' lim lim' ] ≈ id1 A a0' ] |
187 iso-lr I Γ a0 a0' t0 t0' lim lim' {i} = let open ≈-Reasoning (A) in begin | |
188 limit lim' a0 t0 o limit lim a0' t0' | |
271 | 189 ≈↑⟨ limit-uniqueness lim' ( λ {i} → ( begin |
266 | 190 TMap t0' i o ( limit lim' a0 t0 o limit lim a0' t0' ) |
191 ≈⟨ assoc ⟩ | |
282 | 192 ( TMap t0' i o limit lim' a0 t0 ) o limit lim a0' t0' |
266 | 193 ≈⟨ car ( t0f=t lim' ) ⟩ |
282 | 194 TMap t0 i o limit lim a0' t0' |
266 | 195 ≈⟨ t0f=t lim ⟩ |
282 | 196 TMap t0' i |
271 | 197 ∎) ) ⟩ |
266 | 198 limit lim' a0' t0' |
271 | 199 ≈⟨ limit-uniqueness lim' idR ⟩ |
266 | 200 id a0' |
201 ∎ | |
202 | |
203 | |
282 | 204 open import CatExponetial |
267 | 205 |
206 open Functor | |
207 | |
208 -------------------------------- | |
209 -- | |
210 -- Contancy Functor | |
266 | 211 |
268 | 212 KI : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) → Functor A ( A ^ I ) |
213 KI { c₁'} {c₂'} {ℓ'} I = record { | |
291 | 214 FObj = λ a → K A I a ; |
215 FMap = λ f → record { -- NTrans I A (K A I a) (K A I b) | |
267 | 216 TMap = λ a → f ; |
282 | 217 isNTrans = record { |
267 | 218 commute = λ {a b f₁} → commute1 {a} {b} {f₁} f |
219 } | |
282 | 220 } ; |
266 | 221 isFunctor = let open ≈-Reasoning (A) in record { |
267 | 222 ≈-cong = λ f=g {x} → f=g |
266 | 223 ; identity = refl-hom |
267 | 224 ; distr = refl-hom |
266 | 225 } |
267 | 226 } where |
227 commute1 : {a b : Obj I} {f₁ : Hom I a b} → {a' b' : Obj A} → (f : Hom A a' b' ) → | |
291 | 228 A [ A [ FMap (K A I b') f₁ o f ] ≈ A [ f o FMap (K A I a') f₁ ] ] |
282 | 229 commute1 {a} {b} {f₁} {a'} {b'} f = let open ≈-Reasoning (A) in begin |
291 | 230 FMap (K A I b') f₁ o f |
267 | 231 ≈⟨ idL ⟩ |
232 f | |
233 ≈↑⟨ idR ⟩ | |
291 | 234 f o FMap (K A I a') f₁ |
267 | 235 ∎ |
236 | |
237 | |
272 | 238 --------- |
239 -- | |
240 -- limit gives co universal mapping ( i.e. adjunction ) | |
241 -- | |
242 -- F = KI I : Functor A (A ^ I) | |
282 | 243 -- U = λ b → A0 (lim b {a0 b} {t0 b} |
244 -- ε = λ b → T0 ( lim b {a0 b} {t0 b} ) | |
272 | 245 |
282 | 246 limit2couniv : |
291 | 247 ( lim : ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 t0 ) |
248 → ( a0 : ( b : Functor I A ) → Obj A ) ( t0 : ( b : Functor I A ) → NTrans I A ( K A I (a0 b) ) b ) | |
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
249 → coUniversalMapping A ( A ^ I ) (KI I) (λ b → A0 (lim b {a0 b} {t0 b} ) ) ( λ b → T0 ( lim b {a0 b} {t0 b} ) ) |
277 | 250 limit2couniv lim a0 t0 = record { -- F U ε |
274
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
251 _*' = λ {b} {a} k → limit (lim b {a0 b} {t0 b} ) a k ; -- η |
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
252 iscoUniversalMapping = record { |
282 | 253 couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ; |
271 | 254 couniquness = couniquness2 |
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
255 } |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
256 } where |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
257 couniversalMapping1 : {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} → |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
258 A ^ I [ A ^ I [ T0 (lim b {a0 b} {t0 b}) o FMap (KI I) (limit (lim b {a0 b} {t0 b}) a f) ] ≈ f ] |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
259 couniversalMapping1 {b} {a} {f} {i} = let open ≈-Reasoning (A) in begin |
282 | 260 TMap (T0 (lim b {a0 b} {t0 b})) i o TMap ( FMap (KI I) (limit (lim b {a0 b} {t0 b}) a f) ) i |
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
261 ≈⟨⟩ |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
262 TMap (t0 b) i o (limit (lim b) a f) |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
263 ≈⟨ t0f=t (lim b) ⟩ |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
264 TMap f i -- i comes from ∀{i} → B [ TMap f i ≈ TMap g i ] |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
265 ∎ |
271 | 266 couniquness2 : {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} {g : Hom A a (A0 (lim b {a0 b} {t0 b} ))} → |
282 | 267 ( ∀ { i : Obj I } → A [ A [ TMap (T0 (lim b {a0 b} {t0 b} )) i o TMap ( FMap (KI I) g) i ] ≈ TMap f i ] ) |
272 | 268 → A [ limit (lim b {a0 b} {t0 b} ) a f ≈ g ] |
271 | 269 couniquness2 {b} {a} {f} {g} lim-g=f = let open ≈-Reasoning (A) in begin |
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
270 limit (lim b {a0 b} {t0 b} ) a f |
271 | 271 ≈⟨ limit-uniqueness ( lim b {a0 b} {t0 b} ) lim-g=f ⟩ |
270
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
272 g |
8ba03259a177
one yellow remain on ∀{x} → B [ TMap f x ≈ TMap g x ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
273 ∎ |
268 | 274 |
272 | 275 open import Category.Cat |
275 | 276 |
277 | |
278 | 278 open coUniversalMapping |
282 | 279 |
280 univ2limit : | |
281 ( U : Obj (A ^ I ) → Obj A ) | |
291 | 282 ( ε : ( b : Obj (A ^ I ) ) → NTrans I A (K A I (U b)) b ) |
279
8df8e74e6316
limit and prod/equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
278
diff
changeset
|
283 ( univ : coUniversalMapping A (A ^ I) (KI I) U (ε) ) → |
291 | 284 ( Γ : Functor I A ) → Limit A I Γ (U Γ) (ε Γ) |
278 | 285 univ2limit U ε univ Γ = record { |
272 | 286 limit = λ a t → limit1 a t ; |
282 | 287 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; |
288 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f | |
272 | 289 } where |
291 | 290 limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a (U Γ) |
282 | 291 limit1 a t = _*' univ {_} {a} t |
291 | 292 t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} → |
279
8df8e74e6316
limit and prod/equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
278
diff
changeset
|
293 A [ A [ TMap (ε Γ) i o limit1 a t ] ≈ TMap t i ] |
274
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
294 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin |
279
8df8e74e6316
limit and prod/equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
278
diff
changeset
|
295 TMap (ε Γ) i o limit1 a t |
274
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
296 ≈⟨⟩ |
280 | 297 TMap (ε Γ) i o _*' univ {Γ} {a} t |
298 ≈⟨ coIsUniversalMapping.couniversalMapping ( iscoUniversalMapping univ) {Γ} {a} {t} ⟩ | |
274
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
299 TMap t i |
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
300 ∎ |
291 | 301 limit-uniqueness1 : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a (U Γ)} |
279
8df8e74e6316
limit and prod/equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
278
diff
changeset
|
302 → ( ∀ { i : Obj I } → A [ A [ TMap (ε Γ) i o f ] ≈ TMap t i ] ) → A [ limit1 a t ≈ f ] |
274
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
303 limit-uniqueness1 {a} {t} {f} εf=t = let open ≈-Reasoning (A) in begin |
278 | 304 _*' univ t |
305 ≈⟨ ( coIsUniversalMapping.couniquness ( iscoUniversalMapping univ) ) εf=t ⟩ | |
274
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
306 f |
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
307 ∎ |
1b651faa2391
adjoint2limit problems are written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
273
diff
changeset
|
308 |
281
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
309 ----- |
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
310 -- |
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
311 -- product on arbitrary index |
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
312 -- |
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
313 |
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
314 record IProduct { c c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Set c) |
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
315 ( p : Obj A ) -- product |
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
316 ( ai : I → Obj A ) -- families |
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
317 ( pi : (i : I ) → Hom A p ( ai i ) ) -- projections |
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
318 : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where |
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
319 field |
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
320 product : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p |
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
321 pif=q : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i ) o ( product qi ) ] ≈ (qi i) ] |
290 | 322 -- special case of product ( qi = pi ) ( should b proved from pif=q ) |
289
7dc163c026b7
move to iProduct axiom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
288
diff
changeset
|
323 pif=q1 : { i : I } → { qi : Hom A p (ai i) } → A [ pi i ≈ qi ] |
281
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
324 ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ product ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ] |
283 | 325 ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } |
282 | 326 → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ product qi ≈ product qi' ] |
327 | |
328 open IProduct | |
283 | 329 open Equalizer |
281
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
330 |
282 | 331 -- |
332 -- limit from equalizer and product | |
333 -- | |
334 -- | |
283 | 335 -- ai |
336 -- ^ K f = id lim | |
337 -- | pi lim = K i ------------> K j = lim | |
338 -- | | | | |
339 -- p | | | |
340 -- ^ ε i | | ε j | |
341 -- | | | | |
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
342 -- | e = equalizer (id p) (id p) | | |
283 | 343 -- | v v |
344 -- lim <------------------ d' a i = Γ i ------------> Γ j = a j | |
345 -- k ( product pi ) Γ f | |
346 -- Γ f o ε i = ε j | |
347 -- | |
348 -- | |
281
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
349 |
291 | 350 -- pi-ε -- : ( prod : (p : Obj A) ( ai : Obj I → Obj A ) ( pi : (i : Obj I) → Hom A p ( ai i ) ) |
351 -- → IProduct {c₁'} A (Obj I) p ai pi ) | |
352 -- ( lim p : Obj A ) ( e : Hom A lim p ) | |
353 -- ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) → | |
354 -- { i : Obj I } → { q : ( i : Obj I ) → Hom A p (FObj Γ i) } → A [ proj i ≈ q i ] | |
355 -- pi-ε prod lim p e proj {i} {q} = let open ≈-Reasoning (A) in begin | |
356 -- proj i | |
357 -- ≈↑⟨ idR ⟩ | |
358 -- proj i o id1 A p | |
359 -- ≈⟨ cdr {!!} ⟩ | |
360 -- proj i o product (prod p (FObj Γ) proj) q | |
361 -- ≈⟨ pif=q (prod p (FObj Γ) proj) q ⟩ | |
362 -- q i | |
363 -- ∎ | |
364 | |
365 | |
283 | 366 limit-ε : |
281
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
367 ( prod : (p : Obj A) ( ai : Obj I → Obj A ) ( pi : (i : Obj I) → Hom A p ( ai i ) ) |
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
368 → IProduct {c₁'} A (Obj I) p ai pi ) |
282 | 369 ( lim p : Obj A ) ( e : Hom A lim p ) |
370 ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) → | |
291 | 371 NTrans I A (K A I lim) Γ |
290 | 372 limit-ε prod lim p e proj = record { |
282 | 373 TMap = tmap ; |
281
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
374 isNTrans = record { |
282 | 375 commute = commute1 |
281
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
376 } |
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
377 } where |
291 | 378 tmap : (i : Obj I) → Hom A (FObj (K A I lim) i) (FObj Γ i) |
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
379 tmap i = A [ proj i o e ] |
283 | 380 commute1 : {i j : Obj I} {f : Hom I i j} → |
291 | 381 A [ A [ FMap Γ f o tmap i ] ≈ A [ tmap j o FMap (K A I lim) f ] ] |
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
382 commute1 {i} {j} {f} = let open ≈-Reasoning (A) in begin |
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
383 FMap Γ f o tmap i |
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
384 ≈⟨⟩ |
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
385 FMap Γ f o ( proj i o e ) |
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
386 ≈⟨ assoc ⟩ |
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
387 ( FMap Γ f o proj i ) o e |
289
7dc163c026b7
move to iProduct axiom
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
288
diff
changeset
|
388 ≈↑⟨ car ( pif=q1 ( prod p (FObj Γ) proj ) {j} ) ⟩ |
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
389 proj j o e |
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
390 ≈↑⟨ idR ⟩ |
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
391 (proj j o e ) o id1 A lim |
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
392 ≈⟨⟩ |
291 | 393 tmap j o FMap (K A I lim) f |
288 | 394 ∎ |
281
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
395 |
282 | 396 limit-from : |
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
397 ( prod : (p : Obj A) ( ai : Obj I → Obj A ) ( pi : (i : Obj I) → Hom A p ( ai i ) ) |
281
dbd2044add2a
limit from product and equalizer continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
280
diff
changeset
|
398 → IProduct {c₁'} A (Obj I) p ai pi ) |
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
399 ( eqa : {a b c : Obj A} → (e : Hom A c a ) → (f g : Hom A a b) → Equalizer A e f g ) |
290 | 400 ( lim p : Obj A ) -- limit to be made |
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
401 ( e : Hom A lim p ) -- existing of equalizer |
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
402 ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) -- existing of product ( projection actually ) |
291 | 403 → Limit A I Γ lim ( limit-ε prod lim p e proj ) |
290 | 404 limit-from prod eqa lim p e proj = record { |
282 | 405 limit = λ a t → limit1 a t ; |
406 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; | |
407 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f | |
408 } where | |
291 | 409 limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a lim |
283 | 410 limit1 a t = let open ≈-Reasoning (A) in k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom |
291 | 411 t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} → |
290 | 412 A [ A [ TMap (limit-ε prod lim p e proj ) i o limit1 a t ] ≈ TMap t i ] |
283 | 413 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin |
290 | 414 TMap (limit-ε prod lim p e proj ) i o limit1 a t |
283 | 415 ≈⟨⟩ |
416 ( ( proj i ) o e ) o k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom | |
417 ≈↑⟨ assoc ⟩ | |
418 proj i o ( e o k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom ) | |
419 ≈⟨ cdr ( ek=h ( eqa e (id1 A p) (id1 A p ) ) ) ⟩ | |
420 proj i o product (prod p (FObj Γ) proj) (TMap t) | |
421 ≈⟨ pif=q (prod p (FObj Γ) proj) (TMap t) ⟩ | |
422 TMap t i | |
423 ∎ | |
291 | 424 limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {f : Hom A a lim} |
290 | 425 → ({i : Obj I} → A [ A [ TMap (limit-ε prod lim p e proj ) i o f ] ≈ TMap t i ]) → |
282 | 426 A [ limit1 a t ≈ f ] |
283 | 427 limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in begin |
428 limit1 a t | |
429 ≈⟨⟩ | |
430 k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom | |
431 ≈⟨ Equalizer.uniqueness (eqa e (id1 A p) (id1 A p )) ( begin | |
432 e o f | |
433 ≈↑⟨ ip-uniqueness (prod p (FObj Γ) proj) ⟩ | |
434 product (prod p (FObj Γ) proj) (λ i → ( proj i o ( e o f ) ) ) | |
284 | 435 ≈⟨ ip-cong (prod p (FObj Γ) proj) ( λ i → begin |
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
436 proj i o ( e o f ) |
284 | 437 ≈⟨ assoc ⟩ |
285
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
438 ( proj i o e ) o f |
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
439 ≈⟨ lim=t {i} ⟩ |
46d4ad55b948
commutativity continue...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
284
diff
changeset
|
440 TMap t i |
284 | 441 ∎ ) ⟩ |
283 | 442 product (prod p (FObj Γ) proj) (TMap t) |
443 ∎ ) ⟩ | |
444 f | |
445 ∎ | |
446 | |
291 | 447 ---- |
448 -- | |
449 -- Adjoint functor preserves limits | |
450 -- | |
451 -- | |
452 | |
453 open import Category.Cat | |
454 | |
455 ta1 : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) | |
456 ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → ( limit : Limit B I Γ lim tb ) → | |
457 ( U : Functor B A) → NTrans I A ( K A I (FObj U lim) ) (U ○ Γ) | |
458 ta1 B Γ lim tb limit U = record { | |
459 TMap = TMap (Functor*Nat I A U tb) ; | |
460 isNTrans = record { commute = λ {a} {b} {f} → let open ≈-Reasoning (A) in begin | |
461 FMap (U ○ Γ) f o TMap (Functor*Nat I A U tb) a | |
462 ≈⟨ nat ( Functor*Nat I A U tb ) ⟩ | |
463 TMap (Functor*Nat I A U tb) b o FMap (U ○ K B I lim) f | |
464 ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩ | |
465 TMap (Functor*Nat I A U tb) b o FMap (K A I (FObj U lim)) f | |
466 ∎ | |
467 } } | |
468 | |
469 adjoint-preseve-limit : | |
470 { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) | |
471 ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → ( limit : Limit B I Γ lim tb ) → | |
472 { U : Functor B A } { F : Functor A B } | |
473 { η : NTrans A A identityFunctor ( U ○ F ) } | |
474 { ε : NTrans B B ( F ○ U ) identityFunctor } → | |
475 ( adj : Adjunction A B U F η ε ) → Limit A I (U ○ Γ) (FObj U lim) (ta1 B Γ lim tb limit U ) | |
292 | 476 adjoint-preseve-limit B Γ lim tb limitb {U} {F} {η} {ε} adj = record { |
291 | 477 limit = λ a t → limit1 a t ; |
478 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; | |
479 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f | |
480 } where | |
292 | 481 ta = ta1 B Γ lim tb limitb U |
291 | 482 limit1 : (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → Hom A a (FObj U lim) |
483 limit1 a t = let open ≈-Reasoning (A) in ? | |
484 t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) (U ○ Γ)} {i : Obj I} → | |
485 A [ A [ TMap ta i o limit1 a t ] ≈ TMap t i ] | |
292 | 486 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in {!!} |
291 | 487 limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K A I a) (U ○ Γ)} {f : Hom A a (FObj U lim)} |
488 → ({i : Obj I} → A [ A [ TMap ta i o f ] ≈ TMap t i ]) → | |
489 A [ limit1 a t ≈ f ] | |
292 | 490 limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in {!!} |