Mercurial > hg > Members > kono > Proof > category
diff equalizer.agda @ 253:24e83b8b81be
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 11 Sep 2013 20:26:48 +0900 |
| parents | e0835b8dd51b |
| children | 45b81fcb8a64 |
line wrap: on
line diff
--- a/equalizer.agda Mon Sep 09 16:15:09 2013 +0900 +++ b/equalizer.agda Wed Sep 11 20:26:48 2013 +0900 @@ -30,6 +30,7 @@ equalizer : Hom A c a equalizer = e + -- -- Burroni's Flat Equational Definition of Equalizer -- @@ -116,7 +117,7 @@ ≈⟨ cdr assoc ⟩ e o (( h-1 o h) o k eqa j eq ) ≈⟨ cdr (car h-1h=1 ) ⟩ - e o (id1 A c o k eqa j eq ) + e o (id c o k eqa j eq ) ≈⟨ cdr idL ⟩ e o k eqa j eq ≈⟨ ek=h eqa ⟩ @@ -139,7 +140,7 @@ ≈⟨ assoc ⟩ (h o h-1 ) o j ≈⟨ car hh-1=1 ⟩ - id1 A c' o j + id c' o j ≈⟨ idL ⟩ j ∎ @@ -194,23 +195,23 @@ e'←e {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa = let open ≈-Reasoning (A) in begin e o c-iso-r eqa eqa' keqa ≈⟨⟩ - e o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) + e o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) ≈↑⟨ car (ek=h eqa' ) ⟩ - ( equalizer eqa' o k eqa' e (fe=ge eqa) ) o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) + ( equalizer eqa' o k eqa' e (fe=ge eqa) ) o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) ≈⟨⟩ - ( e' o k eqa' e (fe=ge eqa) ) o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) + ( e' o k eqa' e (fe=ge eqa) ) o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) ≈↑⟨ assoc ⟩ - e' o (( k eqa' e (fe=ge eqa) ) o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) ) + e' o (( k eqa' e (fe=ge eqa) ) o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) ) ≈⟨⟩ - e' o (equalizer keqa o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) ) + e' o (equalizer keqa o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) ) ≈⟨ cdr ( ek=h keqa ) ⟩ - e' o id1 A c' + e' o id c' ≈⟨ idR ⟩ e' ∎ --- e←e' e'←e = e --- e'←e e←e = e' is enough for isomorphism but we want to prove l o r = id also. +-- e←e' e'←e e = e +-- e'←e e←e e' = e' is enough for isomorphism but we can prove l o r = id also. 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' ]) ) @@ -218,9 +219,9 @@ c-iso→ {c} {c'} {a} {b} {f} {g} eqa eqa' keqa = let open ≈-Reasoning (A) in begin c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa ≈⟨⟩ - equalizer keqa o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) + equalizer keqa o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) ≈⟨ ek=h keqa ⟩ - id1 A c' + id c' ∎ 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 ) @@ -230,26 +231,26 @@ c-iso← {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa keqa' = let open ≈-Reasoning (A) in begin c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa ≈⟨⟩ - k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) o k eqa' e (fe=ge eqa ) + k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) o k eqa' e (fe=ge eqa ) ≈⟨⟩ equalizer keqa' o k eqa' e (fe=ge eqa ) ≈⟨ cdr ( begin k eqa' e (fe=ge eqa ) ≈⟨ uniqueness eqa' ( begin - e' o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c)) + e' o k keqa' (id c) (f1=g1 (fe=ge eqa) (id c)) ≈↑⟨ car (e'←e eqa eqa' keqa ) ⟩ - ( e o equalizer keqa' ) o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c)) + ( e o equalizer keqa' ) o k keqa' (id c) (f1=g1 (fe=ge eqa) (id c)) ≈↑⟨ assoc ⟩ - e o ( equalizer keqa' o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c))) + e o ( equalizer keqa' o k keqa' (id c) (f1=g1 (fe=ge eqa) (id c))) ≈⟨ cdr ( ek=h keqa' ) ⟩ - e o id1 A c + e o id c ≈⟨ idR ⟩ e ∎ )⟩ - k keqa' (id1 A c) ( f1=g1 (fe=ge eqa) (id1 A c) ) + k keqa' (id c) ( f1=g1 (fe=ge eqa) (id c) ) ∎ )⟩ - equalizer keqa' o k keqa' (id1 A c) ( f1=g1 (fe=ge eqa) (id1 A c) ) ≈⟨ ek=h keqa' ⟩ - id1 A c + equalizer keqa' o k keqa' (id c) ( f1=g1 (fe=ge eqa) (id c) ) ≈⟨ ek=h keqa' ⟩ + id c ∎ @@ -292,9 +293,9 @@ lemma-b3 : {a b d : Obj A} (f : Hom A a b ) { h : Hom A d a } → A [ A [ equalizer (eqa f f ) o k (eqa f f) (id1 A a) (f1=f1 f) ] ≈ id1 A a ] lemma-b3 {a} {b} {d} f {h} = let open ≈-Reasoning (A) in begin - equalizer (eqa f f) o k (eqa f f) (id1 A a) (f1=f1 f) + equalizer (eqa f f) o k (eqa f f) (id a) (f1=f1 f) ≈⟨ ek=h (eqa f f ) ⟩ - id1 A a + id a ∎ lemma-equ4 : {a b c d : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → A [ A [ f o A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ] ] ≈ A [ g o A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ] ] ] @@ -329,13 +330,13 @@ k (eqa {a} {b} {c} f' f' {e} ) (id1 A a) (f1=f1 f') ] cong-δ1 {a} {b} {c} {e} {f} {f'} f=f' = let open ≈-Reasoning (A) in begin - k (eqa {a} {b} {c} f f {e} ) (id1 A a) (f1=f1 f) + k (eqa {a} {b} {c} f f {e} ) (id a) (f1=f1 f) ≈⟨ uniqueness (eqa f f) ( begin - e o k (eqa {a} {b} {c} f' f' {e} ) (id1 A a) (f1=f1 f') + e o k (eqa {a} {b} {c} f' f' {e} ) (id a) (f1=f1 f') ≈⟨ ek=h (eqa {a} {b} {c} f' f' {e} ) ⟩ - id1 A a + id a ∎ )⟩ - k (eqa {a} {b} {c} f' f' {e} ) (id1 A a) (f1=f1 f') + k (eqa {a} {b} {c} f' f' {e} ) (id a) (f1=f1 f') ∎ lemma-b2 : {d : Obj A} {h : Hom A d a} → A [ @@ -362,19 +363,19 @@ ≈⟨ car ((uniqueness (eqa f g) ( begin equalizer (eqa f g) o j ≈↑⟨ idR ⟩ - (equalizer (eqa f g) o j ) o id1 A d - ≈⟨⟩ -- here we decide e (fej) (gej)' is id1 A d + (equalizer (eqa f g) o j ) o id d + ≈⟨⟩ -- here we decide e (fej) (gej)' is id d ((equalizer (eqa f g) o j) o equalizer (eqa (f o equalizer (eqa f g {e}) o j) (g o equalizer (eqa f g {e}) 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) (f1=f1 (( 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 {e} ) o j) (f o equalizer (eqa f g {e}) o j)) o id1 A d + equalizer (eqa (f o equalizer (eqa f g {e} ) o j) (f o equalizer (eqa f g {e}) o j)) o id d ≈⟨ idR ⟩ equalizer (eqa (f o equalizer (eqa f g {e}) o j) (f o equalizer (eqa f g {e}) o j)) - ≈⟨⟩ -- here we decide e (fej) (fej)' is id1 A d - id1 A d + ≈⟨⟩ -- here we decide e (fej) (fej)' is id d + id d ∎ ))) ⟩ - j o id1 A d + j o id d ≈⟨ idR ⟩ j ∎ @@ -401,17 +402,17 @@ begin α bur f g e o k1 h eq ≈⟨⟩ - α bur f g e 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} (id d) (f o h) ) ≈⟨ assoc ⟩ - ( α bur f g e 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} (id d) (f o h) ≈⟨ car (b2 bur) ⟩ - ( h o ( α bur ( f o h ) ( g o h ) (id1 A d))) o δ bur {d} {b} {d} (id1 A d) (f o h) + ( h o ( α bur ( f o h ) ( g o h ) (id d))) o δ bur {d} {b} {d} (id d) (f o h) ≈↑⟨ assoc ⟩ - h o ((( α bur ( f o h ) ( g o h ) (id1 A d) )) o δ bur {d} {b} {d} (id1 A d) (f o h) ) + h o ((( α bur ( f o h ) ( g o h ) (id d) )) o δ bur {d} {b} {d} (id d) (f o h) ) ≈↑⟨ cdr ( car ( cong-α bur eq)) ⟩ - 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 + h o ((( α bur ( f o h ) ( f o h ) (id d)))o δ bur {d} {b} {d} (id d) (f o h) ) + ≈⟨ cdr (b3 bur {d} {b} {d} (f o h) {id d} ) ⟩ + h o id d ≈⟨ idR ⟩ h ∎ @@ -421,11 +422,11 @@ 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} (id d) (f o h) ≈↑⟨ car (cong-γ bur {a} {b} {c} {d} ek=h ) ⟩ - γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id1 A d) (f o h) + γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id 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') ) + γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id d) ( f o ( α bur f g e o k') ) ≈⟨ b4 bur ⟩ k' ∎