Mercurial > hg > Members > kono > Proof > category

comparison pullback.agda @ 303:7f40d6a51c72

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Limit form equalizer and product done. Use equalizer to provle naturality of limit-ε
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 04 Nov 2013 14:46:07 +0900
parents c5b2656dbec6
children 702adc45704f
comparison
equal deleted inserted replaced
302:c5b2656dbec6 303:7f40d6a51c72
312 _*' univ t 312 _*' univ t
313 ≈⟨ ( coIsUniversalMapping.couniquness ( iscoUniversalMapping univ) ) εf=t ⟩ 313 ≈⟨ ( coIsUniversalMapping.couniquness ( iscoUniversalMapping univ) ) εf=t ⟩
314 f 314 f
315 ∎ 315 ∎
316 316
317
318 lemma-p0 : (a b ab : Obj A) ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( prod : Product A a b ab π1 π2 ) →
319 A [ _×_ prod π1 π2 ≈ id1 A ab ]
320 lemma-p0 a b ab π1 π2 prod = let open ≈-Reasoning (A) in begin
321 _×_ prod π1 π2
322 ≈↑⟨ ×-cong prod idR idR ⟩
323 _×_ prod (A [ π1 o id1 A ab ]) (A [ π2 o id1 A ab ])
324 ≈⟨ Product.uniqueness prod ⟩
325 id1 A ab
326 ∎
327
328
317 ----- 329 -----
318 -- 330 --
319 -- product on arbitrary index 331 -- product on arbitrary index
320 -- 332 --
321 333
325 ( pi : (i : I ) → Hom A p ( ai i ) ) -- projections 337 ( pi : (i : I ) → Hom A p ( ai i ) ) -- projections
326 : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where 338 : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where
327 field 339 field
328 product : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p 340 product : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p
329 pif=q : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i ) o ( product qi ) ] ≈ (qi i) ] 341 pif=q : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i ) o ( product qi ) ] ≈ (qi i) ]
330 -- special case of product ( qi = pi ) ( should b proved from pif=q )
331 -- we cannot prove this because qi/pi cannot be interleaved , should be the way to prove
332 pif=q1 : { i : I } → { qi : Hom A p (ai i) } → A [ pi i ≈ qi ]
333 ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ product ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ] 342 ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ product ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ]
334 ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } 343 ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) }
335 → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ product qi ≈ product qi' ] 344 → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ product qi ≈ product qi' ]
336 -- another form of uniquness 345 -- another form of uniquness
337 ip-uniquness1 : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ( product' : Hom A q p ) 346 ip-uniqueness1 : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ( product' : Hom A q p )
338 → ( ∀ { i : I } → A [ A [ ( pi i ) o product' ] ≈ (qi i) ] ) 347 → ( ∀ { i : I } → A [ A [ ( pi i ) o product' ] ≈ (qi i) ] )
339 → A [ product' ≈ product qi ] 348 → A [ product' ≈ product qi ]
340 ip-uniquness1 {a} qi product' eq = let open ≈-Reasoning (A) in begin 349 ip-uniqueness1 {a} qi product' eq = let open ≈-Reasoning (A) in begin
341 product' 350 product'
342 ≈↑⟨ ip-uniqueness ⟩ 351 ≈↑⟨ ip-uniqueness ⟩
343 product (λ i₁ → A [ pi i₁ o product' ]) 352 product (λ i₁ → A [ pi i₁ o product' ])
344 ≈⟨ ip-cong ( λ i → begin 353 ≈⟨ ip-cong ( λ i → begin
345 pi i o product' 354 pi i o product'
346 ≈⟨ eq {i} ⟩ 355 ≈⟨ eq {i} ⟩
347 qi i 356 qi i
348 ∎ ) ⟩ 357 ∎ ) ⟩
349 product qi 358 product qi
350 ∎ 359 ∎
351 pif=q1' : { i : I } → { qi : (j : I ) → Hom A p (ai j) } → A [ pi i ≈ qi i ]
352 pif=q1' {i} {qi} = let open ≈-Reasoning (A) in begin
353 pi i
354 ≈↑⟨ idR ⟩
355 pi i o id1 A p
356 ≈⟨ cdr ( ip-uniquness1 {p} qi (id1 A p) ( begin
357 pi ? o id1 A p
358 ≈⟨ {!!} ⟩
359 qi ?
360 ∎ )) ⟩
361 pi i o product qi
362 ≈⟨ pif=q {p} qi {i} ⟩
363 qi i
364 ∎
365 360
366 open IProduct 361 open IProduct
367 open Equalizer 362 open Equalizer
368 363
369 -- 364 --
373 -- ai 368 -- ai
374 -- ^ K f = id lim 369 -- ^ K f = id lim
375 -- | pi lim = K i -----------→ K j = lim 370 -- | pi lim = K i -----------→ K j = lim
376 -- | | | 371 -- | | |
377 -- p | | 372 -- p | |
378 -- ^ ε i | | ε j 373 -- ^ proj i o e = ε i | | ε j = proj j o e
379 -- | | | 374 -- | | |
380 -- | e = equalizer (id p) (id p) | | 375 -- | e = equalizer (id p) (id p) | |
381 -- | v v 376 -- | v v
382 -- lim <------------------ d' a i = Γ i -----------→ Γ j = a j 377 -- lim <------------------ d' a i = Γ i -----------→ Γ j = a j
383 -- k ( product pi ) Γ f 378 -- k ( product pi ) Γ f
384 -- Γ f o ε i = ε j 379 -- Γ f o ε i = ε j
385 -- 380 --
386 --
387
388 -- pi-ε -- : ( prod : (p : Obj A) ( ai : Obj I → Obj A ) ( pi : (i : Obj I) → Hom A p ( ai i ) )
389 -- → IProduct {c₁'} A (Obj I) p ai pi )
390 -- ( lim p : Obj A ) ( e : Hom A lim p )
391 -- ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) →
392 -- { i : Obj I } → { q : ( i : Obj I ) → Hom A p (FObj Γ i) } → A [ proj i ≈ q i ]
393 -- pi-ε prod lim p e proj {i} {q} = let open ≈-Reasoning (A) in begin
394 -- proj i
395 -- ≈↑⟨ idR ⟩
396 -- proj i o id1 A p
397 -- ≈⟨ cdr {!!} ⟩
398 -- proj i o product (prod p (FObj Γ) proj) q
399 -- ≈⟨ pif=q (prod p (FObj Γ) proj) q ⟩
400 -- q i
401 -- ∎
402
403 381
404 limit-ε : 382 limit-ε :
405 ( prod : (p : Obj A) ( ai : Obj I → Obj A ) ( pi : (i : Obj I) → Hom A p ( ai i ) ) 383 ( eqa : {a b c : Obj A} → (e : Hom A c a ) → (f g : Hom A a b) → Equalizer A e f g )
406 → IProduct {c₁'} A (Obj I) p ai pi )
407 ( lim p : Obj A ) ( e : Hom A lim p ) 384 ( lim p : Obj A ) ( e : Hom A lim p )
408 ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) → 385 ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) →
409 NTrans I A (K A I lim) Γ 386 NTrans I A (K A I lim) Γ
410 limit-ε prod lim p e proj = record { 387 limit-ε eqa lim p e proj = record {
411 TMap = tmap ; 388 TMap = tmap ;
412 isNTrans = record { 389 isNTrans = record { commute = commute1 }
413 commute = commute1
414 }
415 } where 390 } where
416 tmap : (i : Obj I) → Hom A (FObj (K A I lim) i) (FObj Γ i) 391 tmap : (i : Obj I) → Hom A (FObj (K A I lim) i) (FObj Γ i)
417 tmap i = A [ proj i o e ] 392 tmap i = A [ proj i o e ]
418 commute1 : {i j : Obj I} {f : Hom I i j} → 393 commute1 : {i j : Obj I} {f : Hom I i j} →
419 A [ A [ FMap Γ f o tmap i ] ≈ A [ tmap j o FMap (K A I lim) f ] ] 394 A [ A [ FMap Γ f o tmap i ] ≈ A [ tmap j o FMap (K A I lim) f ] ]
421 FMap Γ f o tmap i 396 FMap Γ f o tmap i
422 ≈⟨⟩ 397 ≈⟨⟩
423 FMap Γ f o ( proj i o e ) 398 FMap Γ f o ( proj i o e )
424 ≈⟨ assoc ⟩ 399 ≈⟨ assoc ⟩
425 ( FMap Γ f o proj i ) o e 400 ( FMap Γ f o proj i ) o e
426 ≈↑⟨ car ( pif=q1 ( prod p (FObj Γ) proj ) {j} ) ⟩ 401 ≈⟨ fe=ge ( eqa e (FMap Γ f o proj i) ( proj j )) ⟩
427 proj j o e 402 proj j o e
428 ≈↑⟨ idR ⟩ 403 ≈↑⟨ idR ⟩
429 (proj j o e ) o id1 A lim 404 (proj j o e ) o id1 A lim
430 ≈⟨⟩ 405 ≈⟨⟩
431 tmap j o FMap (K A I lim) f 406 tmap j o FMap (K A I lim) f
436 → IProduct {c₁'} A (Obj I) p ai pi ) 411 → IProduct {c₁'} A (Obj I) p ai pi )
437 ( eqa : {a b c : Obj A} → (e : Hom A c a ) → (f g : Hom A a b) → Equalizer A e f g ) 412 ( eqa : {a b c : Obj A} → (e : Hom A c a ) → (f g : Hom A a b) → Equalizer A e f g )
438 ( lim p : Obj A ) -- limit to be made 413 ( lim p : Obj A ) -- limit to be made
439 ( e : Hom A lim p ) -- existing of equalizer 414 ( e : Hom A lim p ) -- existing of equalizer
440 ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) -- existing of product ( projection actually ) 415 ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) -- existing of product ( projection actually )
441 → Limit A I Γ lim ( limit-ε prod lim p e proj ) 416 → Limit A I Γ lim ( limit-ε eqa lim p e proj )
442 limit-from prod eqa lim p e proj = record { 417 limit-from prod eqa lim p e proj = record {
443 limit = λ a t → limit1 a t ; 418 limit = λ a t → limit1 a t ;
444 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; 419 t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ;
445 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f 420 limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
446 } where 421 } where
447 limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a lim 422 limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a lim
448 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 423 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
449 t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} → 424 t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} →
450 A [ A [ TMap (limit-ε prod lim p e proj ) i o limit1 a t ] ≈ TMap t i ] 425 A [ A [ TMap (limit-ε eqa lim p e proj ) i o limit1 a t ] ≈ TMap t i ]
451 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin 426 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin
452 TMap (limit-ε prod lim p e proj ) i o limit1 a t 427 TMap (limit-ε eqa lim p e proj ) i o limit1 a t
453 ≈⟨⟩ 428 ≈⟨⟩
454 ( ( proj i ) o e ) o k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom 429 ( ( proj i ) o e ) o k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom
455 ≈↑⟨ assoc ⟩ 430 ≈↑⟨ assoc ⟩
456 proj i o ( e o k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom ) 431 proj i o ( e o k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom )
457 ≈⟨ cdr ( ek=h ( eqa e (id1 A p) (id1 A p ) ) ) ⟩ 432 ≈⟨ cdr ( ek=h ( eqa e (id1 A p) (id1 A p ) ) ) ⟩
458 proj i o product (prod p (FObj Γ) proj) (TMap t) 433 proj i o product (prod p (FObj Γ) proj) (TMap t)
459 ≈⟨ pif=q (prod p (FObj Γ) proj) (TMap t) ⟩ 434 ≈⟨ pif=q (prod p (FObj Γ) proj) (TMap t) ⟩
460 TMap t i 435 TMap t i
461 ∎ 436 ∎
462 limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {f : Hom A a lim} 437 limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {f : Hom A a lim}
463 → ({i : Obj I} → A [ A [ TMap (limit-ε prod lim p e proj ) i o f ] ≈ TMap t i ]) → 438 → ({i : Obj I} → A [ A [ TMap (limit-ε eqa lim p e proj ) i o f ] ≈ TMap t i ]) →
464 A [ limit1 a t ≈ f ] 439 A [ limit1 a t ≈ f ]
465 limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in begin 440 limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in begin
466 limit1 a t 441 limit1 a t
467 ≈⟨⟩ 442 ≈⟨⟩
468 k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom 443 k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ) proj ) (TMap t) ) refl-hom