Mercurial > hg > Members > kono > Proof > category

comparison pullback.agda @ 672:749df4959d19

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix completeness
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Nov 2017 09:00:01 +0900
parents 3ce21b2a671a
children 0007f9a25e9c
comparison
equal deleted inserted replaced
671:959954fc29f8 672:749df4959d19
26 -- d <------------------ d' 26 -- d <------------------ d'
27 -- k (π1' × π2' ) 27 -- k (π1' × π2' )
28 28
29 open Equalizer 29 open Equalizer
30 open IsEqualizer 30 open IsEqualizer
31 open Product 31 open IsProduct
32 open Pullback 32 open Pullback
33 33
34 pullback-from : (a b c ab d : Obj A) 34 pullback-from : (a b c ab d : Obj A)
35 ( f : Hom A a c ) ( g : Hom A b c ) 35 ( f : Hom A a c ) ( g : Hom A b c )
36 ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( e : Hom A d ab ) 36 ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( e : Hom A d ab )
37 ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → IsEqualizer A e f g ) 37 ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → IsEqualizer A e f g )
38 ( prod : Product A a b ab π1 π2 ) → Pullback A a b c d f g 38 ( prod : IsProduct A a b ab π1 π2 ) → Pullback A a b c d f g
39 ( A [ π1 o equalizer1 ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ) ] ) 39 ( A [ π1 o equalizer1 ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ) ] )
40 ( A [ π2 o equalizer1 ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ) ] ) 40 ( A [ π2 o equalizer1 ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ) ] )
41 pullback-from a b c ab d f g π1 π2 e eqa prod = record { 41 pullback-from a b c ab d f g π1 π2 e eqa prod = record {
42 commute = commute1 ; 42 commute = commute1 ;
43 p = p1 ; 43 p = p1 ;
116 k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) 116 k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq)
117 ≈⟨ IsEqualizer.uniqueness (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e}) ( begin 117 ≈⟨ IsEqualizer.uniqueness (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e}) ( begin
118 e o p' 118 e o p'
119 ≈⟨⟩ 119 ≈⟨⟩
120 equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p' 120 equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p'
121 ≈↑⟨ Product.uniqueness prod ⟩ 121 ≈↑⟨ IsProduct.uniqueness prod ⟩
122 (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')) 122 (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'))
123 ≈⟨ ×-cong prod (assoc) (assoc) ⟩ 123 ≈⟨ ×-cong prod (assoc) (assoc) ⟩
124 (prod × (A [ A [ π1 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ])) 124 (prod × (A [ A [ π1 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]))
125 (A [ A [ π2 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]) 125 (A [ A [ π2 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ])
126 ≈⟨ ×-cong prod eq1 eq2 ⟩ 126 ≈⟨ ×-cong prod eq1 eq2 ⟩
287 ≈⟨ ( coIsUniversalMapping.couniquness ( iscoUniversalMapping univ) ) εf=t ⟩ 287 ≈⟨ ( coIsUniversalMapping.couniquness ( iscoUniversalMapping univ) ) εf=t ⟩
288 f 288 f
289 ∎ 289 ∎
290 290
291 291
292 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 ) → 292 lemma-p0 : (a b ab : Obj A) ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( prod : IsProduct A a b ab π1 π2 ) →
293 A [ _×_ prod π1 π2 ≈ id1 A ab ] 293 A [ _×_ prod π1 π2 ≈ id1 A ab ]
294 lemma-p0 a b ab π1 π2 prod = let open ≈-Reasoning (A) in begin 294 lemma-p0 a b ab π1 π2 prod = let open ≈-Reasoning (A) in begin
295 _×_ prod π1 π2 295 _×_ prod π1 π2
296 ≈↑⟨ ×-cong prod idR idR ⟩ 296 ≈↑⟨ ×-cong prod idR idR ⟩
297 _×_ prod (A [ π1 o id1 A ab ]) (A [ π2 o id1 A ab ]) 297 _×_ prod (A [ π1 o id1 A ab ]) (A [ π2 o id1 A ab ])
298 ≈⟨ Product.uniqueness prod ⟩ 298 ≈⟨ IsProduct.uniqueness prod ⟩
299 id1 A ab 299 id1 A ab
300 ∎ 300 ∎
301 301
302 302
303 open IProduct 303 open IProduct