Mercurial > hg > Members > kono > Proof > category

comparison pullback.agda @ 681:bd8f7346f252

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix Product and pullback
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 07 Nov 2017 17:12:08 +0900
parents 5d894993477f
children 50a01df1169a
comparison
equal deleted inserted replaced
680:5d894993477f 681:bd8f7346f252
28 28
29 open Equalizer 29 open Equalizer
30 open IsEqualizer 30 open IsEqualizer
31 open IsProduct 31 open IsProduct
32 32
33 pullback-from : (a b c ab d : Obj A) 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
36 pullback-from : {a b c : Obj A}
34 ( f : Hom A a c ) ( g : Hom A b c ) 37 ( f : Hom A a c ) ( g : Hom A b c )
35 ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( e : Hom A d ab ) 38 ( eqa : {a b : Obj A} → (f g : Hom A a b) → Equalizer A f g )
36 ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → IsEqualizer A e f g ) 39 ( prod : ( a b : Obj A ) → Product A a b ) → Pullback A f g
37 ( prod : IsProduct A a b ab π1 π2 ) → Pullback A a b c d f g 40 pullback-from {a} {b} {c} f g eqa prod0 = record {
38 ( A [ π1 o equalizer1 ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ) ] ) 41 ab = ab ;
39 ( A [ π2 o equalizer1 ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ) ] ) 42 π1 = A [ π1 o e ] ;
40 pullback-from a b c ab d f g π1 π2 e eqa prod = record { 43 π2 = A [ π2 o e ] ;
44 isPullback = record {
41 commute = commute1 ; 45 commute = commute1 ;
42 p = p1 ; 46 pullback = p1 ;
43 π1p=π1 = λ {d} {π1'} {π2'} {eq} → π1p=π11 {d} {π1'} {π2'} {eq} ; 47 π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} ; 48 π2p=π2 = λ {d} {π1'} {π2'} {eq} → π2p=π21 {d} {π1'} {π2'} {eq} ;
45 uniqueness = uniqueness1 49 uniqueness = uniqueness1
50 }
46 } where 51 } where
47 commute1 : A [ A [ f o A [ π1 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] 52 π1 = Product.π1 (prod0 a b )
48 ≈ A [ g o A [ π2 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ] 53 π2 = Product.π2 (prod0 a b )
54 e = equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]))
55 ab = equalizer-c (eqa (A [ f o π1 ]) (A [ g o π2 ]))
56 prod = Product.isProduct (prod0 a b)
57 commute1 : A [ A [ f o A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ]
58 ≈ A [ g o A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ]
49 commute1 = let open ≈-Reasoning (A) in 59 commute1 = let open ≈-Reasoning (A) in
50 begin 60 begin
51 f o ( π1 o equalizer1 (eqa ( f o π1 ) ( g o π2 )) ) 61 f o ( π1 o equalizer (eqa ( f o π1 ) ( g o π2 )) )
52 ≈⟨ assoc ⟩ 62 ≈⟨ assoc ⟩
53 ( f o π1 ) o equalizer1 (eqa ( f o π1 ) ( g o π2 )) 63 ( f o π1 ) o equalizer (eqa ( f o π1 ) ( g o π2 ))
54 ≈⟨ fe=ge (eqa (A [ f o π1 ]) (A [ g o π2 ])) ⟩ 64 ≈⟨ fe=ge (isEqualizer (eqa (A [ f o π1 ]) (A [ g o π2 ]))) ⟩
55 ( g o π2 ) o equalizer1 (eqa ( f o π1 ) ( g o π2 )) 65 ( g o π2 ) o equalizer (eqa ( f o π1 ) ( g o π2 ))
56 ≈↑⟨ assoc ⟩ 66 ≈↑⟨ assoc ⟩
57 g o ( π2 o equalizer1 (eqa ( f o π1 ) ( g o π2 )) ) 67 g o ( π2 o equalizer (eqa ( f o π1 ) ( g o π2 )) )
58 ∎ 68 ∎
59 lemma1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → 69 lemma1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] →
60 A [ A [ A [ f o π1 ] o (prod × π1') π2' ] ≈ A [ A [ g o π2 ] o (prod × π1') π2' ] ] 70 A [ A [ A [ f o π1 ] o (prod × π1') π2' ] ≈ A [ A [ g o π2 ] o (prod × π1') π2' ] ]
61 lemma1 {d'} { π1' } { π2' } eq = let open ≈-Reasoning (A) in 71 lemma1 {d'} { π1' } { π2' } eq = let open ≈-Reasoning (A) in
62 begin 72 begin
70 ≈↑⟨ cdr (π2fxg=g prod) ⟩ 80 ≈↑⟨ cdr (π2fxg=g prod) ⟩
71 g o ( π2 o (prod × π1') π2' ) 81 g o ( π2 o (prod × π1') π2' )
72 ≈⟨ assoc ⟩ 82 ≈⟨ assoc ⟩
73 ( g o π2 ) o (prod × π1') π2' 83 ( g o π2 ) o (prod × π1') π2'
74 ∎ 84 ∎
75 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 85 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
76 p1 {d'} { π1' } { π2' } eq = 86 p1 {d'} { π1' } { π2' } eq =
77 let open ≈-Reasoning (A) in k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) ( lemma1 eq ) 87 let open ≈-Reasoning (A) in k (isEqualizer (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ))) (_×_ prod π1' π2' ) ( lemma1 eq )
78 π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' ] ]} → 88 π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' ] ]} →
79 A [ A [ A [ π1 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π1' ] 89 A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) ) ] o p1 eq ] ≈ π1' ]
80 π1p=π11 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in 90 π1p=π11 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in
81 begin 91 begin
82 ( π1 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq 92 ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) ) ) o p1 eq
83 ≈⟨⟩ 93 ≈⟨⟩
84 ( π1 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) 94 ( π1 o e) o k (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) )) (_×_ prod π1' π2' ) (lemma1 eq)
85 ≈↑⟨ assoc ⟩ 95 ≈↑⟨ assoc ⟩
86 π1 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) ) 96 π1 o ( e o k (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) )) (_×_ prod π1' π2' ) (lemma1 eq) )
87 ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩ 97 ≈⟨ cdr ( ek=h (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ))) ⟩
88 π1 o (_×_ prod π1' π2' ) 98 π1 o (_×_ prod π1' π2' )
89 ≈⟨ π1fxg=f prod ⟩ 99 ≈⟨ π1fxg=f prod ⟩
90 π1' 100 π1'
91 ∎ 101 ∎
92 π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' ] ]} → 102 π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' ] ]} →
93 A [ A [ A [ π2 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π2' ] 103 A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) ) ] o p1 eq ] ≈ π2' ]
94 π2p=π21 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in 104 π2p=π21 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in
95 begin 105 begin
96 ( π2 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq 106 ( π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) ) ) o p1 eq
97 ≈⟨⟩ 107 ≈⟨⟩
98 ( π2 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) 108 ( π2 o e) o k (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) )) (_×_ prod π1' π2' ) (lemma1 eq)
99 ≈↑⟨ assoc ⟩ 109 ≈↑⟨ assoc ⟩
100 π2 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) ) 110 π2 o ( e o k (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) )) (_×_ prod π1' π2' ) (lemma1 eq) )
101 ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩ 111 ≈⟨ cdr ( ek=h (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ))) ⟩
102 π2 o (_×_ prod π1' π2' ) 112 π2 o (_×_ prod π1' π2' )
103 ≈⟨ π2fxg=g prod ⟩ 113 ≈⟨ π2fxg=g prod ⟩
104 π2' 114 π2'
105 ∎ 115 ∎
106 uniqueness1 : {d₁ : Obj A} (p' : Hom A d₁ d) {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} 116 uniqueness1 : {d₁ : Obj A} (p' : Hom A d₁ ab) {π1' : Hom A d₁ a} {π2' : Hom A d₁ b}
107 {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → 117 {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} →
108 {eq1 : A [ A [ A [ π1 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} → 118 {eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} →
109 {eq2 : A [ A [ A [ π2 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} → 119 {eq2 : A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} →
110 A [ p1 eq ≈ p' ] 120 A [ p1 eq ≈ p' ]
111 uniqueness1 {d'} p' {π1'} {π2'} {eq} {eq1} {eq2} = let open ≈-Reasoning (A) in 121 uniqueness1 {d'} p' {π1'} {π2'} {eq} {eq1} {eq2} = let open ≈-Reasoning (A) in
112 begin 122 begin
113 p1 eq 123 p1 eq
114 ≈⟨⟩ 124 ≈⟨⟩
115 k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) 125 k (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) )) (_×_ prod π1' π2' ) (lemma1 eq)
116 ≈⟨ IsEqualizer.uniqueness (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e}) ( begin 126 ≈⟨ IsEqualizer.uniqueness (isEqualizer (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) )) ( begin
117 e o p' 127 e o p'
118 ≈⟨⟩ 128 ≈⟨⟩
119 equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p' 129 equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p'
120 ≈↑⟨ IsProduct.uniqueness prod ⟩ 130 ≈↑⟨ IsProduct.uniqueness prod ⟩
121 (prod × ( π1 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p') ) ( π2 o (equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p')) 131 (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'))
122 ≈⟨ ×-cong prod (assoc) (assoc) ⟩ 132 ≈⟨ ×-cong prod (assoc) (assoc) ⟩
123 (prod × (A [ A [ π1 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ])) 133 (prod × (A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]))
124 (A [ A [ π2 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]) 134 (A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ])
125 ≈⟨ ×-cong prod eq1 eq2 ⟩ 135 ≈⟨ ×-cong prod eq1 eq2 ⟩
126 ((prod × π1') π2') 136 ((prod × π1') π2')
127 ∎ ) ⟩ 137 ∎ ) ⟩
128 p' 138 p'
129 ∎ 139 ∎