Mercurial > hg > Members > kono > Proof > category

comparison equalizer.agda @ 221:ea0407fb8f02

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 04 Sep 2013 20:35:43 +0900
parents 5d96be63053f
children 0bc85361b7d0
comparison
equal deleted inserted replaced
220:5d96be63053f 221:ea0407fb8f02
21 open import cat-utility 21 open import cat-utility
22 22
23 record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where 23 record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
24 field 24 field
25 e : Hom A c a 25 e : Hom A c a
26 ef=eg : A [ A [ f o e ] ≈ A [ g o e ] ] 26 fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ]
27 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c 27 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c
28 ek=h : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ e o k {d} h eq ] ≈ h ] 28 ek=h : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ e o k {d} h eq ] ≈ h ]
29 uniqueness : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → 29 uniqueness : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } →
30 A [ A [ e o k' ] ≈ h ] → A [ k {d} h eq ≈ k' ] 30 A [ A [ e o k' ] ≈ h ] → A [ k {d} h eq ≈ k' ]
31 equalizer : Hom A c a 31 equalizer : Hom A c a
46 β {d} {e} {a} {b} f g h = A [ γ {a} {b} {c} f g h o δ (A [ f o h ]) ] 46 β {d} {e} {a} {b} f g h = A [ γ {a} {b} {c} f g h o δ (A [ f o h ]) ]
47 47
48 open Equalizer 48 open Equalizer
49 open EqEqualizer 49 open EqEqualizer
50 50
51 -- Equalizer is unique up to iso
52
53 equalizer-iso : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g )
54 → Hom A c c' --- != id1 A c
55 equalizer-iso {c} eqa eqa' = k eqa' (e eqa) (ef=eg eqa)
56
57 equalizer-iso-eq : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g ) → {eff : Equalizer A {c} f f}
58 → A [ A [ equalizer-iso eqa eqa' o equalizer-iso eqa' eqa ] ≈ id1 A c' ]
59 equalizer-iso-eq {c} {c'} {f} {g} eqa eqa' {eff} = let open ≈-Reasoning (A) in
60 begin
61 equalizer-iso eqa eqa' o equalizer-iso eqa' eqa
62 ≈⟨⟩
63 k eqa' (e eqa) (ef=eg eqa) o k eqa (e eqa') (ef=eg eqa')
64 ≈⟨ car (uniqueness eqa' {!!}) ⟩
65 {!!} o k eqa (e eqa') (ef=eg eqa')
66 ≈⟨ {!!} ⟩
67 id1 A c'
68 ∎
69
70 -- ke = e' k'e' = e → k k' = 1 , k' k = 1
71 -- ke = e'
72 -- k'ke = k'e' = e kk' = 1
73
74 -- x e = e -> x = id?
75 51
76 f1=g1 : { a b : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → A [ A [ f o id1 A a ] ≈ A [ g o id1 A a ] ] 52 f1=g1 : { a b : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → A [ A [ f o id1 A a ] ≈ A [ g o id1 A a ] ]
77 f1=g1 eq = let open ≈-Reasoning (A) in (resp refl-hom eq ) 53 f1=g1 eq = let open ≈-Reasoning (A) in (resp refl-hom eq )
78 54
79 55
104 equalizer+h : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) (i : Hom A c d ) → (h : Hom A d a ) → (h-1 : Hom A a d ) 80 equalizer+h : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) (i : Hom A c d ) → (h : Hom A d a ) → (h-1 : Hom A a d )
105 → A [ A [ h o i ] ≈ e eqa ] → A [ A [ h-1 o h ] ≈ id1 A d ] 81 → A [ A [ h o i ] ≈ e eqa ] → A [ A [ h-1 o h ] ≈ id1 A d ]
106 → Equalizer A {c} (A [ f o h ]) (A [ g o h ] ) 82 → Equalizer A {c} (A [ f o h ]) (A [ g o h ] )
107 equalizer+h {a} {b} {c} {d} {f} {g} eqa i h h-1 eq h-1-id = record { 83 equalizer+h {a} {b} {c} {d} {f} {g} eqa i h h-1 eq h-1-id = record {
108 e = i ; -- A [ h-1 o e eqa ] ; -- Hom A a d 84 e = i ; -- A [ h-1 o e eqa ] ; -- Hom A a d
109 ef=eg = ef=eg1 ; 85 fe=ge = fe=ge1 ;
110 k = λ j eq' → k eqa (A [ h o j ]) (fhj=ghj j eq' ) ; 86 k = λ j eq' → k eqa (A [ h o j ]) (fhj=ghj j eq' ) ;
111 ek=h = ek=h1 ; 87 ek=h = ek=h1 ;
112 uniqueness = uniqueness1 88 uniqueness = uniqueness1
113 } where 89 } where
114 fhj=ghj : {d' : Obj A } → (j : Hom A d' d ) → 90 fhj=ghj : {d' : Obj A } → (j : Hom A d' d ) →
122 ≈⟨ eq' ⟩ 98 ≈⟨ eq' ⟩
123 (g o h ) o j 99 (g o h ) o j
124 ≈↑⟨ assoc ⟩ 100 ≈↑⟨ assoc ⟩
125 g o ( h o j ) 101 g o ( h o j )
126 ∎ 102 ∎
127 ef=eg1 : A [ A [ A [ f o h ] o i ] ≈ A [ A [ g o h ] o i ] ] 103 fe=ge1 : A [ A [ A [ f o h ] o i ] ≈ A [ A [ g o h ] o i ] ]
128 ef=eg1 = let open ≈-Reasoning (A) in 104 fe=ge1 = let open ≈-Reasoning (A) in
129 begin 105 begin
130 ( f o h ) o i 106 ( f o h ) o i
131 ≈↑⟨ assoc ⟩ 107 ≈↑⟨ assoc ⟩
132 f o (h o i ) 108 f o (h o i )
133 ≈⟨ cdr eq ⟩ 109 ≈⟨ cdr eq ⟩
134 f o (e eqa) 110 f o (e eqa)
135 ≈⟨ ef=eg eqa ⟩ 111 ≈⟨ fe=ge eqa ⟩
136 g o (e eqa) 112 g o (e eqa)
137 ≈↑⟨ cdr eq ⟩ 113 ≈↑⟨ cdr eq ⟩
138 g o (h o i ) 114 g o (h o i )
139 ≈⟨ assoc ⟩ 115 ≈⟨ assoc ⟩
140 ( g o h ) o i 116 ( g o h ) o i
183 h+equalizer : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) (h : Hom A b d ) 159 h+equalizer : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) (h : Hom A b d )
184 → (h-1 : Hom A d b ) → A [ A [ h-1 o h ] ≈ id1 A b ] 160 → (h-1 : Hom A d b ) → A [ A [ h-1 o h ] ≈ id1 A b ]
185 → Equalizer A {c} (A [ h o f ]) (A [ h o g ] ) 161 → Equalizer A {c} (A [ h o f ]) (A [ h o g ] )
186 h+equalizer {a} {b} {c} {d} {f} {g} eqa h h-1 h-1-id = record { 162 h+equalizer {a} {b} {c} {d} {f} {g} eqa h h-1 h-1-id = record {
187 e = e eqa ; 163 e = e eqa ;
188 ef=eg = ef=eg1 ; 164 fe=ge = fe=ge1 ;
189 k = λ j eq' → k eqa j (fj=gj j eq') ; 165 k = λ j eq' → k eqa j (fj=gj j eq') ;
190 ek=h = ek=h1 ; 166 ek=h = ek=h1 ;
191 uniqueness = uniqueness1 167 uniqueness = uniqueness1
192 } where 168 } where
193 fj=gj : {e : Obj A} → (j : Hom A e a ) → A [ A [ A [ h o f ] o j ] ≈ A [ A [ h o g ] o j ] ] → A [ A [ f o j ] ≈ A [ g o j ] ] 169 fj=gj : {e : Obj A} → (j : Hom A e a ) → A [ A [ A [ h o f ] o j ] ≈ A [ A [ h o g ] o j ] ] → A [ A [ f o j ] ≈ A [ g o j ] ]
211 ≈⟨ car h-1-id ⟩ 187 ≈⟨ car h-1-id ⟩
212 id1 A b o ( g o j ) 188 id1 A b o ( g o j )
213 ≈⟨ idL ⟩ 189 ≈⟨ idL ⟩
214 g o j 190 g o j
215 ∎ 191 ∎
216 ef=eg1 : A [ A [ A [ h o f ] o e eqa ] ≈ A [ A [ h o g ] o e eqa ] ] 192 fe=ge1 : A [ A [ A [ h o f ] o e eqa ] ≈ A [ A [ h o g ] o e eqa ] ]
217 ef=eg1 = let open ≈-Reasoning (A) in 193 fe=ge1 = let open ≈-Reasoning (A) in
218 begin 194 begin
219 ( h o f ) o e eqa 195 ( h o f ) o e eqa
220 ≈↑⟨ assoc ⟩ 196 ≈↑⟨ assoc ⟩
221 h o (f o e eqa ) 197 h o (f o e eqa )
222 ≈⟨ cdr (ef=eg eqa) ⟩ 198 ≈⟨ cdr (fe=ge eqa) ⟩
223 h o (g o e eqa ) 199 h o (g o e eqa )
224 ≈⟨ assoc ⟩ 200 ≈⟨ assoc ⟩
225 ( h o g ) o e eqa 201 ( h o g ) o e eqa
226 ∎ 202 ∎
227 ek=h1 : {d₁ : Obj A} {j : Hom A d₁ a} {eq : A [ A [ A [ h o f ] o j ] ≈ A [ A [ h o g ] o j ] ]} → 203 ek=h1 : {d₁ : Obj A} {j : Hom A d₁ a} {eq : A [ A [ A [ h o f ] o j ] ≈ A [ A [ h o g ] o j ] ]} →
233 209
234 eefeg : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) 210 eefeg : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g)
235 → Equalizer A {c} (A [ f o e eqa ]) (A [ g o e eqa ] ) 211 → Equalizer A {c} (A [ f o e eqa ]) (A [ g o e eqa ] )
236 eefeg {a} {b} {c} {d} {f} {g} eqa = record { 212 eefeg {a} {b} {c} {d} {f} {g} eqa = record {
237 e = id1 A c ; -- i ; -- A [ h-1 o e eqa ] ; -- Hom A a d 213 e = id1 A c ; -- i ; -- A [ h-1 o e eqa ] ; -- Hom A a d
238 ef=eg = ef=eg1 ; 214 fe=ge = fe=ge1 ;
239 k = λ j eq' → k eqa (A [ h o j ]) (fhj=ghj j eq' ) ; 215 k = λ j eq' → k eqa (A [ h o j ]) (fhj=ghj j eq' ) ;
240 ek=h = ek=h1 ; 216 ek=h = ek=h1 ;
241 uniqueness = uniqueness1 217 uniqueness = uniqueness1
242 } where 218 } where
243 i = id1 A c 219 i = id1 A c
253 ≈⟨ eq' ⟩ 229 ≈⟨ eq' ⟩
254 (g o h ) o j 230 (g o h ) o j
255 ≈↑⟨ assoc ⟩ 231 ≈↑⟨ assoc ⟩
256 g o ( h o j ) 232 g o ( h o j )
257 ∎ 233 ∎
258 ef=eg1 : A [ A [ A [ f o h ] o i ] ≈ A [ A [ g o h ] o i ] ] 234 fe=ge1 : A [ A [ A [ f o h ] o i ] ≈ A [ A [ g o h ] o i ] ]
259 ef=eg1 = let open ≈-Reasoning (A) in 235 fe=ge1 = let open ≈-Reasoning (A) in
260 begin 236 begin
261 ( f o h ) o i 237 ( f o h ) o i
262 ≈⟨ car ( ef=eg eqa ) ⟩ 238 ≈⟨ car ( fe=ge eqa ) ⟩
263 ( g o h ) o i 239 ( g o h ) o i
264 ∎ 240 ∎
265 ek=h1 : {d' : Obj A} {k' : Hom A d' c} {eq' : A [ A [ A [ f o h ] o k' ] ≈ A [ A [ g o h ] o k' ] ]} → 241 ek=h1 : {d' : Obj A} {k' : Hom A d' c} {eq' : A [ A [ A [ f o h ] o k' ] ≈ A [ A [ g o h ] o k' ] ]} →
266 A [ A [ i o k eqa (A [ h o k' ]) (fhj=ghj k' eq') ] ≈ k' ] 242 A [ A [ i o k eqa (A [ h o k' ]) (fhj=ghj k' eq') ] ≈ k' ]
267 ek=h1 {d'} {k'} {eq'} = let open ≈-Reasoning (A) in 243 ek=h1 {d'} {k'} {eq'} = let open ≈-Reasoning (A) in
285 e eqa o h' 261 e eqa o h'
286 ∎ ) ⟩ 262 ∎ ) ⟩
287 k' 263 k'
288 ∎ 264 ∎
289 265
290 266 -- Equalizer is unique up to iso
291 267
268 equalizer-iso : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g )
269 → Hom A c c' --- != id1 A c
270 equalizer-iso {c} eqa eqa' = k eqa' (e eqa) (fe=ge eqa)
271
272 --
273 --
274 -- e eqa f g f
275 -- c ----------> a ------->b
276 --
277 equalizer-iso-eq : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g )
278 → A [ A [ equalizer-iso eqa eqa' o equalizer-iso eqa' eqa ] ≈ id1 A c' ]
279 equalizer-iso-eq {c} {c'} {f} {g} eqa eqa' = let open ≈-Reasoning (A) in
280 begin
281 k eqa' (e eqa) (fe=ge eqa) o k eqa (e eqa' ) (fe=ge eqa' )
282 ≈⟨ {!!} ⟩
283 id1 A c'
284 ∎
285
286 -- ke = e' k'e' = e → k k' = 1 , k' k = 1
287 -- ke = e'
288 -- k'ke = k'e' = e kk' = 1
289
290 -- x e = e -> x = id?
292 291
293 lemma-equ1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a b c : Obj A} (f g : Hom A a b) → 292 lemma-equ1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a b c : Obj A} (f g : Hom A a b) →
294 ( {a b c : Obj A} → (f g : Hom A a b) → Equalizer A {c} f g ) → EqEqualizer A {c} f g 293 ( {a b c : Obj A} → (f g : Hom A a b) → Equalizer A {c} f g ) → EqEqualizer A {c} f g
295 lemma-equ1 A {a} {b} {c} f g eqa = record { 294 lemma-equ1 A {a} {b} {c} f g eqa = record {
296 α = λ f g → e (eqa f g ) ; -- Hom A c a 295 α = λ f g → e (eqa f g ) ; -- Hom A c a
297 γ = λ {a} {b} {c} {d} f g h → k (eqa f g ) {d} ( A [ h o (e ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) ; -- Hom A c d 296 γ = λ {a} {b} {c} {d} f g h → k (eqa f g ) {d} ( A [ h o (e ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) ; -- Hom A c d
298 δ = λ {a} f → k (eqa f f) (id1 A a) (lemma-equ2 f); -- Hom A a c 297 δ = λ {a} f → k (eqa f f) (id1 A a) (lemma-equ2 f); -- Hom A a c
299 b1 = ef=eg (eqa f g) ; 298 b1 = fe=ge (eqa f g) ;
300 b2 = lemma-equ5 ; 299 b2 = lemma-equ5 ;
301 b3 = lemma-equ3 ; 300 b3 = lemma-equ3 ;
302 b4 = lemma-equ6 301 b4 = lemma-equ6
303 } where 302 } where
304 -- 303 --
327 lemma-equ4 {a} {b} {c} {d} f g h = let open ≈-Reasoning (A) in 326 lemma-equ4 {a} {b} {c} {d} f g h = let open ≈-Reasoning (A) in
328 begin 327 begin
329 f o ( h o e (eqa (f o h) ( g o h ))) 328 f o ( h o e (eqa (f o h) ( g o h )))
330 ≈⟨ assoc ⟩ 329 ≈⟨ assoc ⟩
331 (f o h) o e (eqa (f o h) ( g o h )) 330 (f o h) o e (eqa (f o h) ( g o h ))
332 ≈⟨ ef=eg (eqa (A [ f o h ]) (A [ g o h ])) ⟩ 331 ≈⟨ fe=ge (eqa (A [ f o h ]) (A [ g o h ])) ⟩
333 (g o h) o e (eqa (f o h) ( g o h )) 332 (g o h) o e (eqa (f o h) ( g o h ))
334 ≈↑⟨ assoc ⟩ 333 ≈↑⟨ assoc ⟩
335 g o ( h o e (eqa (f o h) ( g o h ))) 334 g o ( h o e (eqa (f o h) ( g o h )))
336 ∎ 335 ∎
337 lemma-equ5 : {d : Obj A} {h : Hom A d a} → A [ 336 lemma-equ5 : {d : Obj A} {h : Hom A d a} → A [