Mercurial > hg > Members > kono > Proof > category

comparison pullback.agda @ 683:88e8a1290dc4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 08 Nov 2017 00:05:50 +0900
parents 50a01df1169a
children 5d9d7c2f2718
comparison
equal deleted inserted replaced
682:50a01df1169a 683:88e8a1290dc4
27 -- k (π1' × π2' ) 27 -- k (π1' × π2' )
28 28
29 open Equalizer 29 open Equalizer
30 open IsEqualizer 30 open IsEqualizer
31 open IsProduct 31 open IsProduct
32
33 -- ( A [ π1 o equalizer1 ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ) ] )
34 -- ( A [ π2 o equalizer1 ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ) ] )
35 32
36 pullback-from : {a b c : Obj A} 33 pullback-from : {a b c : Obj A}
37 ( f : Hom A a c ) ( g : Hom A b c ) 34 ( f : Hom A a c ) ( g : Hom A b c )
38 ( eqa : {a b : Obj A} → (f g : Hom A a b) → Equalizer A f g ) 35 ( eqa : {a b : Obj A} → (f g : Hom A a b) → Equalizer A f g )
39 ( prod : ( a b : Obj A ) → Product A a b ) → Pullback A f g 36 ( prod : ( a b : Obj A ) → Product A a b ) → Pullback A f g
379 d : Obj A 376 d : Obj A
380 d = equalizer-c equ-ε 377 d = equalizer-c equ-ε
381 e : Hom A d p0 378 e : Hom A d p0
382 e = equalizer equ-ε 379 e = equalizer equ-ε
383 equ = isEqualizer equ-ε 380 equ = isEqualizer equ-ε
381 -- projection of the product of Obj I
384 proj : (i : Obj I) → Hom A p0 (FObj Γ i) 382 proj : (i : Obj I) → Hom A p0 (FObj Γ i)
385 proj = pi ( prod (FObj Γ) ) 383 proj = pi ( prod (FObj Γ) )
386 prodΓ = isIProduct ( prod (FObj Γ) ) 384 prodΓ = isIProduct ( prod (FObj Γ) )
385 -- projection of the product of Hom I
387 mu : {j k : Obj I} → (u : Hom I j k ) → Hom A (iprod (prod Fcod)) (Fcod (Homprod u)) 386 mu : {j k : Obj I} → (u : Hom I j k ) → Hom A (iprod (prod Fcod)) (Fcod (Homprod u))
388 mu u = pi (prod Fcod ) (Homprod u) 387 mu u = pi (prod Fcod ) (Homprod u)
389 limit-ε : NTrans I A (K A I (equalizer-c equ-ε ) ) Γ 388 limit-ε : NTrans I A (K A I (equalizer-c equ-ε ) ) Γ
390 limit-ε = record { 389 limit-ε = record {
391 TMap = λ i → tmap i ; 390 TMap = λ i → tmap i ;
416 ≈↑⟨ idR ⟩ 415 ≈↑⟨ idR ⟩
417 (proj k o e ) o id1 A d 416 (proj k o e ) o id1 A d
418 ≈⟨⟩ 417 ≈⟨⟩
419 tmap k o FMap (K A I d) u 418 tmap k o FMap (K A I d) u
420 ∎ 419 ∎
420 -- an arrow to our product of Obj I ( is an equalizer because of commutativity of t )
421 h : {a : Obj A} → (t : NTrans I A (K A I a) Γ ) → Hom A a p0
422 h t = iproduct prodΓ (TMap t)
421 fh=gh : (a : Obj A) → (t : NTrans I A (K A I a) Γ ) → 423 fh=gh : (a : Obj A) → (t : NTrans I A (K A I a) Γ ) →
422 A [ A [ g o iproduct prodΓ (TMap t) ] ≈ A [ f o iproduct prodΓ (TMap t) ] ] 424 A [ A [ g o h t ] ≈ A [ f o h t ] ]
423 fh=gh a t = let open ≈-Reasoning (A) in begin 425 fh=gh a t = let open ≈-Reasoning (A) in begin
424 g o iproduct prodΓ (TMap t) 426 g o h t
425 ≈↑⟨ ip-uniqueness (isIProduct (prod Fcod)) ⟩ 427 ≈↑⟨ ip-uniqueness (isIProduct (prod Fcod)) ⟩
426 iproduct (isIProduct (prod Fcod)) (λ u → pi (prod Fcod) u o ( g o iproduct prodΓ (TMap t) )) 428 iproduct (isIProduct (prod Fcod)) (λ u → pi (prod Fcod) u o ( g o h t ))
427 ≈⟨ ip-cong (isIProduct (prod Fcod)) ( λ u → begin 429 ≈⟨ ip-cong (isIProduct (prod Fcod)) ( λ u → begin
428 pi (prod Fcod) u o ( g o iproduct prodΓ (TMap t) ) 430 pi (prod Fcod) u o ( g o h t )
429 ≈⟨ assoc ⟩ 431 ≈⟨ assoc ⟩
430 ( pi (prod Fcod) u o g ) o iproduct prodΓ (TMap t) 432 ( pi (prod Fcod) u o g ) o h t
431 ≈⟨ car (pif=q (isIProduct (prod Fcod ))) ⟩ 433 ≈⟨ car (pif=q (isIProduct (prod Fcod ))) ⟩
432 (FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u) ) o iproduct prodΓ (TMap t) 434 (FMap Γ (hom u) o pi (prod (FObj Γ)) (hom-j u) ) o h t
433 ≈↑⟨ assoc ⟩ 435 ≈↑⟨ assoc ⟩
434 FMap Γ (hom u) o (pi (prod (FObj Γ)) (hom-j u) o iproduct prodΓ (TMap t) ) 436 FMap Γ (hom u) o (pi (prod (FObj Γ)) (hom-j u) o h t )
435 ≈⟨ cdr ( pif=q prodΓ ) ⟩ 437 ≈⟨ cdr ( pif=q prodΓ ) ⟩
436 FMap Γ (hom u) o TMap t (hom-j u) 438 FMap Γ (hom u) o TMap t (hom-j u)
437 ≈⟨ IsNTrans.commute (isNTrans t) ⟩ 439 ≈⟨ IsNTrans.commute (isNTrans t) ⟩
438 TMap t (hom-k u) o id1 A a 440 TMap t (hom-k u) o id1 A a
439 ≈⟨ idR ⟩ 441 ≈⟨ idR ⟩
440 TMap t (hom-k u) 442 TMap t (hom-k u)
441 ≈↑⟨ pif=q prodΓ ⟩ 443 ≈↑⟨ pif=q prodΓ ⟩
442 pi (prod (FObj Γ)) (hom-k u) o iproduct prodΓ (TMap t) 444 pi (prod (FObj Γ)) (hom-k u) o h t
443 ≈↑⟨ car (pif=q (isIProduct (prod Fcod ))) ⟩ 445 ≈↑⟨ car (pif=q (isIProduct (prod Fcod ))) ⟩
444 (pi (prod Fcod) u o f ) o iproduct prodΓ (TMap t) 446 (pi (prod Fcod) u o f ) o h t
445 ≈↑⟨ assoc ⟩ 447 ≈↑⟨ assoc ⟩
446 pi (prod Fcod) u o ( f o iproduct prodΓ (TMap t) ) 448 pi (prod Fcod) u o ( f o h t )
447 ∎ 449 ∎
448 ) ⟩ 450 ) ⟩
449 iproduct (isIProduct (prod Fcod)) (λ u → pi (prod Fcod) u o ( f o iproduct prodΓ (TMap t)) ) 451 iproduct (isIProduct (prod Fcod)) (λ u → pi (prod Fcod) u o ( f o h t ))
450 ≈⟨ ip-uniqueness (isIProduct (prod Fcod)) ⟩ 452 ≈⟨ ip-uniqueness (isIProduct (prod Fcod)) ⟩
451 f o iproduct prodΓ (TMap t) 453 f o h t
452 ∎ 454 ∎
453 limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a d 455 limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a d
454 limit1 a t = k equ (iproduct prodΓ (TMap t) ) ( fh=gh a t ) 456 limit1 a t = k equ (h t) ( fh=gh a t )
455 t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} → 457 t0f=t1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} →
456 A [ A [ TMap limit-ε i o limit1 a t ] ≈ TMap t i ] 458 A [ A [ TMap limit-ε i o limit1 a t ] ≈ TMap t i ]
457 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin 459 t0f=t1 {a} {t} {i} = let open ≈-Reasoning (A) in begin
458 TMap limit-ε i o limit1 a t 460 TMap limit-ε i o limit1 a t
459 ≈⟨⟩ 461 ≈⟨⟩
460 ( ( proj i ) o e ) o k equ (iproduct prodΓ (TMap t) ) (fh=gh a t) 462 ( ( proj i ) o e ) o k equ (h t) (fh=gh a t)
461 ≈↑⟨ assoc ⟩ 463 ≈↑⟨ assoc ⟩
462 proj i o ( e o k equ (iproduct prodΓ (TMap t) ) (fh=gh a t ) ) 464 proj i o ( e o k equ (h t) (fh=gh a t ) )
463 ≈⟨ cdr ( ek=h equ) ⟩ 465 ≈⟨ cdr ( ek=h equ) ⟩
464 proj i o iproduct prodΓ (TMap t) 466 proj i o h t
465 ≈⟨ pif=q prodΓ ⟩ 467 ≈⟨ pif=q prodΓ ⟩
466 TMap t i 468 TMap t i
467 ∎ 469 ∎
468 limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {f : Hom A a d} 470 limit-uniqueness1 : {a : Obj A} {t : NTrans I A (K A I a) Γ} {f : Hom A a d}
469 → ({i : Obj I} → A [ A [ TMap limit-ε i o f ] ≈ TMap t i ]) → 471 → ({i : Obj I} → A [ A [ TMap limit-ε i o f ] ≈ TMap t i ]) →
470 A [ limit1 a t ≈ f ] 472 A [ limit1 a t ≈ f ]
471 limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in begin 473 limit-uniqueness1 {a} {t} {f} lim=t = let open ≈-Reasoning (A) in begin
472 limit1 a t 474 limit1 a t
473 ≈⟨⟩ 475 ≈⟨⟩
474 k equ (iproduct prodΓ (TMap t) ) (fh=gh a t) 476 k equ (h t) (fh=gh a t)
475 ≈⟨ IsEqualizer.uniqueness equ ( begin 477 ≈⟨ IsEqualizer.uniqueness equ ( begin
476 e o f 478 e o f
477 ≈↑⟨ ip-uniqueness prodΓ ⟩ 479 ≈↑⟨ ip-uniqueness prodΓ ⟩
478 iproduct prodΓ (λ i → ( proj i o ( e o f ) ) ) 480 iproduct prodΓ (λ i → ( proj i o ( e o f ) ) )
479 ≈⟨ ip-cong prodΓ ( λ i → begin 481 ≈⟨ ip-cong prodΓ ( λ i → begin
481 ≈⟨ assoc ⟩ 483 ≈⟨ assoc ⟩
482 ( proj i o e ) o f 484 ( proj i o e ) o f
483 ≈⟨ lim=t {i} ⟩ 485 ≈⟨ lim=t {i} ⟩
484 TMap t i 486 TMap t i
485 ∎ ) ⟩ 487 ∎ ) ⟩
486 iproduct prodΓ (TMap t) 488 h t
487 ∎ ) ⟩ 489 ∎ ) ⟩
488 f 490 f
489 ∎ 491 ∎
490 492
491 493