|
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 -- |
|
|
|
24 -- d
|
|
|
25 --
|
|
|
26
|
|
261
|
27 open Equalizer
|
|
|
28 open Product
|
|
|
29 open Pullback
|
|
|
30
|
|
|
31 pullback-from : (a b c ab d : Obj A)
|
|
260
|
32 ( f : Hom A a c ) ( g : Hom A b c )
|
|
261
|
33 ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( e : Hom A d ab )
|
|
260
|
34 ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g )
|
|
261
|
35 ( prod : Product A a b ab π1 π2 ) → Pullback A a b c d f g
|
|
|
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 {
|
|
260
|
39 commute = commute1 ;
|
|
|
40 p = p1 ;
|
|
261
|
41 π1p=π1 = λ {d} {π1'} {π2'} {eq} → π1p=π11 {d} {π1'} {π2'} {eq} ;
|
|
|
42 π2p=π2 = λ {d} {π1'} {π2'} {eq} → π2p=π21 {d} {π1'} {π2'} {eq} ;
|
|
260
|
43 uniqueness = uniqueness1
|
|
|
44 } where
|
|
261
|
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 ])) ] ] ]
|
|
|
46 commute1 = {!!}
|
|
|
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
|
|
|
48 p1 {d'} { π1' } { π2' } eq = -- _×_ prod π1' π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' ]
|
|
|
50 π1p=π11 = {!!} -- π1fxg=f prod
|
|
|
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' ]
|
|
|
52 π2p=π21 = {!!} -- π2fxg=g prod
|
|
|
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' ] ]} →
|
|
|
54 {eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} →
|
|
|
55 {eq2 : A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} →
|
|
|
56 A [ p1 eq ≈ p' ]
|
|
|
57 uniqueness1 = {!!}
|
