Mercurial > hg > Members > kono > Proof > category

comparison pullback.agda @ 261:a2477147dfec

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
pull back continue
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 20 Sep 2013 16:55:22 +0900
parents a87d3ea9efe4
children e1b08c5e4d2e
comparison
equal deleted inserted replaced
260:a87d3ea9efe4 261:a2477147dfec
22 -- ^ π2 22 -- ^ π2
23 -- | 23 -- |
24 -- d 24 -- d
25 -- 25 --
26 26
27 pullback-from : (a b c ab : Obj A) 27 open Equalizer
28 open Product
29 open Pullback
30
31 pullback-from : (a b c ab d : Obj A)
28 ( f : Hom A a c ) ( g : Hom A b c ) 32 ( f : Hom A a c ) ( g : Hom A b c )
29 ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) 33 ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( e : Hom A d ab )
30 ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g ) 34 ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g )
31 ( prod : Product A a b ab π1 π2 ) → Pullback A a b c ab f g π1 π2 35 ( prod : Product A a b ab π1 π2 ) → Pullback A a b c d f g
32 pullback-from a b c ab f g π1 π2 eqa prod = record { 36 ( A [ π1 o equalizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ){e} ) ] )
37 ( A [ π2 o equalizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ){e} ) ] )
38 pullback-from a b c ab d f g π1 π2 e eqa prod = record {
33 commute = commute1 ; 39 commute = commute1 ;
34 p = p1 ; 40 p = p1 ;
35 π1p=π1 = π1p=π11 ; 41 π1p=π1 = λ {d} {π1'} {π2'} {eq} → π1p=π11 {d} {π1'} {π2'} {eq} ;
36 π2p=π2 = π2p=π21 ; 42 π2p=π2 = λ {d} {π1'} {π2'} {eq} → π2p=π21 {d} {π1'} {π2'} {eq} ;
37 uniqueness = uniqueness1 43 uniqueness = uniqueness1
38 } where 44 } where
39 commute1 : A [ A [ f o π1 ] ≈ A [ g o π2 ] ] 45 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 ])) ] ] ]
40 commute1 = ? 46 commute1 = {!!}
41 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 ab 47 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
42 p1 {d} { π1' } { π2' } eq = ? 48 p1 {d'} { π1' } { π2' } eq = -- _×_ prod π1' π2'
43 π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' ] ] } 49 π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' ] ]} → A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π1' ]
44 → A [ A [ π1 o p1 eq ] ≈ π1' ] 50 π1p=π11 = {!!} -- π1fxg=f prod
45 π1p=π11 { d } { π1' } { π2' } { eq } = ? 51 π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' ] ]} → A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π2' ]
46 π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' ] ] } 52 π2p=π21 = {!!} -- π2fxg=g prod
47 → A [ A [ π2 o p1 eq ] ≈ π2' ] 53 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' ] ]} →
48 π2p=π21 { d } { π1' } { π2' } { eq } = ? 54 {eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} →
49 uniqueness1 : { d : Obj A } → ( p' : Hom A d ab ) → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } 55 {eq2 : A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} →
50 → { π1p=π1' : A [ A [ π1 o p' ] ≈ π1' ] } 56 A [ p1 eq ≈ p' ]
51 → { π2p=π2' : A [ A [ π2 o p' ] ≈ π2' ] } 57 uniqueness1 = {!!}
52 → A [ p1 eq ≈ p' ]
53 uniqueness1 { d } p' { π1' } { π2' } { eq }{ π1p=π1' } { π2p=π2' } = ?