Mercurial > hg > Members > kono > Proof > category

comparison equalizer.agda @ 240:964e258e08fb

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 Sun, 08 Sep 2013 11:54:06 +0900
parents 08afb6ad80c7
children 9e4dc349831e
comparison
equal deleted inserted replaced
239:08afb6ad80c7 240:964e258e08fb
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 } → {g g' : Hom A a b } → A [ g ≈ g' ] → { α α' : Hom A c a } → A [ α ≈ α' ]
42 cong-γ : {a _ c d : Obj A } → {h h' : Hom A d a } → A [ h ≈ h' ] → { γ γ' : Hom A d c } → A [ γ ≈ γ' ]
43 cong-δ : {a b c : Obj A } → {f f' : Hom A a b} → A [ f ≈ f' ] → { δ δ' : Hom A a c } → A [ δ ≈ δ' ]
41 b1 : A [ A [ f o α {a} {b} {c} f g {e} ] ≈ A [ g o α {a} {b} {c} f g {e} ] ] 44 b1 : A [ A [ f o α {a} {b} {c} f g {e} ] ≈ A [ g o α {a} {b} {c} f g {e} ] ]
42 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} ] ] 45 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} ] ]
43 b3 : A [ A [ α {a} {b} {a} f f {id1 A a} o δ {a} {b} {a} {id1 A a} f ] ≈ id1 A a ] 46 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 ]
44 -- b4 : {c d : Obj A } {k : Hom A c a} → A [ β f g ( A [ α f g o k ] ) ≈ k ] 47 -- b4 : {c d : Obj A } {k : Hom A c a} → A [ β f g ( A [ α f g o k ] ) ≈ k ]
45 b4 : {d : Obj A } {k : Hom A d c} → 48 b4 : {d : Obj A } {k : Hom A d c} →
46 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 ] 49 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 ]
47 -- A [ α f g o β f g h ] ≈ h 50 -- A [ α f g o β f g h ] ≈ h
48 β : { d a b : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A d c 51 β : { d a b : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A d c
225 → Burroni A {c} {a} {b} f g e 228 → Burroni A {c} {a} {b} f g e
226 lemma-equ1 {a} {b} {c} f g e eqa = record { 229 lemma-equ1 {a} {b} {c} f g e eqa = record {
227 α = λ {a} {b} {c} f g {e} → equalizer (eqa {a} {b} {c} f g {e} ) ; -- Hom A c a 230 α = λ {a} {b} {c} f g {e} → equalizer (eqa {a} {b} {c} f g {e} ) ; -- Hom A c a
228 γ = λ {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 ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) ; -- Hom A c d 231 γ = λ {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 ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) ; -- Hom A c d
229 δ = λ {a} {b} {c} {e} f → k (eqa {a} {b} {c} f f {e} ) (id1 A a) (lemma-equ2 f); -- Hom A a c 232 δ = λ {a} {b} {c} {e} f → k (eqa {a} {b} {c} f f {e} ) (id1 A a) (lemma-equ2 f); -- Hom A a c
233 cong-α = cong-α1 ;
234 cong-γ = cong-γ1 ;
235 cong-δ = cong-δ1 ;
230 b1 = fe=ge (eqa {a} {b} {c} f g {e}) ; 236 b1 = fe=ge (eqa {a} {b} {c} f g {e}) ;
231 b2 = lemma-b2 ; 237 b2 = lemma-b2 ;
232 b3 = lemma-b3 ; 238 b3 = lemma-b3 ;
233 b4 = lemma-b4 239 b4 = lemma-b4
234 } where 240 } where
241 cong-α1 : {a b c : Obj A } → {g g' : Hom A a b } → A [ g ≈ g' ] → { α α' : Hom A c a } → A [ α ≈ α' ]
242 cong-α1 {a} {b} {c} {g} {g'} eq = let open ≈-Reasoning (A) in {!!}
243 cong-γ1 : {a _ c d : Obj A } → {h h' : Hom A d a } → A [ h ≈ h' ] → { γ γ' : Hom A d c } → A [ γ ≈ γ' ]
244 cong-γ1 = {!!}
245 cong-δ1 : {a b c : Obj A } → {f f' : Hom A a b} → A [ f ≈ f' ] → { δ δ' : Hom A a c } → A [ δ ≈ δ' ]
246 cong-δ1 = {!!}
235 -- 247 --
236 -- e eqa f g f 248 -- e eqa f g f
237 -- c ----------> a ------->b 249 -- c ----------> a ------->b
238 -- ^ g 250 -- ^ g
239 -- | 251 -- |
244 -- 256 --
245 -- e o id1 ≈ e → k e ≈ id 257 -- e o id1 ≈ e → k e ≈ id
246 258
247 lemma-equ2 : {a b : Obj A} (f : Hom A a b) → A [ A [ f o id1 A a ] ≈ A [ f o id1 A a ] ] 259 lemma-equ2 : {a b : Obj A} (f : Hom A a b) → A [ A [ f o id1 A a ] ≈ A [ f o id1 A a ] ]
248 lemma-equ2 f = let open ≈-Reasoning (A) in refl-hom 260 lemma-equ2 f = let open ≈-Reasoning (A) in refl-hom
249 lemma-b3 : A [ A [ equalizer (eqa f f ) o k (eqa f f) (id1 A a) (lemma-equ2 f) ] ≈ id1 A a ] 261 lemma-b3 : {a b d : Obj A} (f : Hom A a b ) { h : Hom A d a } → A [ A [ equalizer (eqa f f ) o k (eqa f f) (id1 A a) (lemma-equ2 f) ] ≈ id1 A a ]
250 lemma-b3 = let open ≈-Reasoning (A) in 262 lemma-b3 {a} {b} {d} f {h} = let open ≈-Reasoning (A) in
251 begin 263 begin
252 equalizer (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f) 264 equalizer (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f)
253 ≈⟨ ek=h (eqa f f ) ⟩ 265 ≈⟨ ek=h (eqa f f ) ⟩
254 id1 A a 266 id1 A a
255 ∎ 267 ∎
329 ( α bur f g o γ bur {a} {b} {c} f g h ) o δ bur {d} {b} {d} {id1 A d} (f o h) 341 ( α bur f g o γ bur {a} {b} {c} f g h ) o δ bur {d} {b} {d} {id1 A d} (f o h)
330 ≈⟨ car (b2 bur) ⟩ 342 ≈⟨ car (b2 bur) ⟩
331 ( h o ( α bur ( f o h ) ( g o h ))) o δ bur {d} {b} {d} {id1 A d} (f o h) 343 ( h o ( α bur ( f o h ) ( g o h ))) o δ bur {d} {b} {d} {id1 A d} (f o h)
332 ≈↑⟨ assoc ⟩ 344 ≈↑⟨ assoc ⟩
333 h o ((( α bur ( f o h ) ( g o h ))) o δ bur {d} {b} {d} {id1 A d} (f o h) ) 345 h o ((( α bur ( f o h ) ( g o h ))) o δ bur {d} {b} {d} {id1 A d} (f o h) )
334 ≈⟨ cdr {!!} ⟩ 346 ≈↑⟨ cdr ( car ( cong-α bur eq)) ⟩
347 h o ((( α bur ( f o h ) ( f o h ))) o δ bur {d} {b} {d} {id1 A d} (f o h) )
348 ≈⟨ cdr (b3 bur {d} {b} {d} (f o h) {id1 A d} ) ⟩
335 h o id1 A d 349 h o id1 A d
336 ≈⟨ {!!} ⟩ 350 ≈⟨ idR ⟩
337 h 351 h
338 ∎ 352 ∎
339 uniqueness1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → 353 uniqueness1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } →
340 A [ A [ (α bur f g) o k' ] ≈ h ] → A [ k1 {d} h eq ≈ k' ] 354 A [ A [ (α bur f g) o k' ] ≈ h ] → A [ k1 {d} h eq ≈ k' ]
341 uniqueness1 {d} {h} {eq} {k'} ek=h = let open ≈-Reasoning (A) in 355 uniqueness1 {d} {h} {eq} {k'} ek=h = let open ≈-Reasoning (A) in
342 begin 356 begin
343 k1 {d} h eq 357 k1 {d} h eq
344 ≈⟨⟩ 358 ≈⟨⟩
345 γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} {id1 A d} (f o h) 359 γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} {id1 A d} (f o h)
346 ≈⟨ ? ⟩ 360 ≈↑⟨ car (cong-γ bur {a} {b} {c} {d} ek=h ) ⟩
361 γ bur f g (A [ α bur f g o k' ]) o δ bur {d} {b} {d} {id1 A d} (f o h)
362 ≈↑⟨ cdr (cong-δ bur {d} {a} {d} (resp {d} {d} {a} {id1 A d} refl-hom ek=h )) ⟩
363 γ bur f g (A [ α bur f g o k' ]) o δ bur (A [ f o A [ α bur f g o k' ] ])
364 ≈⟨ b4 bur ⟩
347 k' 365 k'
348 ∎ 366 ∎
349 367
350 368
351 -- end 369 -- end