|
260
|
1 -- Pullback from product and equalizer
|
|
|
2 --
|
|
|
3 --
|
|
|
4 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
|
|
|
5 ----
|
|
|
6
|
|
|
7 open import Category -- https://github.com/konn/category-agda
|
|
|
8 open import Level
|
|
|
9 module pullback { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where
|
|
|
10
|
|
|
11 open import HomReasoning
|
|
|
12 open import cat-utility
|
|
|
13
|
|
|
14 --
|
|
|
15 -- Pullback
|
|
|
16 -- f
|
|
|
17 -- a -------> c
|
|
|
18 -- ^ ^
|
|
|
19 -- π1 | |g
|
|
|
20 -- | |
|
|
|
21 -- ab -------> b
|
|
|
22 -- ^ π2
|
|
|
23 -- |
|
|
262
|
24 -- | equalizer (f π1) (g π1) = ( π1' × π2' )
|
|
260
|
25 -- d
|
|
|
26 --
|
|
|
27
|
|
261
|
28 open Equalizer
|
|
|
29 open Product
|
|
|
30 open Pullback
|
|
|
31
|
|
|
32 pullback-from : (a b c ab d : Obj A)
|
|
260
|
33 ( f : Hom A a c ) ( g : Hom A b c )
|
|
261
|
34 ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( e : Hom A d ab )
|
|
260
|
35 ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g )
|
|
261
|
36 ( prod : Product A a b ab π1 π2 ) → Pullback A a b c d f g
|
|
|
37 ( A [ π1 o equalizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ){e} ) ] )
|
|
|
38 ( A [ π2 o equalizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ){e} ) ] )
|
|
|
39 pullback-from a b c ab d f g π1 π2 e eqa prod = record {
|
|
260
|
40 commute = commute1 ;
|
|
|
41 p = p1 ;
|
|
261
|
42 π1p=π1 = λ {d} {π1'} {π2'} {eq} → π1p=π11 {d} {π1'} {π2'} {eq} ;
|
|
|
43 π2p=π2 = λ {d} {π1'} {π2'} {eq} → π2p=π21 {d} {π1'} {π2'} {eq} ;
|
|
260
|
44 uniqueness = uniqueness1
|
|
|
45 } where
|
|
261
|
46 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 ])) ] ] ]
|
|
262
|
47 commute1 = let open ≈-Reasoning (A) in
|
|
|
48 begin
|
|
|
49 f o ( π1 o equalizer (eqa ( f o π1 ) ( g o π2 )) )
|
|
|
50 ≈⟨ assoc ⟩
|
|
|
51 ( f o π1 ) o equalizer (eqa ( f o π1 ) ( g o π2 ))
|
|
|
52 ≈⟨ fe=ge (eqa (A [ f o π1 ]) (A [ g o π2 ])) ⟩
|
|
|
53 ( g o π2 ) o equalizer (eqa ( f o π1 ) ( g o π2 ))
|
|
|
54 ≈↑⟨ assoc ⟩
|
|
|
55 g o ( π2 o equalizer (eqa ( f o π1 ) ( g o π2 )) )
|
|
|
56 ∎
|
|
|
57 lemma1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] →
|
|
|
58 A [ A [ A [ f o π1 ] o (prod × π1') π2' ] ≈ A [ A [ g o π2 ] o (prod × π1') π2' ] ]
|
|
|
59 lemma1 {d'} { π1' } { π2' } eq = let open ≈-Reasoning (A) in
|
|
|
60 begin
|
|
|
61 ( f o π1 ) o (prod × π1') π2'
|
|
|
62 ≈↑⟨ assoc ⟩
|
|
|
63 f o ( π1 o (prod × π1') π2' )
|
|
|
64 ≈⟨ cdr (π1fxg=f prod) ⟩
|
|
|
65 f o π1'
|
|
|
66 ≈⟨ eq ⟩
|
|
|
67 g o π2'
|
|
|
68 ≈↑⟨ cdr (π2fxg=g prod) ⟩
|
|
|
69 g o ( π2 o (prod × π1') π2' )
|
|
|
70 ≈⟨ assoc ⟩
|
|
|
71 ( g o π2 ) o (prod × π1') π2'
|
|
|
72 ∎
|
|
261
|
73 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
|
|
262
|
74 p1 {d'} { π1' } { π2' } eq =
|
|
|
75 let open ≈-Reasoning (A) in k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) ( lemma1 eq )
|
|
|
76 π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' ] ]} →
|
|
|
77 A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π1' ]
|
|
|
78 π1p=π11 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in
|
|
|
79 begin
|
|
|
80 ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq
|
|
|
81 ≈⟨⟩
|
|
|
82 ( π1 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq)
|
|
|
83 ≈↑⟨ assoc ⟩
|
|
|
84 π1 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) )
|
|
|
85 ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩
|
|
|
86 π1 o (_×_ prod π1' π2' )
|
|
|
87 ≈⟨ π1fxg=f prod ⟩
|
|
|
88 π1'
|
|
|
89 ∎
|
|
|
90 -- π1fxg=f prod
|
|
261
|
91 π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' ]
|
|
262
|
92 π2p=π21 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in
|
|
|
93 begin
|
|
|
94 ( π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq
|
|
|
95 ≈⟨⟩
|
|
|
96 ( π2 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq)
|
|
|
97 ≈↑⟨ assoc ⟩
|
|
|
98 π2 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) )
|
|
|
99 ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩
|
|
|
100 π2 o (_×_ prod π1' π2' )
|
|
|
101 ≈⟨ π2fxg=g prod ⟩
|
|
|
102 π2'
|
|
|
103 ∎
|
|
261
|
104 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' ] ]} →
|
|
|
105 {eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} →
|
|
|
106 {eq2 : A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} →
|
|
|
107 A [ p1 eq ≈ p' ]
|
|
|
108 uniqueness1 = {!!}
|
