Mercurial > hg > Members > kono > Proof > category

changeset 246:80d9ef47566b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
cong-γ1 done, cong-δ1 remains
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 09 Sep 2013 12:35:56 +0900
parents 0d1f7bbea9bc
children f6e8d6d04af8
files equalizer.agda
diffstat 1 files changed, 32 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/equalizer.agda	Mon Sep 09 12:02:48 2013 +0900
+++ b/equalizer.agda	Mon Sep 09 12:35:56 2013 +0900
@@ -235,8 +235,8 @@
       γ = λ {a} {b} {c} {d} f g 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 ) ;  -- Hom A c d
       δ =  λ {a} {b} {c} e f → k (eqa {a} {b} {c} f f {e} ) (id1 A a)  (lemma-equ2 f); -- Hom A a c
-      cong-α = cong-α1 ;
-      cong-γ = cong-γ1 ;
+      cong-α = λ {a b c e f g g'} eq → cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq ;
+      cong-γ = λ {a} {_} {c} {d} {f} {g} {h} {h'} eq → cong-γ1 {a} {_} {c} {d} {f} {g} {h} {h'} eq  ;
       cong-δ = λ {a b c e f f'} f=f' → cong-δ1 {a} {b} {c} {e} {f} {f'} f=f'  ;
       b1 = fe=ge (eqa {a} {b} {c} f g {e}) ;
       b2 = lemma-b2 ;
@@ -279,18 +279,40 @@
      cong-α1 : {a b c :  Obj A } → { e : Hom A c a }
           → {f g g' : Hom A a b } →  A [ g ≈ g' ] → A [ equalizer (eqa {a} {b} {c} f g {e} )≈ equalizer (eqa {a} {b} {c} f g' {e} ) ] 
      cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq = let open ≈-Reasoning (A) in refl-hom 
-     cong-γ1 :  {a _ c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } →  A [ h ≈ h' ] →  
-                     A [  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 ) 
-                       ≈  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} {_} {c} {d} {f} {g} {h} {h'} h=h' = let open ≈-Reasoning (A) in begin
+     cong-γ1 :  {a _ c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } →  A [ h ≈ h' ] →  { e : Hom A c a} →
+                     A [  k (eqa f g {e} ) {d} ( A [ h  o (equalizer ( eqa (A [ f  o  h  ] ) (A [ g o h  ] ) {id1 A d} )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) 
+                       ≈  k (eqa f g {e} ) {d} ( A [ h' o (equalizer ( eqa (A [ f  o  h' ] ) (A [ g o h' ] ) {id1 A d} )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' )  ]
+     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
-                 {!!}  o {!!}
-                 ≈⟨ {!!} ⟩
+                 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 )) 
              ∎ )⟩    
-                 {!!}  o {!!} 
-             ≈↑⟨ uniqueness (eqa f g) {!!} ⟩    
+                 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)  ≈