Mercurial > hg > Members > kono > Proof > category

comparison equalizer.agda @ 245:0d1f7bbea9bc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 09 Sep 2013 12:02:48 +0900
parents d9317fe71ed6
children 80d9ef47566b
comparison
equal deleted inserted replaced
244:d9317fe71ed6 245:0d1f7bbea9bc
33 -- 33 --
34 -- Flat Equational Definition of Equalizer 34 -- Flat Equational Definition of Equalizer
35 -- 35 --
36 record Burroni { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (f g : Hom A a b) (e : Hom A c a) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where 36 record Burroni { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (f g : Hom A a b) (e : Hom A c a) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
37 field 37 field
38 α : {a b c : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → {e : Hom A c a } → Hom A c a 38 α : {a b c : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (e : Hom A c a ) → Hom A c a
39 γ : {a b c d : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A d c 39 γ : {a b c d : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A d c
40 δ : {a b c : Obj A } → {e : Hom A c a } → (f : Hom A a b) → Hom A a c 40 δ : {a b c : Obj A } → (e : Hom A c a ) → (f : Hom A a b) → Hom A a c
41 cong-α : {a b c : Obj A } → { e : Hom A c a } 41 cong-α : {a b c : Obj A } → { e : Hom A c a }
42 → {f g g' : Hom A a b } → A [ g ≈ g' ] → A [ α f g {e} ≈ α f g' {e} ] 42 → {f g g' : Hom A a b } → A [ g ≈ g' ] → A [ α f g e ≈ α f g' e ]
43 cong-γ : {a _ c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } → A [ h ≈ h' ] 43 cong-γ : {a _ c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } → A [ h ≈ h' ]
44 → A [ γ {a} {b} {c} {d} f g h ≈ γ f g h' ] 44 → A [ γ {a} {b} {c} {d} f g h ≈ γ f g h' ]
45 cong-δ : {a b c : Obj A } → {f f' : Hom A a b} → A [ f ≈ f' ] → A [ δ f ≈ δ f' ] 45 cong-δ : {a b c : Obj A } → {e : Hom A c a} → {f f' : Hom A a b} → A [ f ≈ f' ] → A [ δ e f ≈ δ e f' ]
46 b1 : A [ A [ f o α {a} {b} {c} f g {e} ] ≈ A [ g o α {a} {b} {c} f g {e} ] ] 46 b1 : A [ A [ f o α {a} {b} {c} f g e ] ≈ A [ g o α {a} {b} {c} f g e ] ]
47 b2 : {d : Obj A } → {h : Hom A d a } → A [ A [ ( α {a} {b} {c} f g {e} ) o (γ {a} {b} {c} f g h) ] ≈ A [ h o α (A [ f o h ]) (A [ g o h ]){id1 A d} ] ] 47 b2 : {d : Obj A } → {h : Hom A d a } → A [ A [ ( α {a} {b} {c} f g e ) o (γ {a} {b} {c} f g h) ] ≈ A [ h o α (A [ f o h ]) (A [ g o h ]) (id1 A d) ] ]
48 b3 : {a b d : Obj A} → (f : Hom A a b ) → {h : Hom A d a } → A [ A [ α {a} {b} {d} f f {h} o δ {a} {b} {d} {h} f ] ≈ id1 A a ] 48 b3 : {a b d : Obj A} → (f : Hom A a b ) → {h : Hom A d a } → A [ A [ α {a} {b} {d} f f h o δ {a} {b} {d} h f ] ≈ id1 A a ]
49 -- b4 : {c d : Obj A } {k : Hom A c a} → A [ β f g ( A [ α f g o k ] ) ≈ k ] 49 -- b4 : {c d : Obj A } {k : Hom A c a} → A [ β f g ( A [ α f g o k ] ) ≈ k ]
50 b4 : {d : Obj A } {k : Hom A d c} → 50 b4 : {d : Obj A } {k : Hom A d c} →
51 A [ A [ γ {a} {b} {c} {d} f g ( A [ α {a} {b} {c} f g {e} o k ] ) o ( δ {d} {b} {d} {id1 A d} (A [ f o A [ α {a} {b} {c} f g {e} o k ] ] ) )] ≈ k ] 51 A [ A [ γ {a} {b} {c} {d} f g ( A [ α {a} {b} {c} f g e o k ] ) o ( δ {d} {b} {d} (id1 A d) (A [ f o A [ α {a} {b} {c} f g e o k ] ] ) )] ≈ k ]
52 -- A [ α f g o β f g h ] ≈ h 52 -- A [ α f g o β f g h ] ≈ h
53 β : { d a b : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A d c 53 β : { d a b : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A d c
54 β {d} {a} {b} f g h = A [ γ {a} {b} {c} f g h o δ {d} {b} {d} {id1 A d} (A [ f o h ]) ] 54 β {d} {a} {b} f g h = A [ γ {a} {b} {c} f g h o δ {d} {b} {d} (id1 A d) (A [ f o h ]) ]
55 55
56 open Equalizer 56 open Equalizer
57 open Burroni 57 open Burroni
58 58
59 -- 59 --
229 229
230 lemma-equ1 : {a b c : Obj A} (f g : Hom A a b) → (e : Hom A c a ) → 230 lemma-equ1 : {a b c : Obj A} (f g : Hom A a b) → (e : Hom A c a ) →
231 ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g ) 231 ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g )
232 → Burroni A {c} {a} {b} f g e 232 → Burroni A {c} {a} {b} f g e
233 lemma-equ1 {a} {b} {c} f g e eqa = record { 233 lemma-equ1 {a} {b} {c} f g e eqa = record {
234 α = λ {a} {b} {c} f g {e} → equalizer (eqa {a} {b} {c} f g {e} ) ; -- Hom A c a 234 α = λ {a} {b} {c} f g e → equalizer (eqa {a} {b} {c} f g {e} ) ; -- Hom A c a
235 γ = λ {a} {b} {c} {d} f g h → k (eqa f g ) {d} ( A [ h o (equalizer ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) 235 γ = λ {a} {b} {c} {d} f g h → k (eqa f g ) {d} ( A [ h o (equalizer ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] )
236 (lemma-equ4 {a} {b} {c} {d} f g h ) ; -- Hom A c d 236 (lemma-equ4 {a} {b} {c} {d} f g h ) ; -- Hom A c d
237 δ = λ {a} {b} {c} {e} f → k (eqa {a} {b} {c} f f {e} ) (id1 A a) (lemma-equ2 f); -- Hom A a c 237 δ = λ {a} {b} {c} e f → k (eqa {a} {b} {c} f f {e} ) (id1 A a) (lemma-equ2 f); -- Hom A a c
238 cong-α = cong-α1 ; 238 cong-α = cong-α1 ;
239 cong-γ = cong-γ1 ; 239 cong-γ = cong-γ1 ;
240 cong-δ = λ {a b c f f'} f=f' → cong-δ1 {a} {b} {c} {f} {f'} f=f' ; 240 cong-δ = λ {a b c e f f'} f=f' → cong-δ1 {a} {b} {c} {e} {f} {f'} f=f' ;
241 b1 = fe=ge (eqa {a} {b} {c} f g {e}) ; 241 b1 = fe=ge (eqa {a} {b} {c} f g {e}) ;
242 b2 = lemma-b2 ; 242 b2 = lemma-b2 ;
243 b3 = lemma-b3 ; 243 b3 = lemma-b3 ;
244 b4 = lemma-b4 244 b4 = lemma-b4
245 } where 245 } where
274 ≈⟨ fe=ge (eqa (A [ f o h ]) (A [ g o h ])) ⟩ 274 ≈⟨ fe=ge (eqa (A [ f o h ]) (A [ g o h ])) ⟩
275 (g o h) o equalizer (eqa (f o h) ( g o h )) 275 (g o h) o equalizer (eqa (f o h) ( g o h ))
276 ≈↑⟨ assoc ⟩ 276 ≈↑⟨ assoc ⟩
277 g o ( h o equalizer (eqa (f o h) ( g o h ))) 277 g o ( h o equalizer (eqa (f o h) ( g o h )))
278 ∎ 278 ∎
279 cong-α1 : {a b c : Obj A } → { e : Hom A c a }
280 → {f g g' : Hom A a b } → A [ g ≈ g' ] → A [ equalizer (eqa {a} {b} {c} f g {e} )≈ equalizer (eqa {a} {b} {c} f g' {e} ) ]
281 cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq = let open ≈-Reasoning (A) in refl-hom
282 cong-γ1 : {a _ c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } → A [ h ≈ h' ] →
283 A [ k (eqa f g ) {d} ( A [ h o (equalizer ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h )
284 ≈ k (eqa f g ) {d} ( A [ h' o (equalizer ( eqa (A [ f o h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' ) ]
285 cong-γ1 {a} {_} {c} {d} {f} {g} {h} {h'} h=h' = let open ≈-Reasoning (A) in begin
286 k (eqa f g ) {d} ( A [ h o (equalizer ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h )
287 ≈⟨ uniqueness (eqa f g) ( begin
288 {!!} o {!!}
289 ≈⟨ {!!} ⟩
290 h o equalizer (eqa ( f o h ) ( g o h ))
291 ∎ )⟩
292 {!!} o {!!}
293 ≈↑⟨ uniqueness (eqa f g) {!!} ⟩
294 k (eqa f g ) {d} ( A [ h' o (equalizer ( eqa (A [ f o h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' )
295 ∎
296 cong-δ1 : {a b c : Obj A} {e : Hom A c a } {f f' : Hom A a b} → A [ f ≈ f' ] → A [ k (eqa {a} {b} {c} f f {e} ) (id1 A a) (lemma-equ2 f) ≈
297 k (eqa {a} {b} {c} f' f' {e} ) (id1 A a) (lemma-equ2 f') ]
298 cong-δ1 = {!!}
279 lemma-b2 : {d : Obj A} {h : Hom A d a} → A [ 299 lemma-b2 : {d : Obj A} {h : Hom A d a} → A [
280 A [ equalizer (eqa f g) o k (eqa f g) (A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ]) (lemma-equ4 {a} {b} {c} f g h) ] 300 A [ equalizer (eqa f g) o k (eqa f g) (A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ]) (lemma-equ4 {a} {b} {c} f g h) ]
281 ≈ A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ] ] 301 ≈ A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ] ]
282 lemma-b2 {d} {h} = let open ≈-Reasoning (A) in 302 lemma-b2 {d} {h} = let open ≈-Reasoning (A) in
283 begin 303 begin
314 ∎ ))) ⟩ 334 ∎ ))) ⟩
315 j o id1 A d 335 j o id1 A d
316 ≈⟨ idR ⟩ 336 ≈⟨ idR ⟩
317 j 337 j
318 ∎ 338 ∎
319 cong-α1 : {a b c : Obj A } → { e : Hom A c a }
320 → {f g g' : Hom A a b } → A [ g ≈ g' ] → A [ equalizer (eqa {a} {b} {c} f g {e} )≈ equalizer (eqa {a} {b} {c} f g' {e} ) ]
321 cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq = let open ≈-Reasoning (A) in refl-hom
322 cong-γ1 : {a _ c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } → A [ h ≈ h' ] →
323 A [ k (eqa f g ) {d} ( A [ h o (equalizer ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h )
324 ≈ k (eqa f g ) {d} ( A [ h' o (equalizer ( eqa (A [ f o h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' ) ]
325 cong-γ1 = {!!}
326 -- {a₁ b₁ c₃ : Obj A} {f₁ f' : Hom A a₁ b₁} → A [ f₁ ≈ f' ] →
327 -- A [ k (eqa f₁ f₁) (id1 A a₁) (lemma-equ2 f₁) ≈ k (eqa f' f') (id1 A a₁) (lemma-equ2 f') ]
328 cong-δ1 : {a b c : Obj A} {f f' : Hom A a b} → A [ f ≈ f' ] → { e : Hom A c a } → A [ k (eqa {a} {b} {c} f f {e} ) (id1 A a) (lemma-equ2 f) ≈
329 k (eqa {a} {b} {c} f' f' {e} ) (id1 A a) (lemma-equ2 f') ]
330 cong-δ1 = {!!}
331 339
332 340
333 lemma-equ2 : {a b c : Obj A} (f g : Hom A a b) (e : Hom A c a ) 341 lemma-equ2 : {a b c : Obj A} (f g : Hom A a b) (e : Hom A c a )
334 → ( bur : Burroni A {c} {a} {b} f g e ) → Equalizer A {c} {a} {b} (α bur f g) f g 342 → ( bur : Burroni A {c} {a} {b} f g e ) → Equalizer A {c} {a} {b} (α bur f g e) f g
335 lemma-equ2 {a} {b} {c} f g e bur = record { 343 lemma-equ2 {a} {b} {c} f g e bur = record {
336 fe=ge = fe=ge1 ; 344 fe=ge = fe=ge1 ;
337 k = k1 ; 345 k = k1 ;
338 ek=h = λ {d} {h} {eq} → ek=h1 {d} {h} {eq} ; 346 ek=h = λ {d} {h} {eq} → ek=h1 {d} {h} {eq} ;
339 uniqueness = λ {d} {h} {eq} {k'} ek=h → uniqueness1 {d} {h} {eq} {k'} ek=h 347 uniqueness = λ {d} {h} {eq} {k'} ek=h → uniqueness1 {d} {h} {eq} {k'} ek=h
340 } where 348 } where
341 k1 : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c 349 k1 : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c
342 k1 {d} h fh=gh = β bur {d} {a} {b} f g h 350 k1 {d} h fh=gh = β bur {d} {a} {b} f g h
343 fe=ge1 : A [ A [ f o (α bur f g) ] ≈ A [ g o (α bur f g) ] ] 351 fe=ge1 : A [ A [ f o (α bur f g e) ] ≈ A [ g o (α bur f g e) ] ]
344 fe=ge1 = b1 bur 352 fe=ge1 = b1 bur
345 ek=h1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ (α bur f g) o k1 {d} h eq ] ≈ h ] 353 ek=h1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ (α bur f g e) o k1 {d} h eq ] ≈ h ]
346 ek=h1 {d} {h} {eq} = let open ≈-Reasoning (A) in 354 ek=h1 {d} {h} {eq} = let open ≈-Reasoning (A) in
347 begin 355 begin
348 α bur f g o k1 h eq 356 α bur f g e o k1 h eq
349 ≈⟨⟩ 357 ≈⟨⟩
350 α bur f g o ( γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} {id1 A d} (f o h) ) 358 α bur f g e o ( γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} (id1 A d) (f o h) )
351 ≈⟨ assoc ⟩ 359 ≈⟨ assoc ⟩
352 ( α bur f g o γ bur {a} {b} {c} f g h ) o δ bur {d} {b} {d} {id1 A d} (f o h) 360 ( α bur f g e o γ bur {a} {b} {c} f g h ) o δ bur {d} {b} {d} (id1 A d) (f o h)
353 ≈⟨ car (b2 bur) ⟩ 361 ≈⟨ car (b2 bur) ⟩
354 ( h o ( α bur ( f o h ) ( g o h ))) o δ bur {d} {b} {d} {id1 A d} (f o h) 362 ( h o ( α bur ( f o h ) ( g o h ) (id1 A d))) o δ bur {d} {b} {d} (id1 A d) (f o h)
355 ≈↑⟨ assoc ⟩ 363 ≈↑⟨ assoc ⟩
356 h o ((( α bur ( f o h ) ( g o h ))) o δ bur {d} {b} {d} {id1 A d} (f o h) ) 364 h o ((( α bur ( f o h ) ( g o h ) (id1 A d) )) o δ bur {d} {b} {d} (id1 A d) (f o h) )
357 ≈↑⟨ cdr ( car ( cong-α bur eq)) ⟩ 365 ≈↑⟨ cdr ( car ( cong-α bur eq)) ⟩
358 h o ((( α bur ( f o h ) ( f o h ))) o δ bur {d} {b} {d} {id1 A d} (f o h) ) 366 h o ((( α bur ( f o h ) ( f o h ) (id1 A d)))o δ bur {d} {b} {d} (id1 A d) (f o h) )
359 ≈⟨ cdr (b3 bur {d} {b} {d} (f o h) {id1 A d} ) ⟩ 367 ≈⟨ cdr (b3 bur {d} {b} {d} (f o h) {id1 A d} ) ⟩
360 h o id1 A d 368 h o id1 A d
361 ≈⟨ idR ⟩ 369 ≈⟨ idR ⟩
362 h 370 h
363 ∎ 371 ∎
364 uniqueness1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → 372 uniqueness1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } →
365 A [ A [ (α bur f g) o k' ] ≈ h ] → A [ k1 {d} h eq ≈ k' ] 373 A [ A [ (α bur f g e) o k' ] ≈ h ] → A [ k1 {d} h eq ≈ k' ]
366 uniqueness1 {d} {h} {eq} {k'} ek=h = let open ≈-Reasoning (A) in 374 uniqueness1 {d} {h} {eq} {k'} ek=h = let open ≈-Reasoning (A) in
367 begin 375 begin
368 k1 {d} h eq 376 k1 {d} h eq
369 ≈⟨⟩ 377 ≈⟨⟩
370 γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} {id1 A d} (f o h) 378 γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} (id1 A d) (f o h)
371 ≈↑⟨ car (cong-γ bur {a} {b} {c} {d} ek=h ) ⟩ 379 ≈↑⟨ car (cong-γ bur {a} {b} {c} {d} ek=h ) ⟩
372 γ bur f g (A [ α bur f g o k' ]) o δ bur {d} {b} {d} {id1 A d} (f o h) 380 γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id1 A d) (f o h)
373 ≈↑⟨ cdr (cong-δ bur {d} {a} {d} (resp {d} {d} {a} {id1 A d} refl-hom ek=h )) ⟩ 381 ≈↑⟨ cdr (cong-δ bur (resp ek=h refl-hom )) ⟩
374 γ bur f g (A [ α bur f g o k' ]) o δ bur (A [ f o A [ α bur f g o k' ] ]) 382 γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id1 A d) ( f o ( α bur f g e o k') )
375 ≈⟨ b4 bur ⟩ 383 ≈⟨ b4 bur ⟩
376 k' 384 k'
377 ∎ 385 ∎
378 386
379 387