Mercurial > hg > Members > kono > Proof > category
changeset 217:306f07bece85
add equalizer+h
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 04 Sep 2013 12:13:27 +0900 |
| parents | 0135419f375c |
| children | 749a1ecbc0b5 |
| files | equalizer.agda |
| diffstat | 1 files changed, 73 insertions(+), 35 deletions(-) [+] |
line wrap: on
line diff
--- a/equalizer.agda Tue Sep 03 13:29:21 2013 +0900 +++ b/equalizer.agda Wed Sep 04 12:13:27 2013 +0900 @@ -48,6 +48,79 @@ open Equalizer open EqEqualizer +-- Equalizer is unique up to iso + +equalizer-iso : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g ) + → Hom A c c' --- != id1 A c +equalizer-iso {c} eqa eqa' = k eqa' (e eqa) (ef=eg eqa) + +-- e eqa f g f +-- c ----------> a ------->b +-- ---> d ---> +-- i h + +equalizer+h : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) (i : Hom A c d ) → (h : Hom A d a ) + → A [ A [ h o i ] ≈ e eqa ] + → Equalizer A {c} (A [ f o h ]) (A [ g o h ] ) +equalizer+h {a} {b} {c} {d} {f} {g} eqa i h eq = record { + e = i ; -- Hom A a d + ef=eg = ef=eg1 ; + k = λ j eq' → k eqa (A [ h o j ]) (fhj=ghj j eq' ) ; + ek=h = ek=h1 ; + uniqueness = uniqueness1 + } where + fhj=ghj : {d' : Obj A } → (j : Hom A d' d ) → + A [ A [ A [ f o h ] o j ] ≈ A [ A [ g o h ] o j ] ] → + A [ A [ f o A [ h o j ] ] ≈ A [ g o A [ h o j ] ] ] + fhj=ghj j eq' = let open ≈-Reasoning (A) in + begin + f o ( h o j ) + ≈⟨ assoc ⟩ + (f o h ) o j + ≈⟨ eq' ⟩ + (g o h ) o j + ≈↑⟨ assoc ⟩ + g o ( h o j ) + ∎ + ef=eg1 : A [ A [ A [ f o h ] o i ] ≈ A [ A [ g o h ] o i ] ] + ef=eg1 = let open ≈-Reasoning (A) in + begin + ( f o h ) o i + ≈↑⟨ assoc ⟩ + f o (h o i ) + ≈⟨ cdr eq ⟩ + f o (e eqa) + ≈⟨ ef=eg eqa ⟩ + g o (e eqa) + ≈↑⟨ cdr eq ⟩ + g o (h o i ) + ≈⟨ assoc ⟩ + ( g o h ) o i + ∎ + ek=h1 : {d' : Obj A} {h' : Hom A d' d} {eq' : A [ A [ A [ f o h ] o h' ] ≈ A [ A [ g o h ] o h' ] ]} → + A [ A [ i o k eqa (A [ h o h' ]) (fhj=ghj h' eq') ] ≈ h' ] + ek=h1 {d'} {h'} {eq'} = let open ≈-Reasoning (A) in + begin + i o k eqa (h o h' ) (fhj=ghj h' eq') + ≈⟨ {!!} ⟩ + h' + ∎ + uniqueness1 : {d' : Obj A} {h' : Hom A d' d} {eq' : A [ A [ A [ f o h ] o h' ] ≈ A [ A [ g o h ] o h' ] ]} {k' : Hom A d' c} → + A [ A [ i o k' ] ≈ h' ] → A [ k eqa (A [ h o h' ]) (fhj=ghj h' eq') ≈ k' ] + uniqueness1 {d'} {h'} {eq'} {k'} ik=h = let open ≈-Reasoning (A) in + begin + k eqa (A [ h o h' ]) (fhj=ghj h' eq') + ≈⟨ uniqueness eqa ( begin + e eqa o k' + ≈↑⟨ car eq ⟩ + (h o i ) o k' + ≈↑⟨ assoc ⟩ + h o (i o k') + ≈⟨ cdr ik=h ⟩ + h o h' + ∎ ) ⟩ + k' + ∎ 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 @@ -71,42 +144,7 @@ -- -- -- 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 ]