Mercurial > hg > Members > kono > Proof > category
changeset 242:5d1ecfec6f41
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 08 Sep 2013 17:47:04 +0900 |
| parents | 9e4dc349831e |
| children | 40ac16f69708 |
| files | equalizer.agda |
| diffstat | 1 files changed, 16 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/equalizer.agda Sun Sep 08 12:34:35 2013 +0900 +++ b/equalizer.agda Sun Sep 08 17:47:04 2013 +0900 @@ -38,8 +38,11 @@ α : {a b c : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → {e : Hom A c a } → Hom A c a γ : {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 δ : {a b c : Obj A } → {e : Hom A c a } → (f : Hom A a b) → Hom A a c - cong-α : {a b c : Obj A } → {g g' : Hom A a b } → A [ g ≈ g' ] → { α α' : Hom A c a } → A [ α ≈ α' ] - cong-γ : {a _ c d : Obj A } → {h h' : Hom A d a } → A [ h ≈ h' ] → { γ γ' : Hom A d c } → A [ γ ≈ γ' ] + cong-α : {a b c : Obj A } → { e : Hom A c a } + → {f g g' : Hom A a b } → A [ g ≈ g' ] → A [ α f g {e} ≈ α f g' {e} ] + cong-γ : {a _ c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } → A [ h ≈ h' ] + → { γ γ' : {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 } + → A [ γ f g h ≈ γ' f g h' ] cong-δ : {a b c : Obj A } → {f f' : Hom A a b} → A [ f ≈ f' ] → { δ δ' : Hom A a c } → A [ δ ≈ δ' ] b1 : A [ A [ f o α {a} {b} {c} f g {e} ] ≈ A [ g o α {a} {b} {c} f g {e} ] ] 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} ] ] @@ -230,7 +233,8 @@ → Burroni A {c} {a} {b} f g e lemma-equ1 {a} {b} {c} f g e eqa = record { α = λ {a} {b} {c} f g {e} → equalizer (eqa {a} {b} {c} f g {e} ) ; -- Hom A c a - γ = λ {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 + γ = λ {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 δ = λ {a} {b} {c} {e} f → k (eqa {a} {b} {c} f f {e} ) (id1 A a) (lemma-equ2 f); -- Hom A a c cong-α = cong-α1 ; cong-γ = cong-γ1 ; @@ -240,12 +244,6 @@ b3 = lemma-b3 ; b4 = lemma-b4 } where - cong-α1 : {a b c : Obj A } → {g g' : Hom A a b } → A [ g ≈ g' ] → { α α' : Hom A c a } → A [ α ≈ α' ] - cong-α1 {a} {b} {c} {g} {g'} eq = let open ≈-Reasoning (A) in {!!} - cong-γ1 : {a _ c d : Obj A } → {h h' : Hom A d a } → A [ h ≈ h' ] → { γ γ' : Hom A d c } → A [ γ ≈ γ' ] - cong-γ1 = {!!} - cong-δ1 : {a b c : Obj A } → {f f' : Hom A a b} → A [ f ≈ f' ] → { δ δ' : Hom A a c } → A [ δ ≈ δ' ] - cong-δ1 = {!!} -- -- e eqa f g f -- c ----------> a ------->b @@ -319,6 +317,15 @@ ≈⟨ idR ⟩ j ∎ + cong-α1 : {a b c : Obj A } → { e : Hom A c a } + → {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} ) ] + cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq = let open ≈-Reasoning (A) in refl-hom + cong-γ1 : {a _ c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } → A [ h ≈ h' ] → + 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 ) + ≈ 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' ) ] + cong-γ1 = {!!} + cong-δ1 : {a b c : Obj A } → {f f' : Hom A a b} → A [ f ≈ f' ] → { δ δ' : Hom A a c } → A [ δ ≈ δ' ] + cong-δ1 = {!!} lemma-equ2 : {a b c : Obj A} (f g : Hom A a b) (e : Hom A c a )