Mercurial > hg > Members > kono > Proof > category
changeset 245:0d1f7bbea9bc
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 09 Sep 2013 12:02:48 +0900 |
| parents | d9317fe71ed6 |
| children | 80d9ef47566b |
| files | equalizer.agda |
| diffstat | 1 files changed, 46 insertions(+), 38 deletions(-) [+] |
line wrap: on
line diff
--- a/equalizer.agda Mon Sep 09 10:22:09 2013 +0900 +++ b/equalizer.agda Mon Sep 09 12:02:48 2013 +0900 @@ -35,23 +35,23 @@ -- 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 field - α : {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 : 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 + δ : {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 } → { e : Hom A c a } - → {f g g' : Hom A a b } → A [ g ≈ g' ] → A [ α f g {e} ≈ α f g' {e} ] + → {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 [ γ {a} {b} {c} {d} f g h ≈ γ f g h' ] - cong-δ : {a b c : Obj A } → {f f' : Hom A a b} → A [ f ≈ f' ] → A [ δ f ≈ δ f' ] - 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} ] ] - 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 ] + 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' ] + 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) ] ] + 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 ] -- b4 : {c d : Obj A } {k : Hom A c a} → A [ β f g ( A [ α f g o k ] ) ≈ k ] b4 : {d : Obj A } {k : Hom A d c} → - 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 ] + 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 ] -- A [ α f g o β f g h ] ≈ h β : { d a b : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A d c - β {d} {a} {b} f g h = A [ γ {a} {b} {c} f g h o δ {d} {b} {d} {id1 A d} (A [ f o h ]) ] + β {d} {a} {b} f g h = A [ γ {a} {b} {c} f g h o δ {d} {b} {d} (id1 A d) (A [ f o h ]) ] open Equalizer open Burroni @@ -231,13 +231,13 @@ ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g ) → 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} 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} {e} f → k (eqa {a} {b} {c} f f {e} ) (id1 A a) (lemma-equ2 f); -- Hom A a c + δ = λ {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 ; - cong-δ = λ {a b c f f'} f=f' → cong-δ1 {a} {b} {c} {f} {f'} f=f' ; + cong-δ = λ {a b c e f f'} f=f' → cong-δ1 {a} {b} {c} {e} {f} {f'} f=f' ; b1 = fe=ge (eqa {a} {b} {c} f g {e}) ; b2 = lemma-b2 ; b3 = lemma-b3 ; @@ -276,6 +276,26 @@ ≈↑⟨ assoc ⟩ g o ( h o equalizer (eqa (f o h) ( g o h ))) ∎ + 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 {a} {_} {c} {d} {f} {g} {h} {h'} h=h' = let open ≈-Reasoning (A) in begin + 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 ) + ≈⟨ uniqueness (eqa f g) ( begin + {!!} o {!!} + ≈⟨ {!!} ⟩ + h o equalizer (eqa ( f o h ) ( g o h )) + ∎ )⟩ + {!!} o {!!} + ≈↑⟨ uniqueness (eqa f g) {!!} ⟩ + 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 : {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) ≈ + k (eqa {a} {b} {c} f' f' {e} ) (id1 A a) (lemma-equ2 f') ] + cong-δ1 = {!!} lemma-b2 : {d : Obj A} {h : Hom A d a} → A [ 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) ] ≈ A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ] ] @@ -316,22 +336,10 @@ ≈⟨ 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 = {!!} --- {a₁ b₁ c₃ : Obj A} {f₁ f' : Hom A a₁ b₁} → A [ f₁ ≈ f' ] → --- A [ k (eqa f₁ f₁) (id1 A a₁) (lemma-equ2 f₁) ≈ k (eqa f' f') (id1 A a₁) (lemma-equ2 f') ] - 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) ≈ - k (eqa {a} {b} {c} f' f' {e} ) (id1 A a) (lemma-equ2 f') ] - cong-δ1 = {!!} lemma-equ2 : {a b c : Obj A} (f g : Hom A a b) (e : Hom A c a ) - → ( bur : Burroni A {c} {a} {b} f g e ) → Equalizer A {c} {a} {b} (α bur f g) f g + → ( bur : Burroni A {c} {a} {b} f g e ) → Equalizer A {c} {a} {b} (α bur f g e) f g lemma-equ2 {a} {b} {c} f g e bur = record { fe=ge = fe=ge1 ; k = k1 ; @@ -340,38 +348,38 @@ } where k1 : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c k1 {d} h fh=gh = β bur {d} {a} {b} f g h - fe=ge1 : A [ A [ f o (α bur f g) ] ≈ A [ g o (α bur f g) ] ] + fe=ge1 : A [ A [ f o (α bur f g e) ] ≈ A [ g o (α bur f g e) ] ] fe=ge1 = b1 bur - 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 ] + 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 ] ek=h1 {d} {h} {eq} = let open ≈-Reasoning (A) in begin - α bur f g o k1 h eq + α bur f g e o k1 h eq ≈⟨⟩ - α bur f g o ( γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} {id1 A d} (f o h) ) + α bur f g e o ( γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} (id1 A d) (f o h) ) ≈⟨ assoc ⟩ - ( α bur f g o γ bur {a} {b} {c} f g h ) o δ bur {d} {b} {d} {id1 A d} (f o h) + ( α bur f g e o γ bur {a} {b} {c} f g h ) o δ bur {d} {b} {d} (id1 A d) (f o h) ≈⟨ car (b2 bur) ⟩ - ( h o ( α bur ( f o h ) ( g o h ))) o δ bur {d} {b} {d} {id1 A d} (f o h) + ( h o ( α bur ( f o h ) ( g o h ) (id1 A d))) o δ bur {d} {b} {d} (id1 A d) (f o h) ≈↑⟨ assoc ⟩ - h o ((( α bur ( f o h ) ( g o h ))) o δ bur {d} {b} {d} {id1 A d} (f o h) ) + h o ((( α bur ( f o h ) ( g o h ) (id1 A d) )) o δ bur {d} {b} {d} (id1 A d) (f o h) ) ≈↑⟨ cdr ( car ( cong-α bur eq)) ⟩ - h o ((( α bur ( f o h ) ( f o h ))) o δ bur {d} {b} {d} {id1 A d} (f o h) ) + h o ((( α bur ( f o h ) ( f o h ) (id1 A d)))o δ bur {d} {b} {d} (id1 A d) (f o h) ) ≈⟨ cdr (b3 bur {d} {b} {d} (f o h) {id1 A d} ) ⟩ h o id1 A d ≈⟨ idR ⟩ h ∎ uniqueness1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → - A [ A [ (α bur f g) o k' ] ≈ h ] → A [ k1 {d} h eq ≈ k' ] + A [ A [ (α bur f g e) o k' ] ≈ h ] → A [ k1 {d} h eq ≈ k' ] uniqueness1 {d} {h} {eq} {k'} ek=h = let open ≈-Reasoning (A) in begin k1 {d} h eq ≈⟨⟩ - γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} {id1 A d} (f o h) + γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} (id1 A d) (f o h) ≈↑⟨ car (cong-γ bur {a} {b} {c} {d} ek=h ) ⟩ - γ bur f g (A [ α bur f g o k' ]) o δ bur {d} {b} {d} {id1 A d} (f o h) - ≈↑⟨ cdr (cong-δ bur {d} {a} {d} (resp {d} {d} {a} {id1 A d} refl-hom ek=h )) ⟩ - γ bur f g (A [ α bur f g o k' ]) o δ bur (A [ f o A [ α bur f g o k' ] ]) + γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id1 A d) (f o h) + ≈↑⟨ cdr (cong-δ bur (resp ek=h refl-hom )) ⟩ + γ 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') ) ≈⟨ b4 bur ⟩ k' ∎