Mercurial > hg > Members > kono > Proof > category
diff equalizer.agda @ 235:8835015a3e1a
passed let;s remove yellow
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 08 Sep 2013 04:55:01 +0900 |
| parents | c02287d3d2dc |
| children | e20b81102eee |
line wrap: on
line diff
--- a/equalizer.agda Sun Sep 08 03:56:45 2013 +0900 +++ b/equalizer.agda Sun Sep 08 04:55:01 2013 +0900 @@ -182,7 +182,7 @@ c-iso← : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g ) → ( keqa : Equalizer A (k eqa' e (fe=ge eqa )) (A [ f o e' ]) (A [ g o e' ]) ) → ( keqa' : Equalizer A (k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )) (A [ f o e ]) (A [ g o e ]) ) - → { e'->e : A [ e' ≈ A [ e o equalizer keqa' ] ] } + → { e'->e : A [ e' ≈ A [ e o equalizer keqa' ] ] } -- refl → A [ A [ c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa ] ≈ id1 A c ] c-iso← {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa keqa' {e'->e} = let open ≈-Reasoning (A) in begin c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa @@ -282,6 +282,8 @@ ------- α(f,g) γ(f,g,α(f,g)j) δ(fα(f,g)j) = α(f,g)j ------- γ(f,g,α(f,g)j) δ(fα(f,g)j) = j + eefg : {a b c : Obj A} (f g : Hom A a b) {e : Hom A c a} → Equalizer A e ( A [ f o equalizer (eqa f g) ] ) (A [ g o equalizer (eqa f g) ] ) + eefg f g {e} = eqa ( A [ f o equalizer (eqa f g) ] ) (A [ g o equalizer (eqa f g) ] ) lemma-b4 : {d : Obj A} {j : Hom A d c} → A [ A [ k (eqa f g) (A [ A [ equalizer (eqa f g) o j ] o equalizer (eqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ g o A [ equalizer (eqa f g) o j ] ])) ]) (lemma-equ4 {a} {b} {c} f g (A [ equalizer (eqa f g) o j ])) o @@ -292,9 +294,23 @@ ( k (eqa f g) (( ( equalizer (eqa f g) o j ) o equalizer (eqa (( f o ( equalizer (eqa f g) o j ) )) (( g o ( equalizer (eqa f g) o j ) ))) )) (lemma-equ4 {a} {b} {c} f g (( equalizer (eqa f g) o j ))) o k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (lemma-equ2 (( f o ( equalizer (eqa f g) o j ) ))) ) - ≈⟨ {!!} ⟩ + ≈⟨ car ((uniqueness (eqa f g) ( begin + equalizer (eqa f g) o j + ≈↑⟨ idR ⟩ + (equalizer (eqa f g) o j ) o id1 A d + ≈⟨⟩ + ((equalizer (eqa f g) o j) o equalizer (eqa (f o equalizer (eqa f g) o j) (g o equalizer (eqa f g) o j))) + ∎ ))) ⟩ + j o k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (lemma-equ2 (( f o ( equalizer (eqa f g) o j ) ))) + ≈⟨ cdr ((uniqueness (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) ( begin + equalizer (eqa (f o equalizer (eqa f g) o j) (f o equalizer (eqa f g) o j)) + ≈⟨ {!!} ⟩ + id1 A d + ∎ ))) ⟩ + j o id1 A d + ≈⟨ idR ⟩ j - ∎ + ∎ -- end