|
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
|
|
266
|
9 module pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ') ( Γ : Functor I A ) where
|
|
260
|
10
|
|
|
11 open import HomReasoning
|
|
|
12 open import cat-utility
|
|
|
13
|
|
|
14 --
|
|
264
|
15 -- Pullback from equalizer and product
|
|
260
|
16 -- f
|
|
|
17 -- a -------> c
|
|
|
18 -- ^ ^
|
|
|
19 -- π1 | |g
|
|
|
20 -- | |
|
|
|
21 -- ab -------> b
|
|
|
22 -- ^ π2
|
|
|
23 -- |
|
|
264
|
24 -- | e = equalizer (f π1) (g π1)
|
|
|
25 -- |
|
|
|
26 -- d <------------------ d'
|
|
|
27 -- k (π1' × π2' )
|
|
260
|
28
|
|
261
|
29 open Equalizer
|
|
|
30 open Product
|
|
|
31 open Pullback
|
|
|
32
|
|
|
33 pullback-from : (a b c ab d : Obj A)
|
|
260
|
34 ( f : Hom A a c ) ( g : Hom A b c )
|
|
261
|
35 ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( e : Hom A d ab )
|
|
260
|
36 ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g )
|
|
261
|
37 ( prod : Product A a b ab π1 π2 ) → Pullback A a b c d f g
|
|
|
38 ( A [ π1 o equalizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ){e} ) ] )
|
|
|
39 ( A [ π2 o equalizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ){e} ) ] )
|
|
|
40 pullback-from a b c ab d f g π1 π2 e eqa prod = record {
|
|
260
|
41 commute = commute1 ;
|
|
|
42 p = p1 ;
|
|
261
|
43 π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} ;
|
|
260
|
45 uniqueness = uniqueness1
|
|
|
46 } where
|
|
261
|
47 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
|
48 commute1 = let open ≈-Reasoning (A) in
|
|
|
49 begin
|
|
|
50 f o ( π1 o equalizer (eqa ( f o π1 ) ( g o π2 )) )
|
|
|
51 ≈⟨ assoc ⟩
|
|
|
52 ( f o π1 ) o equalizer (eqa ( f o π1 ) ( g o π2 ))
|
|
|
53 ≈⟨ fe=ge (eqa (A [ f o π1 ]) (A [ g o π2 ])) ⟩
|
|
|
54 ( g o π2 ) o equalizer (eqa ( f o π1 ) ( g o π2 ))
|
|
|
55 ≈↑⟨ assoc ⟩
|
|
|
56 g o ( π2 o equalizer (eqa ( f o π1 ) ( g o π2 )) )
|
|
|
57 ∎
|
|
|
58 lemma1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] →
|
|
|
59 A [ A [ A [ f o π1 ] o (prod × π1') π2' ] ≈ A [ A [ g o π2 ] o (prod × π1') π2' ] ]
|
|
|
60 lemma1 {d'} { π1' } { π2' } eq = let open ≈-Reasoning (A) in
|
|
|
61 begin
|
|
|
62 ( f o π1 ) o (prod × π1') π2'
|
|
|
63 ≈↑⟨ assoc ⟩
|
|
|
64 f o ( π1 o (prod × π1') π2' )
|
|
|
65 ≈⟨ cdr (π1fxg=f prod) ⟩
|
|
|
66 f o π1'
|
|
|
67 ≈⟨ eq ⟩
|
|
|
68 g o π2'
|
|
|
69 ≈↑⟨ cdr (π2fxg=g prod) ⟩
|
|
|
70 g o ( π2 o (prod × π1') π2' )
|
|
|
71 ≈⟨ assoc ⟩
|
|
|
72 ( g o π2 ) o (prod × π1') π2'
|
|
|
73 ∎
|
|
261
|
74 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
|
75 p1 {d'} { π1' } { π2' } eq =
|
|
|
76 let open ≈-Reasoning (A) in k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) ( lemma1 eq )
|
|
|
77 π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' ] ]} →
|
|
|
78 A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π1' ]
|
|
|
79 π1p=π11 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in
|
|
|
80 begin
|
|
|
81 ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq
|
|
|
82 ≈⟨⟩
|
|
|
83 ( π1 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq)
|
|
|
84 ≈↑⟨ assoc ⟩
|
|
|
85 π1 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) )
|
|
|
86 ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩
|
|
|
87 π1 o (_×_ prod π1' π2' )
|
|
|
88 ≈⟨ π1fxg=f prod ⟩
|
|
|
89 π1'
|
|
|
90 ∎
|
|
263
|
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' ] ]} →
|
|
|
92 A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π2' ]
|
|
262
|
93 π2p=π21 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in
|
|
|
94 begin
|
|
|
95 ( π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq
|
|
|
96 ≈⟨⟩
|
|
|
97 ( π2 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq)
|
|
|
98 ≈↑⟨ assoc ⟩
|
|
|
99 π2 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) )
|
|
|
100 ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩
|
|
|
101 π2 o (_×_ prod π1' π2' )
|
|
|
102 ≈⟨ π2fxg=g prod ⟩
|
|
|
103 π2'
|
|
|
104 ∎
|
|
261
|
105 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' ] ]} →
|
|
|
106 {eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} →
|
|
|
107 {eq2 : A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} →
|
|
|
108 A [ p1 eq ≈ p' ]
|
|
264
|
109 uniqueness1 {d'} p' {π1'} {π2'} {eq} {eq1} {eq2} = let open ≈-Reasoning (A) in
|
|
263
|
110 begin
|
|
|
111 p1 eq
|
|
|
112 ≈⟨⟩
|
|
|
113 k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq)
|
|
264
|
114 ≈⟨ Equalizer.uniqueness (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e}) ( begin
|
|
|
115 e o p'
|
|
|
116 ≈⟨⟩
|
|
|
117 equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p'
|
|
|
118 ≈↑⟨ Product.uniqueness prod ⟩
|
|
|
119 (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'))
|
|
|
120 ≈⟨ ×-cong prod (assoc) (assoc) ⟩
|
|
|
121 (prod × (A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]))
|
|
|
122 (A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ])
|
|
|
123 ≈⟨ ×-cong prod eq1 eq2 ⟩
|
|
|
124 ((prod × π1') π2')
|
|
|
125 ∎ ) ⟩
|
|
263
|
126 p'
|
|
|
127 ∎
|
|
|
128
|
|
266
|
129 ------
|
|
|
130 --
|
|
|
131 -- Limit
|
|
|
132 --
|
|
|
133 -----
|
|
|
134
|
|
|
135 -- Constancy Functor
|
|
|
136
|
|
|
137 K : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) → ( a : Obj A ) → Functor I A
|
|
|
138 K I a = record {
|
|
265
|
139 FObj = λ i → a ;
|
|
|
140 FMap = λ f → id1 A a ;
|
|
|
141 isFunctor = let open ≈-Reasoning (A) in record {
|
|
|
142 ≈-cong = λ f=g → refl-hom
|
|
|
143 ; identity = refl-hom
|
|
|
144 ; distr = sym idL
|
|
|
145 }
|
|
|
146 }
|
|
|
147
|
|
|
148 open NTrans
|
|
|
149
|
|
|
150 record Limit { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
|
|
266
|
151 ( a0 : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
|
|
265
|
152 field
|
|
266
|
153 limit : ( a : Obj A ) → ( t : NTrans I A ( K I a ) Γ ) → Hom A a a0
|
|
|
154 t0f=t : { a : Obj A } → { t : NTrans I A ( K I a ) Γ } → ∀ { i : Obj I } →
|
|
265
|
155 A [ A [ TMap t0 i o limit a t ] ≈ TMap t i ]
|
|
266
|
156 limit-uniqueness : { a : Obj A } → { t : NTrans I A ( K I a ) Γ } → { f : Hom A a a0 } → ∀ ( i : Obj I ) →
|
|
265
|
157 A [ A [ TMap t0 i o f ] ≈ TMap t i ] → A [ limit a t ≈ f ]
|
|
|
158
|
|
266
|
159 --------------------------------
|
|
|
160 --
|
|
|
161 -- If we have two limits on c and c', there are isomorphic pair h, h'
|
|
|
162
|
|
|
163 open Limit
|
|
|
164
|
|
|
165 iso-l : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
|
|
|
166 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) ( t0' : NTrans I A ( K I a0' ) Γ )
|
|
|
167 ( lim : Limit I Γ a0 t0 ) → ( lim' : Limit I Γ a0' t0' )
|
|
|
168 → Hom A a0 a0'
|
|
|
169 iso-l I Γ a0 a0' t0 t0' lim lim' = limit lim' a0 t0
|
|
|
170
|
|
|
171 iso-r : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
|
|
|
172 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) ( t0' : NTrans I A ( K I a0' ) Γ )
|
|
|
173 ( lim : Limit I Γ a0 t0 ) → ( lim' : Limit I Γ a0' t0' )
|
|
|
174 → Hom A a0' a0
|
|
|
175 iso-r I Γ a0 a0' t0 t0' lim lim' = limit lim a0' t0'
|
|
|
176
|
|
|
177
|
|
|
178 iso-lr : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
|
|
|
179 ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) ( t0' : NTrans I A ( K I a0' ) Γ )
|
|
|
180 ( lim : Limit I Γ a0 t0 ) → ( lim' : Limit I Γ a0' t0' ) → ∀{ i : Obj I } →
|
|
|
181 A [ A [ iso-l I Γ a0 a0' t0 t0' lim lim' o iso-r I Γ a0 a0' t0 t0' lim lim' ] ≈ id1 A a0' ]
|
|
|
182 iso-lr I Γ a0 a0' t0 t0' lim lim' {i} = let open ≈-Reasoning (A) in begin
|
|
|
183 limit lim' a0 t0 o limit lim a0' t0'
|
|
|
184 ≈↑⟨ limit-uniqueness lim' i ( begin
|
|
|
185 TMap t0' i o ( limit lim' a0 t0 o limit lim a0' t0' )
|
|
|
186 ≈⟨ assoc ⟩
|
|
|
187 ( TMap t0' i o limit lim' a0 t0 ) o limit lim a0' t0'
|
|
|
188 ≈⟨ car ( t0f=t lim' ) ⟩
|
|
|
189 TMap t0 i o limit lim a0' t0'
|
|
|
190 ≈⟨ t0f=t lim ⟩
|
|
|
191 TMap t0' i
|
|
|
192 ∎ ) ⟩
|
|
|
193 limit lim' a0' t0'
|
|
|
194 ≈⟨ limit-uniqueness lim' i idR ⟩
|
|
|
195 id a0'
|
|
|
196 ∎
|
|
|
197
|
|
|
198
|
|
|
199 open import CatExponetial I A
|
|
|
200
|
|
|
201 KI : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) → ( a : Obj A ) → Functor I A
|
|
|
202 KI I Γ a = record {
|
|
|
203 FObj = λ i → a ;
|
|
|
204 FMap = λ f → id1 A a ;
|
|
|
205 isFunctor = let open ≈-Reasoning (A) in record {
|
|
|
206 ≈-cong = λ f=g → refl-hom
|
|
|
207 ; identity = refl-hom
|
|
|
208 ; distr = sym idL
|
|
|
209 }
|
|
|
210 }
|
