Mercurial > hg > Members > kono > Proof > category
changeset 248:efa2fd0e91ee
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 09 Sep 2013 12:55:36 +0900 |
| parents | f6e8d6d04af8 |
| children | bdeed843f8b1 |
| files | equalizer.agda |
| diffstat | 1 files changed, 5 insertions(+), 27 deletions(-) [+] |
line wrap: on
line diff
--- a/equalizer.agda Mon Sep 09 12:47:53 2013 +0900 +++ b/equalizer.agda Mon Sep 09 12:55:36 2013 +0900 @@ -285,34 +285,12 @@ cong-γ1 {a} {c} {d} {f} {g} {h} {h'} h=h' {e} = 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 - e o ( k (eqa f f {e}) (id1 A a) (f1=f1 f) o h) - ≈⟨ assoc ⟩ - (e o k (eqa f f {e}) (id1 A a) (f1=f1 f)) o h - ≈⟨ car ( ek=h (eqa f f {e})) ⟩ - id1 A a o h - ≈⟨ idL ⟩ - h - ≈↑⟨ idR ⟩ - h o (id1 A d ) - ≈⟨⟩ - h o equalizer (eqa ( f o h ) ( g o h )) + e o 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' ) + ≈⟨ ek=h (eqa f g ) ⟩ + h' o (equalizer ( eqa (A [ f o h' ] ) (A [ g o h' ] ))) + ≈↑⟨ car h=h' ⟩ + h o (equalizer ( eqa (A [ f o h' ] ) (A [ g o h' ] ))) ∎ )⟩ - k (eqa f f {e}) (id1 A a) (f1=f1 f) o h - ≈⟨ cdr h=h' ⟩ - k (eqa f f {e}) (id1 A a) (f1=f1 f) o h' - ≈↑⟨ uniqueness (eqa f g) ( begin - e o ( k (eqa f f {e}) (id1 A a) (f1=f1 f) o h') - ≈⟨ assoc ⟩ - (e o k (eqa f f {e}) (id1 A a) (f1=f1 f)) o h' - ≈⟨ car ( ek=h (eqa f f {e})) ⟩ - id1 A a o h' - ≈⟨ idL ⟩ - h' - ≈↑⟨ idR ⟩ - h' o (id1 A d ) - ≈⟨⟩ - h' o equalizer (eqa ( f o h' ) ( g o 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} {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) ≈