Mercurial > hg > Members > kono > Proof > category
changeset 216:0135419f375c
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 03 Sep 2013 13:29:21 +0900 |
| parents | 637b5f58ed28 |
| children | 306f07bece85 |
| files | equalizer.agda |
| diffstat | 1 files changed, 48 insertions(+), 11 deletions(-) [+] |
line wrap: on
line diff
--- a/equalizer.agda Tue Sep 03 04:29:07 2013 +0900 +++ b/equalizer.agda Tue Sep 03 13:29:21 2013 +0900 @@ -48,21 +48,11 @@ open Equalizer open EqEqualizer -ff-equal : {a b : Obj A} (f : Hom A a b) → (eqa : Equalizer A f f ) → A [ e eqa ≈ id1 A a ] -ff-equal {a} {b} f eqa = let open ≈-Reasoning (A) in - begin - e eqa - ≈↑⟨ ek=h eqa ⟩ - e eqa o k eqa (e eqa) refl-hom - ≈⟨ {!!} ⟩ - id1 A a - ∎ - lemma-equ1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a b c : Obj A} (f g : Hom A a b) → ( {a b c : Obj A} → (f g : Hom A a b) → Equalizer A {c} f g ) → EqEqualizer A {c} f g lemma-equ1 A {a} {b} {c} f g eqa = record { - α = λ f g → e (eqa f g ) ; -- Hom A c a + α = λ f g → e (eqa f g ) ; -- Hom A c a γ = λ {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 δ = λ {a} f → k (eqa f f) (id1 A a) (lemma-equ2 f); -- Hom A a c b1 = ef=eg (eqa f g) ; @@ -70,6 +60,53 @@ b3 = lemma-equ3 ; b4 = lemma-equ6 } where + -- + -- e eqa f g f + -- c ----------> a ------->b + -- ^ g + -- | + -- |k₁ = e eqa (f o (e (eqa f g))) (g o (e (eqa f g)))) + -- | + -- d + -- + -- + -- e o id1 ≈ e → k e ≈ id + ff-equal4 : A [ A [ e (eqa f g ) o (e (eqa (A [ f o e (eqa f g) ] ) (A [ g o e (eqa f g) ] ))) ] ≈ + e (eqa f g ) + ] → + A [ k (eqa f g ) (e (eqa f g)) (ef=eg (eqa f g)) ≈ e (eqa (A [ f o e (eqa f g) ] ) (A [ g o e (eqa f g) ] )) ] + ff-equal4 eq = uniqueness (eqa f g) eq + + ff-equal3 : A [ e (eqa (A [ f o e (eqa f g) ] ) (A [ g o e (eqa f g) ] ) ) ≈ k (eqa f g ) (e (eqa f g)) (ef=eg (eqa f g)) ] + ff-equal3 = let open ≈-Reasoning (A) in + begin + e (eqa (A [ f o e (eqa f g) ] ) (A [ g o e (eqa f g) ] ) ) + ≈↑⟨ uniqueness (eqa f g) {!!} ⟩ + k (eqa f g ) (e (eqa f g)) (ef=eg (eqa f g)) + ∎ + ff-equal2 : A [ k (eqa f g) (e (eqa f g)) (ef=eg (eqa f g)) ≈ id1 A a ] + ff-equal2 = let open ≈-Reasoning (A) in + begin + k (eqa f g) (e (eqa f g)) (ef=eg (eqa f g)) + ≈⟨ uniqueness (eqa f g) idR ⟩ + id1 A a + ∎ + ff-equal1 : A [ e (eqa (A [ f o e (eqa f g) ] ) (A [ g o e (eqa f g) ] ) ) ≈ id1 A a ] + ff-equal1 = let open ≈-Reasoning (A) in + begin + e (eqa (f o e (eqa f g) ) (g o e (eqa f g) )) + ≈⟨ {!!} ⟩ + id1 A a + ∎ + ff-equal : {d : Obj A} {k₁ : Hom A d c} → A [ e (eqa (A [ f o A [ e (eqa f g) o k₁ ] ] ) (A [ f o A [ e (eqa f g) o k₁ ] ] ) ) ≈ id1 A d ] + ff-equal {d} {k₁} = let open ≈-Reasoning (A) in + begin + e (eqa (f o e (eqa f g) o k₁) (f o e (eqa f g) o k₁)) + ≈⟨ {!!} ⟩ + id1 A d + ∎ + fg-equal : {d : Obj A} {k₁ : Hom A d c} → A [ e (eqa (A [ f o A [ e (eqa f g) o k₁ ] ] ) (A [ g o A [ e (eqa f g) o k₁ ] ] ) ) ≈ id1 A d ] + fg-equal = {!!} lemma-equ2 : {a b : Obj A} (f : Hom A a b) → A [ A [ f o id1 A a ] ≈ A [ f o id1 A a ] ] lemma-equ2 f = let open ≈-Reasoning (A) in refl-hom lemma-equ3 : A [ A [ e (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f) ] ≈ id1 A a ]